Proving weak properties of rewriting
Résumé
In rule-based programming, properties of programs are in general considered in their strong acceptance i.e., on every computation branch. But in practice, they may hold in their weak acceptance only: on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. Very few results exist to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, nin a unified framework allowing to develop inductive proofs of the considered properties. Proof trees are developed, which simulate rewriting trees by narrowing and an abstraction mechanism exploiting the induction hypothesis. Our technique is constructive in the sense that proof trees can be used to compute an evaluated form of any given data: the good computation branch is developed without to use a costly breadth-first strategy.