Chapter 4 - Exercise 7

Exercise 4.7

(a) Give λω-definitions of the notions legal term, statement, λω-context and domain.

(b) Formulate the following theorems for λω: Free Variables Lemma, Thinning Lemma, Substitution Lemma.

(a) The following are λω analogues of already defined notions.

A term $Γ ⊢ M:σ$ is legal in λω if there exists a context $Γ$ such that a term $M$ with type $σ$ is derivable, where $σ$ is a constructor (type or proper constructor), kind or $\Box$.

A statement is of the form $M:σ$ where $M$ is a term and $σ$ is a constructor, kind or $\Box$.

A λω-context is a list of declarations, where declarations are statements with a variable as the subject, and where the context is derivable according to the derivation rules.

A domain is the ordered list of subjects of the declarations in a context.

(b)  The following are λω analogues of already defined theorems.

Free Variables Lemma. In a judgement $Γ⊢M:σ$, the free variables of $M$ are in the domain, that is, $FV(M) \subseteq dom(Γ)$. 

Thinning Lemma. Let $Γ'$ and $Γ''$ be contexts such that $Γ' ⊆Γ''$. If $Γ' ⊢M : σ$, then also $Γ'' ⊢M : σ$. 

Substitution Lemma. Assume $Γ', x : σ$, $Γ'' ⊢ M : τ$ and $Γ' ⊢N : σ$. Then $Γ', Γ'' ⊢M[x := N] : τ$.

Here,  $σ$ is a constructor (type or proper constructor), kind or $\Box$.

Chapter 4 - Exercise 6

Exercise 4.6

(a) Prove that there are no $Γ$ and $N$ in λω such that $Γ ⊢ \Box : N$ is derivable.

(b) Prove that there are no $Γ$, $M$ and $N $in λω such that $Γ ⊢M→ \Box : N$ is derivable.

(a) We will prove this by structural induction.

Figure 4.1 in the textbook summarises the derivation rules for λω, and the conclusion $Γ ⊢ \Box : N$ must be a result of one of the seven rules.

In fact it can only be a result of (weak) or (conv). Let's consider each in turn.  

Note that (var) is not applicable as the rule creates a variable, not a more general term. That is, $x$ in the rule is a metavariable which can represent a variable like $y$, but not any term, like $yx$ or $\Box$.

The induction hypothesis is that a judgement of the form $Γ ⊢ \Box : N$ is not derivable holds for the premises.

(weak) A conclusion $Γ ⊢ \Box : N$ would require $Γ' ⊢ \Box : N$ as one of the two premises. The induction hypothesis, true for the premises, is that $Γ' ⊢ \Box : N$ is not derivable. So the conclusion of this rule is not derivable.

(conv) A conclusion $Γ ⊢ \Box : N$ would require $Γ ⊢ \Box : M'$ as one of the two premises, where $M =_\beta M'$. By induction, $Γ ⊢ \Box : M'$ is not derivable, and so the conclusion of this rule is not derivable.

So by structural induction $Γ ⊢ \Box : N$ is not derivable in λω.

(b) We will also prove this by structural induction.

A conclusion $Γ ⊢M→ \Box : N$ can only be a result of the (weak), (form) and (conv) rules. Let's consider each in turn.  

The induction hypothesis is that a judgement of the form $Γ ⊢M→ \Box : N$ is not derivable holds for the premises.

(weak) A conclusion $Γ ⊢M→ \Box : N$ would require $Γ' ⊢M→ \Box : N$ as one of the two premises. The induction hypothesis tell us that $Γ' ⊢M→ \Box : N$ is not derivable, So the conclusion of this rule is not derivable.

(form) A conclusion $Γ ⊢M→ \Box : N$ would require two premises $Γ ⊢M: N$ and $Γ ⊢\Box : N$. However, we've shown above that $Γ ⊢ \Box : N$ is not derivable, so the conclusion of this rule is not derivable.

