An ordinal calculus for proving termination in term rewriting
Identifieur interne : 000C09 ( Istex/Curation ); précédent : 000C08; suivant : 000C10An ordinal calculus for proving termination in term rewriting
Auteurs : E. A. Cichon [France] ; H. Touzet [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In this article, we are concerned with the proofs of termination of rewrite systems by the method of interpretations. We propose a modified approach to subrecursive hierarchies of functions by means of a syntactical approach to ordinal recursion. Our method appears to be appropriate for finding interpretations in a systematic way. We provide several examples of applications. It is shown that three usual recursion schemas over the natural numbers, recursion with parameter substitution, simple nested recursion and unnested multiple recursion can be encoded directly in our system. As the corresponding ordinal terms are primitive recursively closed, we get a concise and intuitive proof for the closure of the class of primitive recursive functions under these schemes.
Url:
DOI: 10.1007/3-540-61064-2_40
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000C16
Links to Exploration step
ISTEX:3387C3AF21E63CF6AD6F982E7162AFC5A783CE92Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">An ordinal calculus for proving termination in term rewriting</title><author><name sortKey="Cichon, E A" sort="Cichon, E A" uniqKey="Cichon E" first="E. A." last="Cichon">E. A. Cichon</name><affiliation><mods:affiliation>INRIA-Lorraine - CNRS-CRIN, BP 101, F-54602, Villers-lès-Nancy</mods:affiliation><wicri:noCountry code="subField">Villers-lès-Nancy</wicri:noCountry></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: cichon@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Touzet, H" sort="Touzet, H" uniqKey="Touzet H" first="H." last="Touzet">H. Touzet</name><affiliation><mods:affiliation>INRIA-Lorraine - CNRS-CRIN, BP 101, F-54602, Villers-lès-Nancy</mods:affiliation><wicri:noCountry code="subField">Villers-lès-Nancy</wicri:noCountry></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: touzet@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:3387C3AF21E63CF6AD6F982E7162AFC5A783CE92</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1007/3-540-61064-2_40</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-KVXXTFR0-L/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000C16</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000C16</idno><idno type="wicri:Area/Istex/Curation">000C09</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">An ordinal calculus for proving termination in term rewriting</title><author><name sortKey="Cichon, E A" sort="Cichon, E A" uniqKey="Cichon E" first="E. A." last="Cichon">E. A. Cichon</name><affiliation><mods:affiliation>INRIA-Lorraine - CNRS-CRIN, BP 101, F-54602, Villers-lès-Nancy</mods:affiliation></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: cichon@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Touzet, H" sort="Touzet, H" uniqKey="Touzet H" first="H." last="Touzet">H. Touzet</name><affiliation><mods:affiliation>INRIA-Lorraine - CNRS-CRIN, BP 101, F-54602, Villers-lès-Nancy</mods:affiliation></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: touzet@loria.fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this article, we are concerned with the proofs of termination of rewrite systems by the method of interpretations. We propose a modified approach to subrecursive hierarchies of functions by means of a syntactical approach to ordinal recursion. Our method appears to be appropriate for finding interpretations in a systematic way. We provide several examples of applications. It is shown that three usual recursion schemas over the natural numbers, recursion with parameter substitution, simple nested recursion and unnested multiple recursion can be encoded directly in our system. As the corresponding ordinal terms are primitive recursively closed, we get a concise and intuitive proof for the closure of the class of primitive recursive functions under these schemes.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C09 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000C09 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:3387C3AF21E63CF6AD6F982E7162AFC5A783CE92
|texte= An ordinal calculus for proving termination in term rewriting
}}
| This area was generated with Dilib version V0.6.33. |  |