Bounded, Strongly Sequential and Forward-Branching Term Rewriting Systems

The class of Strongly Sequential Term Rewriting Systems (SS) was defined in [Huet&Lévy (1979)]. [Strandh (1989)] defined the class of bounded TRSs (B). As a subset of B, Strandh defined the class of forward-branching TRSs (FB); FB strictly contains the class of Strongly-Left Sequential TRSs (SLS) defined by [Hoffmann & OʹDonnell (1982)] for their Equational Programming System. For SLS, Hoffmann and OʹDonnell found efficient algorithms to compute normal forms. Strandh showed that as efficient algorithms exist for FB. B is defined in terms of the existence of a deterministic pattern matching automaton called an index tree and FB in terms of the existence of a forward-branching index tree. Two open problems set by Strandh were to characteriseFB in a simpler way and to find an algorithm to build a forward-branching index tree. This article contains three main parts. In the first part, we introduce the Strongly Sequential class and the Bounded class and we check that B = SS. This insures that FB SS and relates Strandhʹs work to all the works initiated by [Huet&Lévy (1979)]. The second part contains the main result of this article: we give a very simple characterisation of FB. Our proof of the characterisation is constructive; itʹs then straightforward to extend it to an algorithm that builds a forward-branching index tree. In the third part we give the algorithm and show that it runs in quadratic time.