Abstract

For orthogonal term rewriting systems G. 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 Levy, 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.

BibTeX Entry

@article{KM-JSC91,
 author    = "Jan Willem Klop and Aart Middeldorp",
 title     = "Sequentiality in Orthogonal Term Rewriting Systems",
 journal   = "Journal of Symbolic Computation",
 volume    = 12,
 number    = 2,
 pages     = "161--195",
 year      = 1991,
 doi       = "10.1016/S0747-7171(08)80124-1"
}