Termination Proofs by Context-Dependent Interpretations
Identifieur interne : 003049 ( Istex/Curation ); précédent : 003048; suivant : 003050Termination Proofs by Context-Dependent Interpretations
Auteurs : Dieter Hofbauer [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated. Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.
Url:
DOI: 10.1007/3-540-45127-7_10
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003088
Links to Exploration step
ISTEX:CDC40FAF4A3DEAFD5C024DF3C31F3A7AAF18CF3ALe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Termination Proofs by Context-Dependent Interpretations</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><affiliation wicri:level="1"><mods:affiliation>Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: dieter@theory.informatik.uni-kassel.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:CDC40FAF4A3DEAFD5C024DF3C31F3A7AAF18CF3A</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45127-7_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-2G0RTB9K-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003088</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003088</idno><idno type="wicri:Area/Istex/Curation">003049</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Termination Proofs by Context-Dependent Interpretations</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><affiliation wicri:level="1"><mods:affiliation>Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: dieter@theory.informatik.uni-kassel.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</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: Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated. Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.</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 003049 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 003049 | 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:CDC40FAF4A3DEAFD5C024DF3C31F3A7AAF18CF3A
|texte= Termination Proofs by Context-Dependent Interpretations
}}
| This area was generated with Dilib version V0.6.33. |  |