3

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

Ziqi Fan
  • 1,816

1 Answers1

2

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.

cinch
  • 1,648
  • 1
  • 4
  • 12