Chapter 3 - Exercise 15

Exercise 3.15

See Exercise 3.14. Define $M$ by

$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy)$$

(a) Reduce the following terms to β-normal form:

$M \; True \; True$

$M \; True \; False$

$M  \; False  \; True$

$M  \; False  \; False$

(b) Which logical operator is represented by $M$?

(a) Let's do each in turn.

First $M \; True \; True$.

$$\begin{align} M \; True \; True & \equiv  λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (True) \; (True) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (True)β \; ((True)βxy) \; ((True)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. x)β \; ((λα : ∗. λx,y : α. x)βxy) \; ((λα : ∗. λx,y : α. x)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. x) \; ((λx,y : β. x)xy) \; ((λx,y : β. x)yy)  \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. x)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. x  \\ \\ &=_\beta True  \end{align}$$

Next $M \; True \; False$.

$$\begin{align} M \; True \; True & \equiv  λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (True) \; (False) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (True)β \; ((False)βxy) \; ((False)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. x)β \; ((λα : ∗. λx,y : α. y)βxy) \; ((λα : ∗. λx,y : α. y)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. x) \; ((λx,y : β. y)xy) \; ((λx,y : β. y)yy)   \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. y)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. y  \\ \\ &=_\beta False  \end{align}$$

Now $M \; False \; True$.

$$\begin{align} M \; True \; True & \equiv  λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (False) \; (True) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (False)β \; ((True)βxy) \; ((True)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. y)β \; ((λα : ∗. λx,y : α. x)βxy) \; ((λα : ∗. λx,y : α. x)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. y) \; ((λx,y : β. x)xy) \; ((λx,y : β. x)yy)  \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. x)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. x  \\ \\ &=_\beta False  \end{align}$$

Finally, $M  \; False  \; False$

$$\begin{align} M \; True \; True & \equiv  λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (False) \; (False) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (False)β \; ((False)βxy) \; ((False)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. y)β \; ((λα : ∗. λx,y : α. y)βxy) \; ((λα : ∗. λx,y : α. y)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. y) \; ((λx,y : β. y)xy) \; ((λx,y : β. y)yy)  \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. y)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. y  \\ \\ &=_\beta False  \end{align}$$

(b) $M$ behaves as the logical conjunction $\land$, also written as "AND".

Chapter 3 - Exercise 14

Exercise 3.14

We may also introduce the polymorphic booleans in λ2:

$Bool ≡Πα : ∗. α →α →α$

$True ≡λα : ∗. λx,y : α. x$

$False ≡λα : ∗. λx,y : α. y$

Construct a λ2-term $Neg : Bool →Bool$ such that $Neg \; True=_β False$ and $Neg False=_β True$. Prove the correctness of your answer

Let's remind ourselves of the untyped $not := λz. z \; false \; true$. We can generalise this to a λ2 term as follows.

$$Neg ≡  λz:Bool. λα:*. z (Bool)(False)(True)$$

Let's check $Neg \; False=_β True$.

$$\begin{align} Neg \; True & \equiv   λz:Bool. λα:*. z (Bool) (False)(True) (False) \\ \\ & \to_\beta (False )(Bool)(False)(True) \\ \\ &\to_\beta (λα : ∗. λx,y : α. y)(Bool)(False)(True)  \\ \\ &\to_\beta (λx,y : Bool. y)(False)(True)   \\ \\ &\to_\beta True \tag*{$\Box$} \end{align}$$

For completeness, let's check $Neg \; True=_β False$.

$$\begin{align} Neg \; True & \equiv   λz:Bool. λα:*. z (Bool) (False)(True) (True) \\ \\ & \to_\beta (True )(Bool)(False)(True) \\ \\ &\to_\beta (λα : ∗. λx,y : α. x)(Bool)(False)(True)  \\ \\ &\to_\beta (λx,y : Bool. x)(False)(True)   \\ \\ &\to_\beta False \tag*{$\Box$} \end{align}$$

Chapter 3 - Exercise 13

Exercise 3.13

See the previous exercise.

(a) We define $Add$ in λ2 as follows:

$Add ≡λm,n : Nat . λα : ∗. λf : α →α. λx : Nat . mαf(nαf x)$

Show that $Add$ simulates addition, by evaluating $Add \; One \; One$.

(b) Find a λ2-term $Mult$ that simulates multiplication on $Nat$. (Hint: see Exercise 1.10.)

(a) Let's evaluate  $Add \; One \; One$.

$$\begin{align} Add \; One \; One & \equiv  (λm,n : Nat . λα : ∗. λf : α →α. λx : Nat . mαf(nαf x)) \; (λα : ∗. λf : α →α. λx : α. f x) \; (λα : ∗. λf : α →α. λx : α. f x) \\ \\  & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λα : ∗. λf : α →α. λx : α. f x] αf([λα : ∗. λf : α →α. λx : α. f x] αf x)  \\ \\  & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λx : α. f x] ([λx : α. f x]x)  \\ \\  & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λx : α. f x] (f x)   \\ \\  & \to_\beta λα : ∗. λf : α →α. λx : Nat . [f (fx)]   \\ \\ &\to_\beta Two \tag*{$\Box$}\end{align}$$

So $Add \; One \; One$ is indeed $Two$. 

Note that I think there is a typo in the textbook, where $λx : Nat$ should be $λx : α$.

(b) From exercise 1.10 we're given $mult := λmnfx. m(nf)x$. From this we can generalise a λ2 $Mult$ as follows.

$$Mult := λm,n:Nat . λα:*. λf:α→α.λx:α. mα(nαf)x$$

Let's test it with $Mult \; One \; Two$.

$$\begin{align} Mult \; One \; Two & \equiv  λm,n:Nat . λα:*. λf:α→α.λx:α. mα(nαf)x \; (λα : ∗. λf : α →α. λx : α. f x) \; (λα : ∗. λf : α →α. λx : α. f (fx)) \\ \\  &\to_\beta λα:*. λf:α→α.λx:α. [λα : ∗. λf : α →α. λx : α. f x] α([λα : ∗. λf : α →α. λx : α. f (fx)] αf)x \\ \\  &\to_\beta λα:*. λf:α→α.λx:α. [λf : α →α. λx : α. f x](λx : α. f (fx))x   \\ \\  &\to_\beta λα:*. λf:α→α.λx:α.  (f (fx)) \\ \\ &\to_\beta Two \tag*{$\Box$} \end{align}$$

So $Mult \; One \; Two$ is indeed $Two$.

Chapter 3 - Exercise 12

Exercise 3.12

As mentioned in Section 3.8, we have in λ2 the polymorphic Church numerals. They resemble the untyped Church numerals, as described in Exercises 1.10 and 1.13(b). For example:

$Nat ≡ Πα : ∗. (α →α) →α →α$,

$Zero ≡ λα : ∗. λf : α →α. λx : α. x$, having type Nat,

$One ≡ λα : ∗. λf : α →α. λx : α. f x$, with type Nat, as well,

$Two ≡ λα : ∗. λf : α →α. λx : α. f(f x)$.

We define $Suc$ as follows as a λ2-term:

$$Suc ≡λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x)$$

Check that $Suc$ acts as a successor function for the polymorphic Church numerals, by proving that $Suc \; Zero =_β One$ and $Suc \; One =_β Two$.

Let's start with $Suc \; Zero =_β One$.

$$\begin{align} Suc \; Zero & \equiv ( λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x) ) \; ( λα : ∗. λf : α →α. λx : α. x )  \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λα : ∗. λf : α →α. λx : α. x) βf x)  \\ \\ & \to_\beta  λβ : ∗. λf : β →β. λx : β. f( (λf : β →β. λx : β. x) f x)  \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λx : β. x) x)  \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. fx \\ \\ &=_\beta One  \tag*{$\Box$} \end{align}$$

Note the penultimate line is the definition of $One$ with the variable $\alpha$ renamed to $\beta$.

Now let's consider $Suc \; One =_β Two$.

