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.