Sequentiality in orthogonal term rewriting systems (Q1186735)

Term rewriting systems can be used for computing with equations. A term rewriting system is called orthogonal if it is (1) left-linear (no variable appears more than once in a left hand side of a rule) and (2) non-overlapping (no left-hand side of a rule is unifyable with a non- variable subterm of a left-hand side of a rule). This property is very useful since it guaranties confluence: no term can be rewritten to two different normal forms. But, there may be a term which can be rewritten to a normal form and at the same time it is the starting point of an infinite rewriting sequence. So it is of great importance to develop a rewriting strategy that avoids infinite computations whenever possible. Huet and Lévy have defined a subclass of orthogonal term rewriting systems, called strongly sequential rewriting systems, that allow for such a strategy: For any term \(t\) one can compute a `needed redex', that is a subterm \(t_ 0\) of \(t\) that has to be rewritten in any rewriting sequence starting with \(t\) and ending in the normal form of \(t\). Now, the rewriting strategy is just to rewrite in each step a needed redex. Huet and Lévy have proved that it is decidable whether an orthogonal rewriting system is strongly sequential, but their proof is highly complex and in essence it is a correctness proof of some algorithm. The aim of the paper is to analyse the notation of a strongly sequential term rewriting system and so to arrive at a conceptually much simpler proof of the decidability result. The resulting decision algorithm is of high computational complexity, so a second algorithm is given that has a computational complexity comparable to the algorithm of Huet and Lévy. It is also proved that strong sequentiality in a modular property, i.e. the disjoint union of two strongly sequential term rewriting systems is again strongly sequential.