Church-Rosser Property

Definition

An abstract reduction system has the Church-Rosser property if, whenever $a{\leftrightarrow }^{\ast }b$, there exists $c$ such that $a{\to }^{\ast }c$ and $b{\to }^{\ast }c$.

Thus inter-convertible objects can always be reduced to a common descendant.

Relation to Confluence

For abstract reduction systems, the Church-Rosser property is equivalent to confluence. Some authors use the two names interchangeably, while others reserve “Church-Rosser” for the formulation in terms of convertibility.

In lambda calculus, the statement that beta reduction has this property is the classical Church-Rosser theorem.

Related Concepts

Abstract Reduction System
Confluence
Normal Form
Lambda Calculus

References

baader1998-term-rewriting