SEQUENTIALITY IN ORTHOGONAL TERM REWRITING-SYSTEMS

For orthogonal term rewriting systems Q. Huet and J.-J. Lévy have introduced the property of ‘strong sequentiality’. A strongly sequential orthogonal term rewriting system admits an efficiently computable normalizing one-step reduction strategy. As shown by Huet and Lévy, strong sequentiality is a decidable property. In this paper we present an alternative analysis of strongly sequential term rewriting systems, leading to two simplified proofs of the decidability of this property. We also compare some related notions of sequentiality that recently have been proposed. © 1991, Academic Press Limited. All rights reserved.