← 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].
