Induction for termination - Archive ouverte HAL Access content directly
Reports Year : 2000

Induction for termination

(1) , (1) , (1)
1
Isabelle Gnaedig
Hélène Kirchner
Olivier Fissore
• Function : Author
• PersonId : 835374

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. 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. A variant of the method is given, where the induction ordering on terms is replaced by a hierarchy ordering on the signature. An extension is also proposed to characterize terminating subsets of the term algebra, for non innermost terminating systems. Rule-based descriptions of the three techniques are presented, their correctness is established and examples are given.

Dates and versions

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

Identifiers

• HAL Id : inria-00099315 , version 1

Cite

Isabelle Gnaedig, Hélène Kirchner, Olivier Fissore. Induction for termination. [Intern report] A00-R-357 || gnaedig00a, 2000, pp.22. ⟨inria-00099315⟩

76 View