4
$\begingroup$

Prerequisites

Consider the $\lambda$-calculus where terms are equivalence classes over the $\alpha$-equality.

We define $\to_\beta$-reduction in the usual way, i.e. the least congruent relation on $\lambda$-terms (hence congruent with application and abstraction) satisfying

$$(\lambda x. M) N \to_\beta M[x := N]$$

Following this, $=_\beta$ is defined as the least equivalence relation containing $\to_\beta$.

Question

Now, probably an easy one:

Prove that $$\lambda x .x =_\beta x$$ doesn't hold.

Comments

It is clear to me that the above equation does not hold. On both sides are normal forms which differ. I can even prove it using a lot of machinery: Church-Rosser, parallel reduction relation and an order in beta-reduction sequences. But it seems as if this should be an easy one and I'm just overlooking something. Insofar I'm looking for ideas for a formal proof.

Exercise is based on one from the book "Lectures on the Curry-Howard Isomorphism" by Sørensen and Urzyczyn.

$\endgroup$
  • $\begingroup$ I wonder if there is some way to formalize "the right depends on a free variable, the left does not, and beta reduction preserves dependency on free variables". It would not be correct to say that beta reduction preserves the existence of free variables though. $\endgroup$ – DanielV Aug 20 '16 at 14:12
5
$\begingroup$

The Church-Rosser property is all you need: $\lambda x.x$ and $x$ are both $\rightarrow_{\beta}$-normal forms so they can only be $\rightarrow_{\beta}$-equivalent if they are $\alpha$-equivalent, which they are not.

To explain this in more detail, let me write $a \rightarrow b$ to mean that $b$ can be obtained from $a$ by repeated $\beta$-reductions. The Church-Rosser property says that if $a \rightarrow b$ and $a \rightarrow c$ then there is a term $d$ such that $b \rightarrow d$ and $c \rightarrow d$. If $\lambda x.x$ and $x$ were $\rightarrow_{\beta}$-equivalent, then there would be a sequence of terms $t_1, \ldots, t_n$ with $t_1 \equiv \lambda x.x$ and $t_n \equiv x$ such that for each $i$, $1 \le i < m$ either $t_i\rightarrow t_{i+1}$ or $t_{i+1}\rightarrow t_i$. Church-Rosser lets you transform any triple of the form $t_{i-1} \leftarrow t_{i} \rightarrow t_{i+1}$ in this sequence into a triple of the form $t_{i-1} \rightarrow t_{i}' \leftarrow t_{i+1}$. Repeatedly applying this transformation will result in a sequence $t_1', \dots, t_n'$ with $t_1' \equiv \lambda x.x$ and $t_n' \equiv x$, such that $t_1' \rightarrow t_2'$ and $t_n' \rightarrow t_{n-1}'$. But $t_1'$ and $t_n'$ are both $\rightarrow_{\beta}$-normal forms, so this is impossible, unless $t_1' = t_2' = \ldots = t_{n-1}' = t_n'$, which is not the case if $t_1' \equiv \lambda x.x$ and $t_n' \equiv x$.

$\endgroup$

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.