Exercise 1.4
Consider the following λ-term:
$$U := (λz. zxz)((λy. xy)x)$$
(a) Give a list of all subterms of U.
(b) Draw the tree representation of U.
(c) Find the set of all free variables of U by a calculation, as in Examples 1.4.2.
(d) Find out which of the following λ-terms are α-equivalent to U and give a motivation why; also check which of them satisfies the Barendregt convention:
(λy. yxy)((λz. xz)x),
(λx. xyx)((λz. yz)y),
(λy. yxy)((λy. xy)x),
(λv. (vx)v)((λu. uv)x).
(a) We find all the sub terms by breaking the bigger ones iteratively. Note the given λ-term is also a sub-term (but not a proper subterm).
$(λz. zxz)((λy. xy)x)$
$(λz. zxz)$, $(zxz)$, $z$ twice, and $x$
$((λy. xy)x)$, $x$, $(λy.xy)$, $x$ again, and $y$
So $z$ occurs twice, $x$ three times, $y$ once in the multi-set of subterms.
(b) Click to enlarge the diagram.
As a check, you can try this online λ-term renderer (link).
(c) Finding the free variables by calculation means applying Definition 1.4.1.
$$\begin{align}FV ( (λz. zxz)((λy. xy)x) ) &= FV (λz. zxz) \cup FV ((λy. xy)x) \\ \\ & = ( FV (zxz) \setminus \{z\} ) \cup ( FV (\lambda y . xy) \cup FV (x) ) \\ \\ &= \{x\} \cup ( FV (xy) \setminus \{y\} ) \cup \{x\} \\ \\ &= \{x\} \cup ( \{x\} ) \cup \{x\} \\ \\ &= \{x\} \end{align}$$
(d) If we render diagrams for all of the terms, we can see that they are all equivalent up to name changes, except the last one $(λv. (vx)v)((λu. uv)x)$ which is structurally different. Let's consider each one in turn.
- Starting with $U := (λz. zxz)((λy. xy)x)$ we can rename $z \to y$ in the first part to give $(λy. yxy)((λy. xy)x)$, and then rename $y \to z$ in the second part to give $(λy. yxy)((λz. xz)x)$. We can do this based on compatibility in Definition 1.5.2 where if $M =_{\alpha}N$ then $M L=_{\alpha}N L$ and $L M =_{\alpha}L N$.
- This is a simple cycling of variable names $x \to y \to z \to x$. But let's see what steps we'd take to achieve this. Starting with $U := (λz. zxz)((λy. xy)x)$ we rename $z \to w$ to give $(λw. wxw)((λy. xy)x)$. We then rename $y \to z$ to give $(λw. wxw)((λz. xz)x)$. Then we rename $x \to y$ to give $(λw. wyw)((λz. yz)y)$. Finally we rename $w \to x$ to give the desired $(λx. xyx)((λz. yz)y)$.
- This is simpler because only the first part changes. Starting with $U := (λz. zxz)((λy. xy)x)$ we rename $z \to y$ to give $(λy. yxy)((λy. xy)x)$. We again justify this using the compatibility in Definition 1.5.2. The second part is insulated from renaming in the first part.
- Noting that application is left-associative, the first part $(λv. (vx)v)$ is $(λv. vxv)$. This means first parts are α-alpha equivalent by a simple rewriting $z \to v$. Let's compare the second parts $((λy. xy)x)$ and $((λu. uv)x)$. These can never be α-equivalent because $(λy. xy)$ is semantically different to $(λu. uv)$. The former applies $x$ to the argument, the latter applies the argument to $v$.
