Induction for innermost and outermost ground termination

Isabelle Gnaedig 1 Hélène Kirchner 1 Olivier Fissore 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Rapport
[Intern report] A01-R-178 || gnaedig01a, 2001, 38 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00100696
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:49:43
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100696, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner, Olivier Fissore. Induction for innermost and outermost ground termination. [Intern report] A01-R-178 || gnaedig01a, 2001, 38 p. 〈inria-00100696〉

Partager

Métriques

Consultations de la notice

208