[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |