According to the "Type Theory and Formal Proof" book, Church-Rosser theorem (confluence) is as follow:

Suppose that for a given term $M$, we have $M \twoheadrightarrow_\beta N_1$ and $M\twoheadrightarrow_\beta N_2$. Then there is a $\lambda-term$ $N_3$ such that $N_1\twoheadrightarrow_\beta N_3$ and $N_2\twoheadrightarrow_\beta N_3$.

But if we take $(\lambda u.v)((\lambda x.xx)(\lambda x.xx))$ expression as $M$, then it will reduce to $v$ if we start with the left sub term and reduces to $(\lambda u.v)((\lambda x.xx)(\lambda x.xx))$ if we start with the right sub term. And they would never reduce to equal terms if we keep reducing the sound one using the right sub term since it would keep converting to itself for ever.

Isn't the above example a refutation of the CR theorem, or I have missed a point somewhere?!


If we keep reducing the right subterm, then yes, we will never get to $v$. But noone says that we are restricted to this decision. The Church-Rosser theorem does not claim that any possible reduction series must lead to $N_3$. Church-Rosser just states that $N_2 \twoheadrightarrow_\beta N_3$, i.e. that there exists some beta reduction series that will lead from $N_2$ to $N_3$. And it is obvious that no matter how many times we just reduce back to $(\lambda u.v)((\lambda x.xx)(\lambda x.xx))$, at any point we can choose our next reduction step to be on the left-hand side, which will immediately get us to $v$. So it is possible to find a reduction series from both $N_1: v$ and $N_2: (\lambda u.v)((\lambda x.xx)(\lambda x.xx))$ to $N_3:v$ -- and that's all the Church-Rosser theorem states.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.