Induction for weak termination - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2002

Induction for weak termination

Résumé

We propose an original approach to prove weak termination of innermost rewriting on ground term algebras, based on induction, abstraction and narrowing. The abstraction mechanism schematizes the application of the induction hypothesis on terms, and narrowing schematizes reductions. 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. An extension of the method is given, where the information given by abstraction are memorized and used. Our method is more specific than methods proving strong termination of rewriting under strategies, which also give a weak termination proof for the standard rewriting. Indeed, ours can in addition handle TRSs that are not strongly innermost terminating.
Fichier non déposé

Dates et versions

inria-00101056 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00101056 , version 1

Citer

Isabelle Gnaedig, Olivier Fissore, Hélène Kirchner. Induction for weak termination. [Intern report] A02-R-111 || gnaedig02a, 2002, 23 p. ⟨inria-00101056⟩
101 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More