Termination of rewriting strategies : a generic approach
Identifieur interne : 006152 ( Main/Merge ); précédent : 006151; suivant : 006153Termination of rewriting strategies : a generic approach
Auteurs : Isabelle Gnaedig ; Hélène KirchnerSource :
English descriptors
- KwdEn :
Abstract
We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modeled by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. Abstraction constraints can be used to control the narrowing mechanism, well known to easily diverge. The generic method is then instantiated for the innermost, outermost and local strategies.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 004088
- to stream Crin, to step Curation: 004088
- to stream Crin, to step Checkpoint: 000377
Links to Exploration step
CRIN:gnaedig05aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="292">Termination of rewriting strategies : a generic approach</title></titleStmt><publicationStmt><idno type="RBID">CRIN:gnaedig05a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004088</idno><idno type="wicri:Area/Crin/Curation">004088</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004088</idno><idno type="wicri:Area/Crin/Checkpoint">000377</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000377</idno><idno type="wicri:Area/Main/Merge">006152</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Termination of rewriting strategies : a generic approach</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></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>abstraction</term><term>induction</term><term>innermost strategy</term><term>local strategy</term><term>narrowing</term><term>outermost strategy</term><term>rewrite system</term><term>rewriting strategy</term><term>termination proof</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3165">We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modeled by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. Abstraction constraints can be used to control the narrowing mechanism, well known to easily diverge. The generic method is then instantiated for the innermost, outermost and local strategies.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006152 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 006152 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:gnaedig05a
|texte= Termination of rewriting strategies : a generic approach
}}
| This area was generated with Dilib version V0.6.33. |  |