$$\begin{align} Suc \; One & \equiv ( λn : Nat . λβ : ∗. λf : β →β. λx : β. f(nβf x) ) \; ( λα : ∗. λf : α →α. λx : α. f x )   \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λα : ∗. λf : α →α. λx : α. fx) βf x)  \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λf : β →β. λx : β. fx) f x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (λx : β. fx) x) \\ \\ & \to_\beta λβ : ∗. λf : β →β. λx : β. f( (fx)  \\ \\ &=_\beta Two  \tag*{$\Box$}  \end{align}$$

Again the penultimate line is the definition of $Two$ with the variable $\alpha$ renamed to $\beta$.

Chapter 3 - Exercise 11

Exercise 3.11

Take $⊥$as in Exercise 3.5. Prove that the following term is legal in the empty context:

$$ λx : ⊥. x(⊥→⊥→⊥)(x(⊥→⊥)x)(x(⊥→⊥→⊥)xx) $$

What is its type?

Let's remind ourselves of $⊥$,

$$ ⊥ \equiv Πα:*.α $$

This tells us $x$ is a function that takes a type as argument, and returns an object of that type.

The following flag format derivation considers the 3 sub-terms in the longer term: $x(⊥→⊥→⊥)$, $(x(⊥→⊥)x)$, and $(x(⊥→⊥→⊥)xx)$ separately, before combining them.

We have derived the term and it has a type $⊥→⊥x$ in the empty context, so is legal.

Chapter 3 - Exercise 10

Exercise 3.10

Let $M ≡ λx : (Πα : ∗. α →α) . x(σ →σ)(xσ)$. 

(a) Prove that $M$ is legal in λ2.

(b) Find a term $N$ such that $M N$ is legal in λ2 and may be considered to be a proper way of adding type information to $(λx. xx)(λy. y)$.

(a) To show $M$ is legal in λ2 we need to find a context such that $M$ has a type. The following derivation does this.

In the context $Γ \equiv σ:*$, the term $M$ has a type $(\Pi \alpha: * . (\alpha \to \alpha)) \to \sigma \to \sigma$, so $M$ is legal.

(b) Looking at the definition of $M$, we can see it takes an argument with type $(Πα : ∗. α →α)$. We can try a simple form for $N$, that is

$$N \equiv λα:*.λy:α.y$$

In fact section 3.8 of the textbook tells us this is the only closed term of that type. Furthermore, it corresponds to the sub-term $(λy. y)$ of the term we want to type.

Let's check that applying $M$ to $N$ does result in type $σ →σ$ as expected from the type of $M$.

$$\begin{align} M N & \equiv  ( λx : (Πα : ∗. α →α) . x(σ →σ)(xσ) ) \; (λα:*.λy:α.y) \; : \; σ →σ \\ \\ &\to_β  (λα:*.λy:α.y) (σ →σ) \; ((λα:*.λy:α.y)σ) \; : \; σ →σ \\ \\ &\to_β (λy:σ →σ.y)(λy:σ.y) \; : \; σ →σ \\ \\ &\to_β λy:σ.y \; : \; σ →σ \end{align}$$

$MN$ is legal because it has a type $σ →σ$ in the context $Γ \equiv σ:*$.

This $MN$ is a proper way of adding type information to $(λx. xx)(λy. y)$, as the following shows.

$$ σ:* \; ⊢\;  (λx: (Πα : ∗. α →α) . x(σ →σ)(xσ))(λy:σ. y) \; : \; σ →σ$$

Chapter 3 - Exercise 9

Exercise 3.9

Find a closed λ2-version of $S ≡λxyz. xz(yz)$, and establish its type.

It is useful to remind ourselves of the derivation for the simply typed $S$ (ex 2.3).

There we found the type of $S$ is

$$ S : (B \to (A \to C)) \to (B \to A) \to B \to C $$

Here we want to parameterise the types of $x$, $y$ and $z$, and we can do this as follows.

$$ λα,β,γ:*. λx:β → (α→γ). λy:β→α . λz:β. xz(yz) :  Παβγ:*.(β → (α→γ)) → (β→α) → β → γ$$

The type is analogous to the previously established type, but this time the components $α,β,γ$ are abstracted.

Chapter 3 - Exercise 8

Exercise 3.8

Recall that $K ≡λxy. x$ in untyped lambda calculus.

Consider the following types:

$$\begin{align} T1 &≡ Πα,β : ∗. α →β →α \\ \\ T2 &≡ Πα : ∗. α →(Πβ : ∗. β →α) \end{align}$$

Find inhabitants $t1$ and $t2$ of $T1$ and $T2$, which may be considered as different closed λ2-versions of $K$.

An inhabitant of $T1$ is

$$ λα:*.λβ:*.λx:α.λy:β.x  $$

This is like $K$ but with each variable typed.

An inhabitant of $T2$ is

$$ λα:*. λx:α . (λβ:*. λy:β. x)$$

This is similar to the previous term but the type of $y$ is delayed until after $x$ is established. 

Chapter 3 - Exercise 7

Exercise 3.7

Take $⊥$ as in Exercise 3.5.

Let context $Γ$ be $α : ∗, β : ∗, x : α →⊥, f : (α →α) →α$.

Give a derivation to successively calculate an inhabitant of $α$ and an inhabitant of $β$, both in context $Γ$.

Let's write out the context in an easier to read format.

$$\begin{align}α &: ∗ \\ β& : ∗, \\ x &: α → Πγ:*.γ \\ f &: (α →α) →α \end{align}$$

Let's interpret the meaning of $x$. It is a function that, when supplied with an element of type $α$ returns a function of type $Πγ:*.γ$. That function must be of the form $λγ:*.M$, where $M:γ$. When provided a type $γ$, that function returns a term of type $γ$. So if $m$ has type $ρ$ then $xmα$ has type $α$.

Athough $xmα$ inhabits $α$, there is no $m$ in the context, so we need to abstract it away.

The type of $f$ suggests a term of type $(α→α)$ would be useful. This suggests we try $λm:α.xmα$ which has type $(α→α)$. Now we can easily see that $f(λm:α.xmα)$ has type $α$. 

So $f(λm:α.xmα)$ is a term that inhabits $α$, in the given context.

If $m$ has type $ρ$ then $xmβ$ has type $β$. Again we have to abstract $m$ away. Let's try $λm:β.xmβ$ which has type $β→β$. This leads to $f(λm:β.xmβ)$ having type $β$. 

So $f(λm:β.xmβ)$ is a term that inhabits $β$, in the given context.

Chapter 3 - Exercise 6

Exercise 3.6

Find terms in $Λ_{\mathbb{T}2}$ that are inhabitants of the following λ2-types, each in

the given context $Γ$:

(a) $Πα,β : ∗. (nat →α) →(α →nat →β) →nat →β$, where $Γ ≡nat : ∗$

(b) $Πδ : ∗. ((α →γ) →δ) →(α →β) →(β →γ) →δ$, where $Γ ≡α : ∗, β : ∗, γ : ∗$

(c) $Πα,β,γ : ∗. (α →(β →α) →γ) →α →γ$, in the empty context.

(a) The following derivation in flag notation shows the following term is an inhabitant in the given context.

$$ \lambda \alpha, \beta :* .\lambda f: nat \to \alpha . \lambda g: \alpha \to nat \to \beta .\lambda x:nat .\; g(fx)x $$

(b) The following derivation in flag notation shows the following term is an inhabitant in the given context.

$$ \lambda \delta: *. \lambda f: (\alpha \to \gamma) \to \delta . \lambda g: \alpha \to \beta .\lambda h:\beta \to \gamma. f(\lambda x:\alpha . h(gx)) $$

(c) The following derivation in flag notation shows the following term is an inhabitant in the given context.

$$ \lambda \alpha, \beta, \gamma : * . \lambda f:\alpha \to (\beta \to \alpha) \to \gamma . \lambda x : \alpha . fx (\lambda y:\beta.x) $$

Chapter 3 - Exercise 5

Exercise 3.5

Let $⊥≡Πα : ∗. α$ and $Γ ≡β : ∗, x : ⊥$.

(a) Show that there is a $t$ such that $⊥: t$. 

(b) Find an inhabitant of $β$ in context $Γ$.

(c) Give three not β-convertible inhabitants of $β →β$ in context $Γ$, each in β-normal form.

(d) Prove that the following terms inhabit the same type in context $Γ$:

$$λf : β →β →β. f(xβ)(xβ)$$

$$x((β →β →β) →β)$$

(a) Note that this exercise is updated by the errata, replacing the original.

An initial inspection of $⊥≡Πα : ∗. α$ tells us it takes a type $α$, itself of type $*$, and outputs that type. Therefore $⊥≡Πα : ∗. α$ should have type $*$. 

To show this more formally, we use the Formation Rule Definition 3.4.7.

$Γ ⊢ B : ∗$ if $Γ$ is a λ2-context, $B ∈\mathbb{T}2$ and all free type variables in $B$ are declared in $Γ$.

Here we have an empty yet valid λ2-context, and $B$ is $Πα : ∗. α$, a λ2-type with no free variable, and so $\emptyset ⊢ Πα : ∗. α : *$. By the Thinning lemma, we then have for any λ2-context  $Γ⊢⊥:*$.

(b) The context is not restricting what the inhabitant of $β$ can be, other that it being of type $*$.

The inhabitant must be a valid term, so we use $x$ to form that term. 

The term $xβ$ is of type $β$, and so is an inhabitant of $β$.

(c) Three examples of inhabitants of $β→β$ that aren't β-convertible to each other, and are in β-normal form are as follows.

Example 1

$$λz:β\; .z$$

has type $β→β$. The context defines $β$ so we don't need to in this term.

Example 2

$$λβ \; .xβ$$

has type $β→β$. Both $x$ and $β$ are defined in the context so this term does not need to. This is not β-convertible to $λz:β.z$.

Example 3

$$x (β→β)$$

has type $β→β$. This works because $(β→β)$ has type $*$ by the formation rule. This term is not β-convertible to $λz:β.z$ nor $λβ \; .xβ$. 

(d) The following flag notation derivation establishes the type of $λf : β →β →β. f(xβ)(xβ)$ as $(\beta \to \beta \to \beta) \to \beta$ in the context $Γ$:

And the following derivation establishes the type of $x((β →β →β) →β)$ also as $(\beta \to \beta \to \beta) \to \beta$ in the context $Γ$:

Therefore the two terms inhabit the same type in the context $Γ$.