Skip to Main content Skip to Navigation
Reports

Innermost sufficient completeness

Isabelle Gnaedig 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In the context of a general approach of studying properties of rewriting under strategies, we focus in this paper on the property of completeness of function definitions. We propose a procedure proving sufficient completeness of rewriting in the specific case of the innermost strategy, under the only assumption that the rewriting system innermost terminates on ground terms. It relies on an inductive proof that every ground term rewrites into a constructor term. The innermost rewriting relation on ground terms is simulated through an abstraction mechanism and narrowing. The inductive hypothesis allows assuming that terms smaller than the starting terms for an induction ordering rewrite into a constructor term. The existence of the induction ordering is checked during the proof process, by ensuring satisfiability of ordering constraints. An extension of this procedure is also proposed, to establish in the same time sufficient completeness and the needed innermost termination property.
Complete list of metadatas

https://hal.inria.fr/inria-00099765
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:41:03 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM

Identifiers

  • HAL Id : inria-00099765, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Innermost sufficient completeness. [Intern report] A03-R-131 || gnaedig03a, 2003, 22 p. ⟨inria-00099765⟩

Share

Metrics

Record views

102