# Opposite Direction of Church-Rosser Theorem

lambda-calculus

The Church-Rosser theorem states that if $$a \twoheadrightarrow b$$ and $$a \twoheadrightarrow c$$, then there exists a Lambda expression $$d$$ such that $$b \twoheadrightarrow d$$ and $$c \twoheadrightarrow d$$, where $$\twoheadrightarrow$$ denotes a sequence of $$\rm{\beta}$$ reductions. Intuitively, the theorem indicates that if two Lambda expressions have the same source, then they have the same destination. I am wondering if the opposite direction of the theorem holds: if two Lambda expressions have the same destination, then they have the same source.

Formally, the hypothesis can be written as follows: if $$b \twoheadrightarrow d$$ and $$c \twoheadrightarrow d$$, there exists a Lambda expression $$a$$ such that $$a \twoheadrightarrow b$$ and $$a \twoheadrightarrow c$$.

I'm afraid there's no such ideal symmetric confluence property in untyped lambda calculus. Consider $$b:=(λyx.x)M_1↠λx.x, c:=(λyx.x)M_2↠λx.x$$ where $$M_1, M_2$$ are distinct terms. Clearly terms $$b,c$$ here cannot be alternative rewritten terms from a common term since there's no relation between the arbitrary distinct terms $$M_1, M_2$$.
Another way is to think of Church numerals as representing natural numbers, then obviously any number may have infinitely many ways to express, such as $$20=19+1 (Suc)=21-1 (Pred)=...$$, thus one cannot find a fixed common ancestor term within any finite sequence.