[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.

Remark

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

References

[Man93]

Ken Mano, September 1993. Personal communication.

[Oos92]

V. van Oostrom. Confluence by decreasing diagrams. IR 298, Vrije Universiteit, Amsterdam, The Netherlands, August 1992. To appear in Theoretical Computer Science.

[vO94]

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]