Chapter 1 - Exercise 20

Exercise 20

(a) Construct a λ-term $M$ such that $M=_β λxy. x M y$.

(b) Construct a λ-term $M$ such that $M xyz=_β xyzM$.

(a) To solve this equation, we first define an abstraction of the expression as follows.

$$ L  :=  λz (λxy. x z y)$$

Which means

$$\begin{align} L M  & =_β  λxy. xMy \\ \\ & =_β M \end{align}$$

So if we can find an $M$ such that $LM =_β M$ then this $M$ is a solution to the given equation. The fixed point theorem guarantees such an $M$ exists. 

One way to construct that $M$ is to use the Curry fixed point combinator $Y$, defined as follows.

$$Y := λy. (λx. y(xx))(λx. y(xx))$$

The key property of $Y$ is that 

$$YL =_β L(YL)$$

So if we construct

$$M := YL$$

we can check this $M:= YL$ is a solution

$$\begin{align} M & =_β (YL) \\ \\ & =_β L(YL)  \\ \\ & =_β LM \\ \\ & =_β λxy. xMy \qquad \Box \end{align}$$

(b) We'll start from the expression that will make use of the abstraction $L$ we'll construct.

$$ M =_β LM $$

Using the given $M xyz =_β xyz M$, we have

$$M xyz =_β LM xyz  =_β xyz M$$

This means $L$ must be

$$L := λaxyz . xyza$$

The key property of the Curry fixed point combinator $Y$ is

$$YL =_β L(YL)$$

So if we set

$$ M := YL $$

then we can check this $M:=YL$ is a solution

$$\begin{align} Mxyz & =_β (YL) xyz \\  \\& =_β L(YL) xyz \\ \\  & =_β LM xyz \\ \\ & =_β  xyzM  \qquad \Box  \end{align}$$

Chapter 1 - Exercise 19

Exercise 1.19

We define $U := λzx. x(zzx)$ and $Z := U U$. Prove that $Z$ is a fixed point combinator, i.e. $ZM$ is a fixed point for every λ-term $M$, so $M(ZM) =_β ZM$. Show that even holds: $ZM \to_β M(ZM)$.

Let's start with $ZM$.

$$\begin{align} ZM & = (UU)M \\ \\  & = (λzx.x(zzx))(λba.a(bba))M \\ \\ & \to λx.x((λba.a(bba))(λba.a(bba))x)M  \\ \\ & \to M((λba.a(bba))(λba.a(bba))M) \\ \\ & \to M(ZM) \end{align}$$

We have shown

$$ZM \to_β M(ZM)$$

Which means,

$$M(ZM )=_β ZM$$

That is, Z is a fixed point combinator for any M, because $M(ZM) =_β ZM$.

Chapter 1 - Exercise 18

Exercise 1.18

Let $L$, $M$ and $N$ be λ-terms such that $L=_β M$ and $L \to_β N$. 

Moreover, let $N$ be in β-normal form. Prove that also $M \to_β N$.

$L =_β M$ means one of the following is true

• case 1: $L \to_β M$
• case 2: $M \to_β L$

Let's consider each case in turn.

Case 1: $L \to_β M$ and $L \to_β N$, where $N$ is in β-normal-form, means $M \to_β N$ by the Church-Rosser Theorem.

Case 2:  $M \to_β L$ and $L \to_β N$, means  $M \to_β N$ by the transitivity of β-reduction.

Both cases lead to the conclusion $M \to_β N$

Chapter 1 - Exercise 17

Exercise 1.17

Prove the following: if $MN$ is strongly normalising, then both $M$ and $N$ are strongly normalising.

Strongly normalising means a term has no infinite β-reduction paths starting from it.

The term $MN$ has three possibilities for redexes:

• the full term $MN$
• the first sub-term $M$
• the second sub-term $N$

If there were an infinite reduction path, it would have to start from one of these three possibilities.

Since there is no infinite reduction path, none of the three possibilities has an infinite reduction path. Specifically, terms $M$ and $N$ have no infinite reduction path from them.

Therefore $M$ and $N$ are strongly normalising.

Chapter 1 - Exercise 16

Exercise 1.16

