On Rewriting with Divergent Rewrite Systems

Monica Nesi

(joint work with B. Intrigila and P. Inverardi)

University of L'Aquila

Abstract: This talk presents a rewriting strategy to deal with divergence of completion procedures. Given a rewrite system R, whose completion with respect to a reduction ordering > diverges into an infinite rewrite system R', a strategy can be defined to simulate the application of the infinitely many rewrite rules derived from critical pairs, without attempting any completion. This is done by applying a subset E of the rules in R also as expansion rules, provided that E is ``cp-complete'', namely reduction in R together with expansion in E is able to compute all normal forms with respect to the infinite rewrite system R'. The strategy has been implemented in the HOL proof assistant. Finally, we consider the undecidability of the cp-completeness of a given set of expansion rules and how to characterize classes of rewrite systems for which the decision problem is decidable.

Back to schedule.

Nicolas Magaud

Last modified: Wed Feb 14 13:39:48 MET 2001