Strongly sequential and inductively sequential term rewriting systems

Author

Michael Hanus, Salvador Lucas, and A. Middeldorp

Abstract

The concept of definitional tree by Antoy serves to introduce control information into the bare set of rules of a constructor-based term rewriting system (TRS). TRSs whose rules can be arranged into a definitional tree are called inductively sequential. By relying on the existence of such a definitional tree, an optimal rewriting strategy, the outermost-needed strategy is defined. Optimality was proved w.r.t. the Huet and Lévy's theory of neededness. In this paper, we prove that strongly sequential and inductively sequential constructor-based TRSs coincide. We also show that outermost-needed rewriting only reduces strongly needed redexes.

Keywords

definitional trees, neededness, strong sequentiality, term rewriting, declarative programming.