Let $M$ be a λ-term with the following properties:

(1) $M$ has a β-normal form.

(2) There exists a reduction path $M ≡ M_0 →_β M_1 →_β M_2 →_β \ldots $  of infinite length.

(a) Prove that every $M_i$ has a β-normal form.

(b) Give an example of a λ-term with the mentioned two properties and show that it satisfies these properties.

(a) By property (2) every $M_i$ can be β-converted to $M_{i-1}$.  This process can be repeated until $M_0 ≡ M$. By property (1) $M$ has a β-normal form. Therefore there is a path from every $M_i$ to this β-normal form. So every $M_i$ has a β-normal-form.

(b) The example given in 1.9.3 works. Let's define it

$$T :=  (λu. v)Ω = (λu. v)( (λx. xx)(λx. xx) )$$

There are two redexes, the full term $T$ and the sub-term Ω.

The redex $T$ β-reduces to $v$ which is in β-normal-form. So the λ-term has a β-normal-form, property (1).

The second redex Ω has only one option for β-reduction, $Ω \to Ω$. This means there is a reduction path from $T :=  (λu. v)Ω$ of infinity length, $T \to T \to T \to \ldots$. This is property (2).

Chapter 1 - Exercise 15

Exercise 1.15

In Examples 1.9.3 we have seen that neither Ω nor ΔΔ reduces to a β-nf.

Prove that both λ-terms do not have a β-nf, as well.

The term Ω has only one possibility for β-reduction which leads to Ω again. This means there is only one β-reduction path, which is infinite in length. To be clear, no part of this chain has a term which is in β-normal-form.  Therefore Ω does not have a β-nf.

The argument for ΔΔ is the same. The only difference is the detail that each β-reduction step actually increases the number of redexes in the resulting term.

(note:  I think the textbook has a typo as example 1.9.3 shows ΔΔ does not reduce to a β-nf, not Δ, and it doesn't make sense to show a term Δ does not have a β-nf when it is in β-nf already)

Chapter 1 - Exercise 14

Exercise 1.14

The term ‘If x then u else v’ is represented by λx. xuv. Check this by calculating the β-normal forms of $(λx. xuv) \; true$ and $(λx. xuv) \; false$, respectively. (The booleans true and false are defined in Exercise 1.12.)

Let's try this with true.

$$\begin{align} (λx. xuv) \; true & = (λx. xuv) (λab.a) \\ \\ & \to  (λab.a) u v  \\ \\ & \to u \end{align}$$

That worked!

Now let's try it with false.

$$\begin{align} (λx. xuv) \; false & = (λx. xuv) (λab.b) \\ \\ & \to  (λab.b) u v  \\ \\ & \to v \end{align}$$

That also worked!

Chapter 1 - Exercise 13

Exercise 1.13

Consider the λ-terms zero, true and false from Exercises 1.10 and 1.12. 

Let $iszero := λz. z(λx. \; false) \; true$.

(a) Prove that iszero zero reduces to true.

(b) A natural number $n > 0 $ may be represented by the following Church numeral: $λfx. f(f(...(x)))$, with $n$ copies of the variable $f$. 

Prove that iszero n reduces to false for any Church numeral $n$ except 0. (Consequently, iszero represents a test-for-zero.)

(a)

$$\begin{align} iszero \; zero & = (λz. z(λx. \; false) \; true) \; zero \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) (λfx.x) \\ \\ & \to (λfx.x) (λx.  (λab . b))  (λcd.c) \\ \\ & \to (λcd.c)  \\ \\ & = true  \end{align}$$

(b) We'll do this by induction, first showing that iszero 1 reduces to false, then showing iszero $n$ reduces to false implies iszero $n+1$ reduces to false.

The base case $n=1$.

$$\begin{align} iszero \; 1 & = (λz. z(λx. \; false) \; true) \; 1 \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) \; (λfx. f x) \\ \\ & \to (λfx.f x)(λx. (λab . b)) (λcd.c)   \\ \\ & \to (λx. (λab . b)) (λcd.c)  \\ \\ & \to (λab . b) \\ \\ & = false \end{align}$$

The induction step, using inductive hypothesis $iszero \; n \to false$

$$\begin{align} iszero \; (n+1) & = (λz. z(λx. \; false) \; true) \; (n+1) \\ \\ & = (λz. z(λx. (λab . b)) (λcd.c)) \; (λfx. f^{n+1} x) \\ \\ & \to (λfx.f^{n+1} x)(λx. (λab . b)) (λcd.c)   \\ \\ & \to (λx. (λab . b))^{n+1} (λcd.c)  \\ \\ & = (λx. (λab . b)) (λx. (λab . b))^{n} (λcd.c)  \\ \\ & \to  (λx. (λab . b)) \; false  \; \text{ using inductive hypothesis} \\ \\ & =  (λx. (λab . b)) \; (λcd.d) \\ \\ & \to (λab . b) \\ \\ & = false \end{align}$$

So by induction we have shown iszero $n$, for $n > 0$.

Chapter 1 - Exercise 12

Exercise 1.12

We define the λ-terms true and false (the booleans) and not (resembling the logical ¬-operator) by:

$true := λxy. x$ (so it happens that true ≡ K)

$false := λxy. y$ (and false ≡ zero)

$not := λz. z  \; false \; true$

Show that $not(not\; p) =_β p$ for all λ-terms $p$, in each of the following two cases: (a) $p \to_β \; true$ or (b) $p \to _β \; false$.

Let's do some algebra first.

$$\begin{align} not(not \;p) & = (λz.z (false) (true)) ((λy.y (false) (true) ) p)  \\ \\ & = (λz.z (λab.b) (λef.e) )((λy.y (λcd.d) (λgh.g) ) p)   \\ \\ & \to (λz.z (λab.b) (λef.e) )(p (λcd.d) (λgh.g) ) \\ \\ & \to  (p (λcd.d) (λgh.g) ) (λab.b) (λef.e)  \end{align} $$

(a) When $p \to_β \; true$