(conv) A conclusion $Γ ⊢M→ \Box : N$ would require $Γ ⊢M→ \Box : M$ as one of the two premises, where $M =_\beta N$. The induction hypothesis tells us that a judgement of the form $Γ ⊢M→ \Box : M$ is not derivable, and so the conclusion of this rule is not derivable.

So by structural induction $Γ ⊢M→ \Box : N$ is not derivable in λω.

Chapter 4 - Exercise 5

Exercise 4.5

Give a shortened λω-derivation in flag format of the following judgement:

$α : ∗, x : α ⊢ λy : α. x : (λβ : ∗. β →β)α$

The following is a shorted derivation in flag format (click to enlarge).

Chapter - Exercise 4

Exercise 4.4

Give shortened λω-derivations in flag format of the following judgements:

(a) $α : ∗, β : ∗→∗ \; ⊢ \; β(βα) : ∗$

(b) $α : ∗, β : ∗→∗, x : β(βα) \; ⊢ \; λy : α. x : α →β(βα)$

(c) $∅ \; ⊢ \; λα : ∗. λβ : ∗→∗. β(βα) : ∗→(∗→∗) →∗$

(d) $∅ \; ⊢ \; (λα : ∗. λβ : ∗→∗. β(βα)) \; nat \; (λγ : ∗. γ) : ∗$, assuming that $nat$ is a constant of type $∗$.

(a) The following shows both the full and shortened derivation.

(b) The following is a shortened derivation.

(c) The following is a shortened derivation.

(d) The following is a shortened derivation.

Chapter 4 - Exercise 3

Exercise 4.3

(a) Give a complete (i.e. not shortened) λω-derivation in flag format of

$$α,β : ∗, x : α, y : α →β ⊢ yx : β$$

(b) Give a shortened λω-derivation in flag format of

$$α,β : ∗, x : α, y : α →β, z : β →α ⊢ z(yx) : α$$

(a) The flag notation derivation is as follows (click to enlarge).

(b) The flag notation derivation is as follows (click to enlarge). It expands on the above because all except one statement in the context is the same as the previous example.

Chapter 4 - Exercise 2

Exercise 4.2

Give complete λω-derivations, first in tree format and then in flag format (not shortened), of the following judgements:

(a) $∅ ⊢ (∗→∗) →∗ : \Box$

(b) $α : ∗, β : ∗ ⊢ (α →β) →α : ∗$

(a) The tree format derivation is as follows.

$$ (1) \; \emptyset \vdash * : \Box \quad (sort)$$

$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box \quad} {(2) \; \emptyset \vdash * \to * : \Box} \;(form) $$

$$ \frac{(2) \; \emptyset \vdash * \to * : \Box \qquad 1) \; \emptyset \vdash * : \Box} {(3) \; \emptyset \vdash (* \to *) \to * : \Box} \;(form) $$

The flag format derivation is as follows.

(b) The tree format derivation is as follows.

$$ (1) \; \emptyset \vdash * : \Box \quad (sort)$$

$$ \frac{(1) \; \emptyset \vdash * : \Box}{(2) \; \alpha:* \vdash \alpha:*} \; (var) $$

$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box}{(3) \; \alpha:* \vdash *:\Box} \; (weak) $$

$$ \frac{(2) \; \alpha:* \vdash \alpha:* \qquad (3) \; \alpha:* \vdash *:\Box}{(4) \; \alpha:*, \beta:* \vdash \alpha:*} \; (weak) $$

$$ \frac{(3) \; \alpha:* \vdash *:\Box}{(5) \; \alpha:*, \beta:* \vdash \beta:*} \; (var) $$

$$ \frac{(4) \; \alpha:*, \beta:* \vdash \alpha:* \qquad (5) \; \alpha:*, \beta:* \vdash \beta:*}{(6) \; \alpha:*, \beta:* \vdash \alpha \to \beta:*} \; (form) $$

$$ \frac{(6) \; \alpha:*, \beta:* \vdash \alpha \to \beta:* \qquad (4) \; \alpha:*, \beta:* \vdash \alpha:*}{(7) \; \alpha:*, \beta:* \vdash (\alpha \to \beta) \to \alpha:*} \; (form) $$

