Give a shortened derivation in λ2 to show that the following term is legal in the context $Γ ≡ nat : ∗, bool : ∗$
$$(λα,β : ∗. λf : α →α. λg : α →β. λx : α. g(f(f x))) \; nat \; bool$$
The following is a derivation in flag format.
Given a context $Γ ≡ nat : ∗, bool : ∗$, the given term has type $(nat \to nat) \to (nat \to bool) \to nat \to bool$, and so the term is legal.
Take $M$ as in Exercise 3.2. Assume $nat : ∗$, $bool : ∗$, $suc : nat → nat$ and $even : nat →bool$.
(a) Prove that $M \; nat \; nat \; bool \; suc \; even$ is legal.
(b) Prove that $λx : nat. even (suc \; x)$ is legal, in two ways:
(1) using Exercise 3.3(a) and Subject Reduction; (2) directly.
Let's remind ourselves of $M$,
$$M ≡λα,β,γ : ∗. λf : α →β. λg : β →γ. λx : α. g(f \; x)$$
We have already shown in Exercise 3.2 that $M$ is legal,
$$\emptyset \vdash \alpha, \beta, \gamma : *. \lambda g : \beta \to \gamma . \lambda f : \alpha \to \beta. \lambda x: \alpha . g (fx) : \Pi \alpha, \beta, \gamma : * . (\beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma$$
By the Thinning Lemma, every context $Γ$ entails the same term and type.
(a) We're given $Γ⊢nat:*$ and $Γ⊢bool:*$. Using (appl2) three times gives us
$$Γ⊢ ( α,β,γ:*. λ g : nat \to bool . λ f : nat \to nat. λ x: nat. g (f \; x) ) \; nat \; nat \; bool$$
$$: (nat \to bool) \to (nat \to nat) \to nat\to bool$$
Since $suc : nat → nat$ and $even : nat →bool$ are compatible types, we can use (appl) twice to get
$$Γ⊢ ( α,β,γ:*. λ g : nat \to bool . λ f : nat \to nat. λ x: nat. g (f \; x) ) \; nat \; nat \; bool \; suc \; even \; : nat\to bool$$
We have shown that for any context $Γ$, the term $M \; nat \; nat \; bool \; suc \; even$ has a type $nat \to bool$, and so is legal.
(b) (1) The term $λx : nat. even (suc \; x)$ is β-equivalent to $M \; nat \; nat \; bool \; suc \; even$ which we have shown has type $nat \to bool$, under any context.
So by Subject Reduction, $λx : nat. even (suc \; x)$ also has type $nat \to bool$, under any context, and so is legal.
(b) (2) Direct proof uses the following flag notation.
We have shown that for a context $Γ= nat:*, \; bool:*, \; suc: nat \to nat, \; even : nat \to bool$ the term $λx : nat. even (suc \; x)$ has type $nat \to book$, and so is legal.
Give a full (i.e. not-shortened) derivation in λ2 to show that the following term is legal; use the flag format. (cf. Example 3.1.1 (3).)
$$M ≡λα,β,γ : ∗. λf : α →β. λg : β →γ. λx : α. g(f x)$$
It is worth reviewing the summary of λ2 derivation rules in Figure 3.1.
The following is the derivation in flag format.
By showing there is a context $Γ$ such that $M$ has a type, are have shown $M$ is legal. The context here happens to be empty.
How many λ2-contexts are there consisting of the four declarations?
$$α : ∗$$
$$β : ∗$$
$$f : α →β$$
$$x : α$$
Definition 3.4.4 defines λ2 contexts:
(1) $∅$ is a λ2-context; $dom(∅) = ()$, the empty list.
(2) If $Γ$ is a λ2-context, $α ∈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)$.
Using this definition we have the following possibilities for valid λ2-contexts:
Prove the Compatibility cases in the proof of Lemma 2.11.5.
Lemma 2.11.5 (Subject Reduction) is
If $Γ ⊢L : ρ$ and if $L \to _{β} L^′$, then $Γ ⊢L^′ : ρ$.
The proof of Lemma 2.11.5 is done by induction on the generation of $L \to_β L^′$. That is, all modes of constructing $L \to_β L^′$ are considered, and for each, we show that indeed, given $Γ ⊢L : ρ$ each mode of generating $L \to _{β} L^′$ leads to $Γ ⊢L^′ : ρ$.
There are four modes of generating $L \to_β L^′$, as follows.
(1) Basis. $(λx : σ. M)N →_β M[x := N]$
(2) Compatibility. If $M →_β N$, then $MK →_β NK$
(3) Compatibility. If $M →_β N$, then $KM →_β KN$
(4) Compatibility. If $M →_β N$, then $λx. M →_β λx. N$
The textbook provides a proof for the (1) basis case. We'll provide the proofs for the compatibility cases (2-4).
(2) (Compatibility) If $M →_β N,$ then $MK →_β NK$
In this case $L ≡MK$ and $L^′ ≡NK$.
So, we aim to show that if $Γ ⊢MK : ρ$ and if $MK \to _{β} NK$, then $Γ ⊢NK: ρ$.
We assume:
We start with
$$Γ ⊢ MK : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ ⊢ M :γ→ ρ \quad \land \quad Γ ⊢K : γ$$
The induction hypothesis tells us
$$Γ⊢N: γ→ρ$$
And so, finally,
$$Γ⊢NK:ρ$$
So we have shown that if $Γ ⊢MK : ρ$ and if $MK \to _{β} NK$, then $Γ ⊢NK: ρ$.
(3) (Compatibility) If $M →_β N,$ then $KM →_β KN$
In this case $L ≡KM$ and $L^′ ≡KN$.
So, we aim to show that if $Γ ⊢KM : ρ$ and if $KM \to _{β} KN$, then $Γ ⊢KN: ρ$.
We assume:
We start with
$$Γ ⊢ KM : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ ⊢ K :γ→ ρ \quad \land \quad Γ ⊢M : γ$$
The induction hypothesis tells us
$$Γ⊢N: γ$$
And so, finally,
$$Γ⊢KN:ρ$$
So we have shown that if $Γ ⊢KM : ρ$ and if $KM \to _{β} KN$, then $Γ ⊢KN: ρ$.
(4) Compatibility. If $M →_β N$, then $λx. M →_β λx. N$
In this case $L ≡λx. M$ and $L^′ ≡λx. N$.
So, we aim to show that if $Γ ⊢λx. M : ρ$ and if $λx. M \to _{β} λx. N$, then $Γ ⊢λx. N: ρ$.
We assume:
We start with
$$Γ ⊢λx. M : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ, x:α ⊢ M :β \quad \land \quad ρ \equiv α→β$$
The induction hypothesis tells us
$$Γ, x:α ⊢N: β$$
And so, finally,
$$Γ ⊢λx. N : ρ$$
So we have shown that if $Γ ⊢λx. M : ρ$ and if $λx. M \to _{β} λx. N$, then $Γ ⊢λx. N: ρ$.
Prove Lemma 2.10.9 (the ‘Uniqueness of Types Lemma’).
(Hint: use Lemma 2.10.7 (the ‘Generation Lemma’).)
The Uniqueness of Types Lemma 2.10.9 is:
Assume $Γ ⊢M : σ$ and $Γ ⊢M : τ$. Then $σ ≡τ$.
The Generation Lemma 2.10.8 is:
(1) If $Γ ⊢x : σ$, then $x : σ ∈ Γ$
(2) If $Γ ⊢MN : τ$, then there is a type $σ$ such that $Γ ⊢ M : σ →τ$ and $Γ ⊢N : σ$
(3) If $Γ ⊢λx : σ. M : ρ$, then there is $τ$ such that $Γ, x : σ ⊢M : τ$ and $ρ ≡σ →τ$.
All λ-terms are the result of being constructed by one of the (var), (appl) or (abst) rules, as per the Derivation rules of Definition 2.4.5. This means we can use structural induction for each of these three modes of constructing an arbitrary λ-term.
(var)-rule
If $Γ⊢x:α$ and $Γ⊢x:β$ are the results of the (var) rule, then the context $Γ$ must contain $x:α$ and $x:β$, by the Generation Lemma.
To be well-formed, there can only be one $x$ in $Γ$ and so $x:α \equiv x:β$, which means $α \equiv β$.
(appl)-rule
If $Γ⊢AB:α$ and $Γ⊢AB:β$ are the results of the (appl) rule, then as premises to the (appl) rule we must have, by the Generation Lemma,
$$Γ⊢A:γ→α \quad \text{and} \quad Γ⊢B:γ$$
$$Γ⊢A:σ→β \quad \text{and} \quad Γ⊢B:σ$$
As an induction hypotheses we assume the uniqueness of types applies to these premises. That means
$$γ→α \equiv σ→β$$
$$γ \equiv σ$$
The first gives us $α \equiv β$. Thus we have shown that the type of $AB:α$ and $AB:β$ are the same.
(abst)-rule
If $Γ⊢λx:σ.M:α$ and $Γ⊢λx:σ.M:β$ are the results of the (abst) rule, then the premises to the (abst) rule must be, by the Generation Lemma,
$$Γ, x:σ⊢M:γ \qquad \text{and} \qquad {α \equiv σ→γ}$$
$$Γ, x:σ⊢M:ρ \qquad \text{and} \qquad {β \equiv σ→σ}$$
As an induction hypotheses we assume the uniqueness of types for these premises. This gives us $ γ \equiv ρ $, which immediately gives us $α \equiv β$.
Thus $Γ⊢λx:σ.M:α$ and $Γ⊢λx:σ.M:β$ have the same type.
By showing the uniqueness lemma holds for each mode of construction, we have shown it holds for arbitrary λ-terms.
Prove Lemma 2.10.8 (the ‘Subterm Lemma’).
Let's remind ourselves of Lemma 2.10.8, the Subterm Lemma.
If M is legal, then every sub-term of M is legal.
Definition 1.3.5 defines sub-terms of λ-terms.
(1) (Basis) $Sub(x) = {x}$, for each $x ∈V$.
(2) (Application) $Sub((MN)) = Sub(M)∪Sub(N)∪{(MN)}$.
(3) (Abstraction) $Sub((λx. M)) = Sub(M)∪{(λx. M)}$.
We start by noting that all λ-terms are at the top level one of three forms, a variable, an application, or an abstraction. We can therefore use the (var), (appl) and (abst) construction rules in a structural induction proof.
(var)-rule
We'll consider a precursor judgement $Γ⊢M:α$ from which the (var) rule results in $Γ⊢x:β$ where $x:β \in Γ$.
Our aim is show that if $x$ is legal, then every sub-term of $x$ is legal.
This is trivially true.
Note that we didn't need to use an induction hypothesis.
(appl)-rule
We'll consider two precursors $Γ⊢A;α→β$, and $Γ⊢B:α$. Here $A$ and $B$ are legal terms, a premise for the (appl) rule which gives us $Γ⊢AB:β$.
As an induction hypothesis we'll assume that if $A$ and $B$ are legal, then both their sub-terms are legal.
Our aim is to show that if $AB$ is legal, then every sub-term of $AB$ is legal.
Definition 1.3.5 tells us the sub-terms of $AB$ are $AB$ itself, and the sub-terms of $A$ and $B$. We have $AB$ is legal by assumption. The remain options $A$ and $B$ have legal sub-terms by the induction hypothesis.
(abst)-rule
We'll consider the precursor $Γ, x:α⊢M:β$. Here $M$ is a legal term, a premise for the (abst) rule which gives us $Γ⊢λx.M:α→β$.
As an induction hypotheses we'll assume that if $M$ is legal, then every sub-term of $M$ is legal.
Our aim is to show that if $λx.M$ is legal, then every sub-term of $λx.M$ is legal.
Definition 1.3.5 tells us the sub-terms of $λx.M$ is $λx.M$ itself, and the sub-terms of $M$. The term $λx.M$ is legal by assumption. The induction hypothesis tells us $M$ is legal and so are its sub-terms.
We've shown that if a λ-term is legal, then all its sub-terms are legal, but showing this is true for all three modes of constructing that λ-term.