$$\begin{align} not(not \; true) & \to  ((true) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ &= ((λxy. x) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ & \to ( λcd.d ) (λab.b) (λef.e) \\ \\ & \to (λef.e) \\ \\ & = true  \end{align} $$

(b) When $p \to_β \; false$

$$\begin{align} not(not \; false) & \to  ((false) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ &= ((λxy. y) (λcd.d) (λgh.g) ) (λab.b) (λef.e) \\ \\ & \to ( λgh.g ) (λab.b) (λef.e) \\ \\ & \to (λab.b) \\ \\ & = false  \end{align} $$

So we have shown $not(not\; p) =_β p$ .

Chapter 1 - Exercises 10-11

Exercise 1.10

We define the λ-terms zero, one, two (the first three so-called Church numerals), and the λ-terms add and mult (which mimic addition and multiplication of Church numerals) by:

zero := $λfx. x$

one := $λfx. f x$

two := $λfx. f(f x)$

add := $λmnfx. mf(nf x)$

mult := $λmnfx. m(nf)x$

(a) Show that add one one $\to _β$ two.

(b) Prove that add one one $\neq_β$ mult one zero.

(a) We do this by β-reduction.

$$\begin{align} add\;one\;one&= (λmnfx. mf(nf x)) \; (λgy. g y) \; (λhz. h z) \\ \\ & \to λfx. (λgy. g y)f( (λhz. h z)f x) \\ \\  & \to λfx. (λgy. g y)f( (λhz. h z)f x)  \\ \\  & \to λfx. (λgy. g y)f(f x)  \\ \\  & \to λfx.f(f x)  \\ \\ & = two \end{align}$$

(b) Again we do this by β-reduction, and show the result is not two.

$$\begin{align} mult \; one \; zero &= (λmnfx. m(nf)x) (λgy. g y) (λhz. z) \\ \\ & \to (λfx. (λgy. g y)((λhz. z)f)x) \\ \\ & \to (λfx.((λhz. z)f)x) \\ \\ & \to (λfx.x) \\ \\ & = zero \end{align}$$

The expression reduces to zero, which is correct, and not two.

Exercise 1.11

The successor is the function mapping natural number $n$ to $n+1$. It is represented in λ-calculus by $suc := λmf x. f(mf x)$. Check the following for the Church numerals defined in the previous exercise:

(a) $suc \; zero =_β one$

(b) $suc \; one =_β two$

(a)

$$\begin{align} suc \; zero & = (λmf x. f(mf x)) (λgy. y) \\ \\ & \to (λf x. f( (λgy. y)f x)) \\ \\ & \to  (λf x. f x) \\ \\ & = one \end{align}$$

(b)

$$\begin{align} suc \; one & = (λmf x. f(mf x)) (λgy. fy) \\ \\ & \to (λf x. f((λgy. fy)f x)) \\ \\ & \to  (λf x. f(f x)) \\ \\ & = two \end{align}$$

Chapter 1 - Exercise 9

Exercise 1.9

Consider the following λ-terms (cf. Section 1.12):

$K := λxy. x$

$S := λxyz. xz(yz)$

(a) Check that $K P Q \to _β P$ and $S P QR \to _ β P R(QR)$, for arbitrary λ-terms $P$, $Q$ and $R$.

(b) Let $I := λx. x$. Prove that $S K K \to _β I$.

(c) Let $B := S(K S)K$. Prove that $B U V W \to _β U(V W)$.

(d) Prove that $S S S K K=_β S K K K$.

(a) Let's start with $K P Q$,

$$\begin{align} K P Q & = (\lambda xy . x) P \; Q\\ \\ & = (\lambda x . (\lambda y . x)) P \; Q \\ \\ & \to (\lambda y . P) Q \\ \\ & \to P  \end{align}$$

Now let's consider $S P Q R$ 

$$\begin{align} S P Q R & = (\lambda x y z . xz(yz)) P \; Q \; R \\ \\ & = (\lambda x . (\lambda y . (\lambda z . (xz (yz) )))) P \; Q \; R \\ \\ & \to (\lambda y . (\lambda z . (P z (y z) )))  Q \; R  \\ \\ & \to (\lambda z . (P z (Qz) ))  R \\ \\ & \to P R (Q R) \end{align} $$

(b) We note that $I:= \lambda x.x$ is the identity function.

$$\begin{align} S K K  & = (λx y z. x z (y z)) (λab. a) (λcd. c) \\ \\ & \to ( λy z. (λab. a) z(y z) ) (λcd. c) \\ \\ & \to  ( λz. (λab. a) z( (λcd. c) z) ) \\ \\ & \to  ( λz.z) \end{align}$$

(c) This is algebra torture, but we'll proceed carefully.

$$\begin{align} S (K S) K & = (\lambda x y z . x z (y z) ) (K S) K \\ \\ &\to (\lambda y z . (K S) z (y z) ) K \\ \\ & \to (\lambda z . (K S) z (K z) ) \\ \\ & \to  (\lambda z . ((\lambda a b . a) (\lambda u v w . u w (v w))) z ( (\lambda a b . a) z) ) \\ \\ & \to (\lambda z . (\lambda u v w . u w (v w)) ( (\lambda a b . a) z) )  \\ \\ & \to (\lambda z . (\lambda v w . ( (\lambda a b . a) z) w (v w) ) )  \\ \\ & \to  (\lambda z . (\lambda v w . z (vw) ) )  \\ \\ & = (\lambda z v w . z (v w)) \end{align}$$

So

$$(\lambda z v w . z (v w)) \;  U V W \to U (V W)$$

(d) Again, algebra torture. Here we need to show the two expressions reduce to the same β-normal-form.

First we consider $S S S K K$. 

$$\begin{align} S S S K K & = ( ( (S S) S) K )  K \\ \\ & =  ( ( ( (λxyz. xz(yz)) (λabc. ac(bc))) (λuvw. uw(vw))) (λjk. j) )  (λmn. m)  \\ \\ & \to ( ( (λyz. (λabc. ac(bc))z(yz) ) (λuvw. uw(vw))) (λjk. j) )  (λmn. m) \\ \\ & \to ( λz. (λabc. ac(bc))z( (λuvw. uw(vw)) z) ) (λjk. j)  (λmn. m)  \\ \\ & \to (λabc. ac(bc)) (λjk. j) ( (λuvw. uw(vw)) (λjk. j))  (λmn. m) \\ \\ & \to (λjk. j)  (λmn. m) ( ( (λuvw. uw(vw)) (λjk. j))  (λmn. m) ) \\ \\ & \to  (λmn. m)  \end{align}$$

Next we consider $S K K K$. Note that $S K K K = I$, so the expression reduces to just $K$ which is $λxy. x$, the same as what the first expression reduces to.

Since the two expressions reduce to the same normal form, they are β-equivalent.

Chapter 1 - Exercise 7 - 8

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.

Chapter 1 - Exercises 5 - 6

Exercise 1.5

Give the results of the following substitutions:

(a) (λx. y(λy. xy))[y := λz. zx],

(b) ((xyz)[x := y])[y := z],

(c) ((λx. xyz)[x := y])[y := z],

(d) (λy. yyx)[x := yz].

(a) Because $x$ and $y$ are bound variables in the term, we should α-rename them before substitution happens.

$$\begin{align} (\lambda x. y(\lambda y. xy)) \; [y := \lambda z. zx] & =_{\alpha} (\lambda a. y(\lambda b. a b))\; [y := \lambda z. zx] \\ \\ & = (\lambda a. (\lambda z. z x)(\lambda b. a b)) \\ \\ & =_{\alpha} (\lambda a. (\lambda z. z x)(\lambda y. a y)) \end{align}$$

The last line re-introduces $y$ but is not necessary.

(b) The variables $x$, $y$ and $z$ in the term are free, unbound so we can proceed with the substation in the given order. 

$$\begin{align} ((x y z)[x := y])[y := z] & = (y y z)[y := z] \\ \\ & = (z z z) \end{align} $$

(c) Here $x$ is a bound variable so we should α-rename the term before attempting substitution.

$$\begin{align}((λx. xyz)[x := y])[y := z] & =_{\alpha} ((λa. ayz)[x := y])[y := z] \\ \\ & =  (λa. ayz)[y := z] \\ \\ &= (λa. a z z) \\ \\ & =_{\alpha} (λx. x z z)  \end{align}$$

Note that the first substitution $[x := y]$ has no effect.

(d) Here $y$ is bound variable so we should α-rename the term before proceeding with substitution.

$$\begin{align} (λy. yyx)[x := yz] & =_{\alpha} (λa. aax)[x := y z] \\ \\ & =  (λa. a a (y z)) \\ \\ & =_{\alpha} (λx. x x (y z))  \end{align}$$

Exercise 1.6

Show that the following proposition is not always true:

$$M[x := N,y := L] ≡ M[x := N][y := L]$$

where the expression on the left-hand side means a simultaneous substitution; so, $M[x := N,y := L]$ is the result of replacing all free $x$’s and $y$’s in $M$ at the same time(‘together’) by $N$ and $L$, respectively. (The expression on the right-hand side is concerned with sequential substitution.)

Let's take $M := xy$, $N:=y$ and $L:=x$, and perform the simultaneous substitution.

$$\begin{align} (x y) [x:= y, y:=x]  = (y x) \end{align}$$

Now let's consider the sequential substitution.

$$\begin{align} (x y) [x:= y][y:=x]  & = (y y) [y:=x] \\ \\ & = (x x) \end{align}$$

This counter-example shows the proposition is not always true.

Chapter 1 - Ex 4

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$.

Let's now consider how the expressions align with the Barendregt convention of using different names for all binding and bound variables for easier comprehension.

$(λy. yxy)((λz. xz)x)$ - All bound and binding variables have distinct names.

$(λx. xyx)((λz. yz)y)$ - All bound and binding variables have distinct names.

$(λy. yxy)((λy. xy)x)$ - The $y$ in the second part should be renamed. For example $(λy. yxy)((λw. xw)x)$

$(λv. (vx)v)((λu. uv)x)$ - All bound and binding variables have distinct names.

Chapter 1 - Ex 1 - 3

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$.

Welcome!

I've just started working through Type Theory and Formal Proof, and in this blog I'll be working through the exercises.

I previously worked through beginner courses on maths proofs, Lean for formalising simple maths proofs, Lisp and Haskell.

My overall aim is to understand how type theory can be used to check mathematical proofs.