Induction for innermost and outermost ground termination
Identifieur interne : 008F59 ( Main/Exploration ); précédent : 008F58; suivant : 008F60Induction for innermost and outermost ground termination
Auteurs : Isabelle Gnaedig ; Hélène Kirchner ; Olivier FissoreSource :
English descriptors
- KwdEn :
Abstract
We propose an original approach to prove termination of innermost rewriting on ground term algebras, based on induction, abstraction and narrowing. Our method applies in particular to non-terminating systems which are innermost terminating, and to systems that do not innermost terminate on the free term algebra but do on the ground term one. The induction relation, an F-stable ordering having the subterm property, is not given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints. The method is based on an abstraction mechanism, introducing variables that represent ground terms in normal form, and on narrowing, schematizing reductions on ground terms. An extension of the method is given, where the noetherian induction is strengthened by a structural induction. A variant is also proposed, to characterize terminating subset of the ground term algebra, for non-innermost terminating system. Finally, the method is adapted in a natural way to outermost termination.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 002F05
- to stream Crin, to step Curation: 002F05
- to stream Crin, to step Checkpoint: 001575
- to stream Main, to step Merge: 009480
- to stream Main, to step Curation: 008F59
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="389">Induction for innermost and outermost ground termination</title></titleStmt><publicationStmt><idno type="RBID">CRIN:gnaedig01a</idno><date when="2001" year="2001">2001</date><idno type="wicri:Area/Crin/Corpus">002F05</idno><idno type="wicri:Area/Crin/Curation">002F05</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002F05</idno><idno type="wicri:Area/Crin/Checkpoint">001575</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001575</idno><idno type="wicri:Area/Main/Merge">009480</idno><idno type="wicri:Area/Main/Curation">008F59</idno><idno type="wicri:Area/Main/Exploration">008F59</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Induction for innermost and outermost ground termination</title><author><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></author><author><name sortKey="Fissore, Olivier" sort="Fissore, Olivier" uniqKey="Fissore O" first="Olivier" last="Fissore">Olivier Fissore</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>induction</term><term>innermost</term><term>narrowing</term><term>ordering constraints</term><term>outermost</term><term>rewriting</term><term>rule based languages</term><term>strategy</term><term>termination</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="5217">We propose an original approach to prove termination of innermost rewriting on ground term algebras, based on induction, abstraction and narrowing. Our method applies in particular to non-terminating systems which are innermost terminating, and to systems that do not innermost terminate on the free term algebra but do on the ground term one. The induction relation, an F-stable ordering having the subterm property, is not given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints. The method is based on an abstraction mechanism, introducing variables that represent ground terms in normal form, and on narrowing, schematizing reductions on ground terms. An extension of the method is given, where the noetherian induction is strengthened by a structural induction. A variant is also proposed, to characterize terminating subset of the ground term algebra, for non-innermost terminating system. Finally, the method is adapted in a natural way to outermost termination.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Fissore, Olivier" sort="Fissore, Olivier" uniqKey="Fissore O" first="Olivier" last="Fissore">Olivier Fissore</name><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008F59 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008F59 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:gnaedig01a
|texte= Induction for innermost and outermost ground termination
}}
| This area was generated with Dilib version V0.6.33. |  |