[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #56

Originator: V. van Oostrom
Date: June 1993

Summary: Does the Church-Rosser property of abstract reduction systems imply decreasing Church-Rosser?

An abstract reduction system is “decreasing Church-Rosser”, if there exists a labelling of the reduction relation by a well-founded set of labels, such that all local divergences can be completed to form a “decreasing diagram” (see [Oos92] for precise definitions). Does the Church-Rosser property imply decreasing Church-Rosser? That is, is it always possible to localize the Church-Rosser property? This is known to be the case for (weakly) normalizing and finite systems.


It is now known to hold for countable systems [Man93],[vO94, Cor. 2.3.30].


Ken Mano, September 1993. Personal communication.
V. van Oostrom. Confluence by decreasing diagrams. IR 298, Vrije Universiteit, Amsterdam, The Netherlands, August 1992. To appear in Theoretical Computer Science.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, March 1994.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]