Problem 5 - Lambda Calculus

For a $\lambda$-expression $M$ containing no $\lambda$-abstraction and for a variable $x$, $\lambda$-expression $M_x$ is defined as follows:

$$x_x = I$$

$$y_x = Ky \; \hbox{($x$ and $y$ are distinct variables)}$$

$$(MN)_x = S M_x N_x$$

where $I = \lambda x.x$, $K = \lambda x.\lambda y.x$, $S = \lambda f.\lambda g.\lambda x.fx(gx)$. Show that $\lambda x.M$ and $M_x$ are $\beta$-convertible to each other.

We want to show that $M_x$ and $\lambda x.M$ are $\beta$-convertible to each other, i.e. $M_x$ (resp. $\lambda x.M$) can be obtained from $\lambda x.M$ (resp. $M_x$) by a serie of $\beta$-contractions and reversed $\beta$-contractions and changes of bound variables. We recall that a $\beta$-contraction of $(\lambda x.M)N$ is the application of the substitution $[N/x]M$.

$M$ cannot be a $\lambda$-abstraction. We will demonstrate the property of $\beta$-equality by induction on the lenght of $M$. First, assume that $M$ is a variable. It can be $x$, so that:

$$M_x = x_x = I = \lambda x.x = \lambda x.M$$

and the property is true for $M=x$ ($\beta$-equality with a list of empty $\beta$-contractions). Or $M$ can be a variable $y\neq x$, so that:

$$M_x = y_x = K y = (\lambda x.\lambda y_1.x)y \triangleright_{1\beta} \lambda y_1.y \equiv_\alpha \lambda x.y = \lambda x.M$$

and the property is true for any variable (thanks to a $\beta$-contraction and a change of bound variables).

Now, let us assume that the property is true for any $\lambda$-expression containing no $\lambda$-abstraction of length $<k$. Let $M$ be a $\lambda$-expression containing no $\lambda$-abstraction of length $k$. As $lgh(M)>1$, $M$ is not a variable and can be written has an application. Let us assume that $M=PQ$.

$$M_x = (PQ)_x = SP_xQ_x = (\lambda f.\lambda g. \lambda x.fx(gx))P_xQ_x \triangleright_{1\beta} \lambda x.P_x x (Q_x x)$$

We now use the assumption of the induction to write:

$$M_x \triangleright_{1\beta} \lambda x.(\lambda x.P)x((\lambda x.Q)x)$$

We have the following change of bound variables $(\lambda x.P)x \equiv_\alpha P$ and thus:

$$M_x \equiv_\alpha \lambda x.PQ = \lambda x.M$$

And the property has been proved.