The flag format derivation is as follows.

Chapter 4 - Exercise 1

Exercise 4.1

Give a diagram of the tree corresponding to the complete tree derivation of line (16) of Section 4.5.

For ease of reference, the following is the flag formation derivation of line  16.

And the following is a diagram representing this derivation.

This is a good guide to creating graphs in tikz for latex (link).

Chapter 3 - Exercise 21

Exercise 3.21

Give a recursive definition for $FTV(A)$, the set of free type variables in $A$, for an expression $A$ in $\mathbb{T}2$ or in $Λ_{\mathbb{T}2}$.

Let's remind ourselves of the recursive definition for free variables in untyped λ-terms.

Definition 1.4.1 ($FV$, the set of free variables of a λ-term)

(1) (Variable) $FV(x) = \{x\}$

(2) (Application) $FV(MN) = FV(M)∪FV(N)$

(3) (Abstraction) $FV(λx. M) = FV(M) \{x\}$

Let's also remind ourselves of the sets $\mathbb{T}2$ and $Λ_{\mathbb{T}2}$.

$\mathbb{T}2 = \mathbb{V} |(\mathbb{T}2 →\mathbb{T}2) |(Π\mathbb{V} : ∗. \mathbb{T}2)$

$Λ_{\mathbb{T}2} = V|(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})|(Λ_{\mathbb{T}2}\mathbb{T}2)|(λV : \mathbb{T}2. Λ_{\mathbb{T}2})|(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$

Our recursive definition will need to cover all these cases. In the following section we'll consider each case.

$A$ in $\mathbb{T}2$, the λ2 Types

Let's consider the syntax cases for λ2 types.

• $\mathbb{V}$. These are type variables, for which we usually use lower case greek symbols, eg $α, β, γ$. In this case the type variable is free, and so $$FTV(α)=\{α\}$$
• $(\mathbb{T}2 →\mathbb{T}2)$. These are arrow types between other type variables, for example $α→β$. In this case the free type variables are those in the "from" and "to" expressions. So $$FTV(M→N)=FTV(M) \cup FTV(N)$$
• $(Π\mathbb{V} : ∗. \mathbb{T}2)$. These are the abstractions over a single type variable. An example is $Πα:*.α→Mα$. In this case, the abstracted variable is bound, not free, and so $$FTV(Πα:*.M) = FTV(M) \setminus \{α\}$$

$A$ in $Λ_{\mathbb{T}2}$, the Pre-Typed λ2 Terms

Let's now consider the syntax cases for the pre-typed λ2-terms.

• $V$. This is the simple case of a single term variable annotated with a type, eg $x$. These variables are pre-typed, and so the expression $x$ has no type variables in it. This means $$FTV(x)=\emptyset$$
• $(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})$. This is the application of one term to another, for example $MN$. Here we have $$FTV(MN)=FTV(M) \cup FTV(N)$$
• $(Λ_{\mathbb{T}2}\mathbb{T}2)$. This is the application of a term to a type, for example $Mα$. In this case $α$ is free, and so we have $$FTV(Mα)=FTV(M) \cup \{α\}$$
• $(λV : \mathbb{T}2. Λ_{\mathbb{T}2})$. This is an abstraction over a term variable, for example $λx.M$. Since $x$ is not a type variable, we have $$FTV(λx.M)=FTV(M)$$
• $(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$. This is an abstraction over a type variable, for example $λα.M$. Here $α$ is not free, and so $$FTV(λα.M) = FTV(M) \setminus \{α\}$$

Recursive Definition

λ2 Types

• (Type Variable) $FTV(α)=\{α\}$
• (Arrow Type) $FTV(M→N)=FTV(M) \cup FTV(N)$
• (Abstraction) $FTV(Πα:*.M) = FTV(M) \setminus \{α\}$

λ2 Terms

• (Term Variable) $FTV(x)=\emptyset$
• (Application to term) $FTV(MN)=FTV(M) \cup FTV(N)$
• (Application to type) $FTV(Mα)=FTV(M) \cup \{α\}$
• (Abstraction of term) $FTV(λx.M)=FTV(M)$
• (Abstraction of type) $FTV(λα.M) = FTV(M) \setminus \{α\}$

Chapter 3 - Exercise 20

Exercise 3.20

Prove the Free Variables Lemma for λ2 (cf. Lemma 3.6.4): if $Γ ⊢ L : σ$, then $FV(L) ⊆dom(Γ)$.

The textbook has already proved the Free Variables Lemma (2.10.3) for simply-typed λ-terms, That proof used definition 2.4.5 which provides the three derivation rules, (var), (appl) and (abst). 

That means we can prove the Free Variables Lemma by considering the additional derivation rules for λ2-terms listed in Figure 3.1. These are $(form)$, $(appl_2)$ and $(abst_2)$. Let's consider each in turn.

Formation Rule

Consider a judgement resulting from the formation rule. Then it has the form $Γ⊢B:*$ where $B$ is a λ2-type, and any free variables in $B$ are declared in $Γ$. That is $FV(B) \subseteq dom(Γ)$.

Like the (var) rule, the $(form)$ rule does not have any premises.

$(appl_2)$ Rule

Now consider a judgement resulting from the λ2 application rule, $(appl_2)$. 

If the two premises are $Γ ⊢ M : (Πα : ∗. A)$ and $Γ ⊢ B : ∗$, then the resulting judgement is $Γ ⊢ MB : A[α := B]$. 

By induction, we assume the Free Variables Lemma holds for the premises, $Γ ⊢ M : (Πα : ∗. A)$ and $Γ ⊢ B : ∗$. This means $FV(M) \subseteq dom(Γ)$ and $FV(B) \subseteq dom(Γ)$. By Definition 1.4.1 $FV(MB) = FV(M)∪FV(B)$, which gives us $FV(MB) \subseteq dom(Γ)$.

$(abst_2)$ Rule

Finally consider a judgement resulting from the λ2 abstraction rule, $(abs_2)$.

If the premise is $Γ, α : ∗ ⊢ M : A$, then the resulting judgement is $Γ ⊢ λα : ∗. M : Πα : ∗. A$.

By induction, we assume the Free Variables Lemma holds for the premise $Γ, α : ∗ ⊢ M : A$. This means $FV(M) \subseteq dom(Γ) \cup \{α\}$. Again using Definition 1.4.1 for free variables, we have $FV(λα : ∗. M) = FV(M) \setminus \{α\}$, and so $FV(λα : ∗. M) \subseteq dom(Γ)$.

By showing the Free Variables Lemma holds for the 3 addition derivation rules for λ2-terms, and using the previous result that the Free Variables Lemma holds for simply typed λ-terms, we have shown it holds for all λ2-terms.

Chapter 3 - Exercise 19

Exercise 3.19

Prove: if $Γ ⊢ L : σ$, then $Γ$ is a λ2-context.

Let's first remind ourselves of the definition 3.4.4 of a λ2-context.

(1) $∅$ is a λ2-context; $dom(∅) = ()$, the empty list.

(2) If $Γ$ is a λ2-context, $α ∈\mathbb{V}$ and $α  \notin dom(Γ)$, then $Γ, α : ∗$ is a λ2-context; $dom(Γ,α : ∗) = (dom(Γ), α)$, i.e. $dom(Γ)$ concatenated with $α$.

(3) If $Γ$ is a λ2-context, if $ρ ∈ \mathbb{T}2$ such that $α ∈dom(Γ)$ for all free type variables $α$ occurring in $ρ$ and if $x \notin dom(Γ)$, then $Γ, x : ρ$ is a λ2-context; $dom(Γ,x : ρ) = (dom(Γ), x)$.

We'll use structural induction on $Γ$ to prove the statement.

Base Case

The base case is $Γ≡\emptyset$. The statement we need to prove for the base case is

$$ ( Γ ≡\emptyset ⊢ L : σ ) \implies Γ \text{ is a λ2 context}$$

The definition 3.4.4 (1) tells us the empty set $\emptyset$ is a λ2 context, so the base case is proven.

Induction Step

The induction hypothesis is as follows

$$ ( Γ^{\prime} ≡\emptyset ⊢ L : σ ) \implies Γ^{\prime} \text{ is a λ2 context}$$

We need to prove that for any $L$ constructed from $Γ^{\prime}$ using each of the two constructors of definition 3.4.4 (2) and (3), the following statement is true.

$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$

Let's consider each in turn.

Type Variable Constructor

Using definition 3.4.4 (2), if $Γ^{\prime}$ is a λ2-context, $α ∈\mathbb{V}$ and $α  \notin dom(Γ^{\prime})$, then $Γ = Γ^{\prime}, α : ∗$ is a λ2-context.

The Thinning Lemma tells us that if $ Γ^{\prime} ⊢ L : σ$, then $Γ = Γ^{\prime}, α : ∗ ⊢ L : σ$. 

So we have

$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$

Object Variable Constructor

Using definition 3.4.4 (3),  if $Γ$ is a λ2-context, and if $ρ ∈ \mathbb{T}2$ such that $α ∈dom(Γ)$ for all free type variables $α$ occurring in $ρ$ and if $x \notin dom(Γ)$, then $Γ, x : ρ$ is a λ2-context.

The Thinning Lemma tells us that if $ Γ^{\prime} ⊢ L : σ$, then $Γ = Γ^{\prime}, x : ρ ⊢ L : σ$. 

So again we have

$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$

Conclusion

We showed the statement

$$ ( Γ ≡\emptyset ⊢ L : σ ) \implies Γ \text{ is a λ2 context}$$

is true for the base case of $Γ≡\emptyset$, and also for $Γ$ constructed using any of the two constructors from the definition of a λ2 context. 

So by structural induction, the statement is true in general.

Chapter 3 - Exercise 18

Exercise 3.18

See Exercise 3.14. We define the type $Tree$, representing the set of binary trees with boolean-labelled nodes and leaves, by

$$Tree ≡ Πα : ∗. (Bool →α) →(Bool →α →α →α) →α$$

Then $λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M$ has type $Tree$, for every λ2-term $M$ of type $α$.

(a) Sketch the three trees that are represented if we take for M, respectively:

$u \; False$

$v \; True(u \; False)(u \; True)$

$v \; True(u \; True)(v \; False(u \; True)(u \; False))$

(b) Give a λ2-term which, on input a polymorphic boolean $p$ and two trees $s$ and $t$, delivers the combined tree with $p$ on top, left subtree $s$ and right subtree $t$.

(a) The value of a node is of type Bool. The function $u$ represents a leaf, a terminal node, and the function $v$ represents a node with two sub-trees.

The following diagram shows representations of the three terms (click to enlarge).

(b) The desired λ2-term must have a type $Bool → Tree → Tree → Tree$.

We have $s$ and $t$ as follows:

$$ s ≡ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M_s $$

$$ t ≡ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. M_t $$

Here $M_s$ and $M_t$ have type $α$, and the entire term has type $Tree$.

The combined tree is as follows:

$$ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v (p)(M_s)(M_t) $$

We can derive $M_s:α$ and $M_t:α$ from $s$ and $t$ as follows

$$M_s = sαuv, \quad M_t = tαuv$$

So the combined tree is:

$$ λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v(p)(sαuv)(tαuv) $$

We can write the desired λ2-term with type $Bool → Tree → Tree → Tree$.

$$  λp:Bool. λs,t:Tree . ( λα : ∗. λu : Bool →α. λv : Bool →α →α →α. v(p)(sαuv)(tαuv) )$$

Chapter 3 - Exercise 17

Exercise 3.17

See the previous exercises. Find a λ2-term $Iszero$ that represents the test-for-zero. That is, define a λ2-term such that $Iszero \; Zero =_β True$ and $Iszero \; n =_β False$ for all polymorphic Church numerals $n$ except $Zero$. (Hint: see Exercise 1.14)

Let's remind ourselves of some definitions.

The Church booleans.

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

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

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

The Church numerals.

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

$Zero ≡ λα : ∗. λf : α →α. λx : α. x$

$One ≡ λα : ∗. λf : α →α. λx : α. f x$

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

From Exercise 1.13, we have the untyped $iszero := λz. z(λx. \; false) \; true$. 

The key to how it works is that zero $λfx.x$ applied to $(λx. \; false) (true)$ picks $true$, and any non-zero Church numeral $λfx.f^{n}x$ picks $false$. This is the mechanism we need to re-use in our generalisation to λ2.

Comparing the λ2 Church numerals with the selection mechanism above, we see we need to resolve the type variable $λα : ∗$ leaving a term that takes two parameters $ λf : α →α. λx : α$.

$$Iszero \equiv λz:Nat.z(Bool)(λx:Bool. \; False) \; True $$

The type of $x$ as $Bool$ is required because $(λx. \; False)$ needs to be $Bool \to Bool$, and that requires the type argument to $z$ also needs to be $Bool$ such that the $f$ in the Church numerals is $Bool \to Bool$.

Let's check $Iszero \; Zero =_β True$.

$$\begin{align} Iszero \; Zero &\equiv (λz:Nat.z(Bool)(λx: Bool. \; False) \; True ) \; Zero \\ \\ & =_β  (Zero)(Bool)(λx:Bool. \; False) \; True \\ \\ & =_β  (λf : Bool →Bool. λx : Bool. x)(λx: Bool. \; False) \; True \\ \\ & =_β  True  \end{align}$$

Let's also check $Iszero \; One =_β False$.

$$\begin{align} Iszero \; One &\equiv (λz:Nat.z(Bool)(λx: Bool. \; False) \; True ) \; One \\ \\ & =_β  (One)(Bool)(λx:Bool. \; False) \; True \\ \\ & =_β  (λf : Bool →Bool. λx : Bool. fx)(λx: Bool. \; False) \; True \\ \\ & =_β  False  \end{align}$$

Chapter 3 - Exercise 16

Exercise 3.16

See the previous exercises. Find λ2-terms that represent the logical operators ‘inclusive or’, ‘exclusive or’ and ‘implication’.

The Wikipedia page helps think about what logical operators must do (link). This page is also helpful (link). This thinking tells us a logical conjunction operating on two Booleans $p,q$ must return $q$ if $p$ is true, else return $p$, which would be false in this case. That is, $pqp$,

Using this we can look afresh at the λ2 generalisation to see how it does this.

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

If $u$ is true, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false). 

If $u$ is false, then we select $(vβyy)$ and regardless of $v$ we pick $y$ (false).

Inclusive Or

Using the linked pages, we can see a logical disjunction operating on two Booleans $p, q$ must return $p$ if $p$ is true, else return $q$, where the value of $q$ becomes the final result. That is, $ppq$.

We generalise this to λ2 as follows.

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

If $u$ is true, then we select $(vβxx)$ and regardless of $v$ is true we pick $x$ (true). 

If $u$ is false, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).

Exclusive Or

A logical exclusive or operating on two Booleans $p, q$ must return $\neg q$ if $p$ is true, else return $q$, where the value of $q$ becomes the final result. That is, $p(\neg q)q$.

We generalise this to λ2 as follows.

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

If $u$ is true, then we select $(vβyx)$ and if $v$ is true we pick $y$ (false), else $x$ (true).

If $u$ is false, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).

Implication

A logical implication operating (link) on two Booleans $p, q$ always returns true, except if $p$ is true and $q$ is false. That is, $pqq$.

We generalise this to λ2 as follows.

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

If $u$ is true, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).

If $u$ is false, then we select $(vβxx)$ and regardless of $v$ we pick $x$ (true).

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 : α$. Further discussion here (link).

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