Exercise 1.7
Consider the λ-term $U$ of Exercise 1.4, again.
(a) Mark all redexes in $U$.
(b) Find all reduction paths from $U$ and the β-normal form of $U$ (if it exists).
$$U := (\lambda z. zxz)((\lambda y. xy)x)$$
(a) There are two redexes, corresponding to the two $\lambda$'s which must also have an argument.
- The full term itself, $(\lambda z. zxz)((\lambda y. xy)x)$
- The sub term, $(\lambda y. x y) x$.
(b) There are two paths, each resulting from a different order of resolving the redexes:
Path 1:
$$\begin{align}(\lambda z. zxz)((\lambda y. xy)x) & \to (\lambda z. zxz)(xx) \\ \\ & \to ((xx)x(xx)) \\ \\ & \to (x x x) (x x) \end{align}$$
Path 2:
$$\begin{align}(\lambda z. zxz)((\lambda y. xy)x) & \to (((\lambda y. xy)x)) x (((\lambda y. xy)x)) \\ \\ & \to (( x x)) x ((x x)) \\ \\ & \to (x x x) (x x) \end{align}$$
The β-normal form is $(xxx)(xx)$ and both paths leads to it.
You can use this online lambda calculator to check your own calculations (link).
Exercise 1.8
Show that the terms $(λx. xx) y$ and $(λxy. yx) x \; x$ are not β-convertible.
To show the two terms are not β-convertible, we need to show the β-normal-form for both are not equivalent.
Let's reduce the first term:
$$\begin{align} (\lambda x . x x) y & \to y \; y \end{align} $$
And the second term:
$$\begin{align} (\lambda x y . y x) x x & = (\lambda x . (\lambda y . y x)) x \; x \\ \\ & \to (\lambda y . y x ) x \\ \\ & \to x \; x \end{align} $$
So the two terms reduce to different β-normal-forms and so are not β-convertible.
