[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #10

Originator: J. R. Kennaway
Date: April 1991

Summary: Has any full, finitely-generated and Church-Rosser term-rewriting system (or system with bound variables) a recursive, one-step, normalizing reduction strategy?

Let a term-rewriting system (or more generally, a system with bound variables [Klo92]) have the following properties: it is “finitely generated” (has finitely many function symbols and rules), it is “full” (its terms are all that can be formed from the function symbols), and it is Church-Rosser. Does it follow that it has a recursive, one-step, normalizing reduction strategy? (There are counterexamples if any of the three conditions is dropped.) Kennaway [Ken89] showed that for “weakly” orthogonal systems the answer is yes. So, any counterexample must come from the murky world of non-orthogonal systems. See also [AM96].

References

[AM96]

Sergio Antoy and Aart Middeldorp. A sequential reduction strategy. Theoretical Computer Science, 165(1):75–95, 1996.

[Ken89]

J. R. Kennaway. Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic, 43:31–56, 1989.

[Klo92]

Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]