Exercise 1.1
Apply Notation 1.3.10 on the following λ-terms. So, remove parentheses and combine λ-abstractions:
(a) $(λx. (((xz)y)(xx)))$
(b) $((λx. (λy. (λz. (z((xy)z)))))(λu. u))$
(a) We can remove the outermost brackets. Inside the body we can simplify $(xz)y$ to $(xzy)$ due to right-associativity. We can't reduce $(xzy)(xx)$ to $(xzyxx)$.
So the solution is
$$\lambda x. xzy(xx)$$
Note, application takes precedence over abstraction, so we don't need to write $\lambda x. (xzy(xx))$.
(b) There are quite a few levels of parentheses here. Let's consider two of the inner-most expressions.
The $(z((xy)z))$ is equivalent to $z(xyz)$ by left-associativity of application.
The nested lambdas $(\lambda x (\lambda y (\lambda z . M)))$ simplify to $\lambda xyz . M$.
This gives us
$$\lambda xyz . z(xyz)(\lambda u . u)$$
For this exercise we don't apply $\lambda xyz . z(xyz)$ to $(\lambda u . u)$.
Exercise 1.2
Find out for each of the following λ-terms whether it is α-equivalent, or not, to λx. x(λx. x):
(a) λy. y(λx. x),
(b) λy. y(λx. y),
(c) λy. y(λy. x).
Here is a nice, less text-booky, explanation of α-equivalence (link).
(a) $\lambda y . y (\lambda x . x)$ is α-equivalent. Only the bound variables have been renamed. That is, the $x$ in the second part $(\lambda x . x)$ have not been renamed because they are not free variables in $x(\lambda x. x)$.
Referring to Definition 1.5.1
- Condition 1: renaming $x$ to $y$ is ok because $y$ is not a free variable in $x(\lambda x. x)$.
- Condition 2: renaming $x$ to $y$ is ok because $y$ is not a binding variable in $x(\lambda x. x)$.
(b) $\lambda y . y (\lambda x . y)$ is not α-equivalent. The term $(\lambda x . y)$ is not the identity function in the original term.
Referring to Definition 1.5.1
- Condition 1: renaming the last $x$ to $y$ is wrong because it is not a free variable in $x(\lambda x. x)$.
(c) $\lambda y . y (\lambda y . x)$ is not α-equivalent. The term $(\lambda y . x)$ is not the identity function in the original term.
- In this case $\lambda y. y(\lambda y. x)$ can't be reached from the original term by α-conversion.
Exercise 1.3
Use the definition of $=_α$ to prove that $λx. x(λz. y) =_α λz. z(λz. y)$, in spite of the fact that $z$ occurs as a binding variable in $x(λz. y)$.
Let's start with the destination $\lambda z.z(\lambda z. y)$ and rewrite $z$ to $x$ to give $\lambda x .x (\lambda z . y)$. Note we're only rewriting free variables in the body $z(\lambda z. y)$ so the second $z$ doesn't change. The two conditions are met, $x$ is not a free variable in the body, and neither is it a binding variable.
Now we use the symmetry property (3b) of Definition 1.5.2 to say that
$$\lambda z.z(\lambda z. y) =_{\alpha} \lambda x .x (\lambda z . y)$$
implies
$$\lambda x.x(\lambda z. y) =_{\alpha} \lambda z .z (\lambda z . y)$$
What is interesting in this exercise is that we can rewrite a lambda term $A$ to the α-equivalent $B$, but we can't necessary rewrite $B$ to $A$.
