← All problems
Unverified

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

The source page states the original problem together with its recorded qualifications and progress updates as follows.

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 [Oostrom, 1993] 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.

Recorded progress.

It is now known to hold for countable systems [Oostrom, 1993].

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu