Inductively sequential term-graph rewrite systems

Abstract

Definitional trees have been introduced by Sergio Antoy in order to design an efficient term rewrite strategy which computes needed outermost redexes. In this paper, we consider the use of definitional trees in the context of term-graph rewriting. We show that, unlike the case of term rewrite systems, the strategies induced by definitional trees do not always compute needed redexes, in presence of term-graph rewrite systems. We then define a new class called inductively sequential term-graph rewrite systems (istGRS) for which needed redexes are still provided by definitional trees. Systems in this class are not confluent in general. We give additional syntactic criteria over istGRS's which ensure the confluence property with respect to the set of admissible term-graphs. © 2008 Springer-Verlag Berlin Heidelberg.