Problem 3 - Lambda Calculus

Answer the following questions on $\lambda$-calculus.

1.

Give a $\lambda$-term ($\lambda$-expression) which has its normal form, but may not reach its normal form depending on the order of reduction.

2.

Give the definition of the Church-Rosser property.

3.

Using the Church-Rosser property, prove that every $\lambda$-term has at most one normal form, where mutually $\alpha$-convertible $\lambda$-terms are regarded as the same.

1.

Let us consider the $\lambda$-expression $P=(\lambda u.v)L$ where $L=(\lambda x.xxy)(\lambda x.xxy)$. If we subsitute $L$ for $u$ in $v$ first then:

$$P=(\lambda u.v) \triangleright_{1\beta} [L/u]v = v$$

where $v$ is a variable (that contains no $\beta$-redexes) and therefore a normal form: the normal form of $P$. But, if we choose a different order for the reduction, then $P$ may not reach its normal form, such as in:

$$P\triangleright_{1\beta} (\lambda u.v)(Ly) \triangleright_{1\beta} (\lambda u.v)(Lyy)\cdots$$

where we have first substituted $(\lambda x.xxy)$ for $x$ in $(\lambda x.xxy)$.

2.

Here is the Church-Rosser theorem for $\beta$-reduction. It says that if $P\triangleright_\beta M$ and $P\triangleright_\beta N$, then there exists $T$ such that $M \triangleright_\beta T$ and $N\triangleright_\beta T$.

3.

Let us suppose that the $\lambda$-expression $P$ has two $\beta$-normal forms $M$ and $N$. We can also write this:

$$P \triangleright_\beta M, \quad P \triangleright_\beta N$$

As $M$ and $N$ are $\beta$-normal forms, they do not contain any redexes. According to the Church-Rosser theorem for $\beta$-reduction, there exists $T$ such that:

$$M \triangleright_\beta T, \quad N \triangleright_\beta T$$

But, as $M$ and $N$ contain no redexes, it means that the $\beta$-reduction has just involved changes of bound variables. In other words, $M$, $T$, and $N$ are $\alpha$-congruent, i.e. mutually $\alpha$-convertible $\lambda$-terms inside these expression are regarded as being the same.