Exercise 2.10
Prove that the following pre-typed λ-terms are legal, by giving derivations in (shortened) flag notation.
(a) $xz(yz)$
(b) $λx : (α →β) →β. x(yz)$
(c) $λy : α. λz : β →γ. z(xyy)$
(d) $λx : α →β. y(xz)z$
(a) All of the variables are not pre-typed, they are all free variables. We need to show the λ-term is type-able by finding suitable types for these free variables.
Before we start, let's parenthesise the term for greater clarity as $(xz)(yz)$.
Let's start with $x:A, y:B, z:C$. Since $y$ is applied to $z$, we have $B=C \to D$. Similarly, since $x$ is applied to $z$, we have $A = C \to E$. And since $xz$ is applied to $yz$, we have $E=D \to F$.
Summarising, and renaming the variables, we have
$$ x: α \to β \to γ, y: α \to β, z: α \quad \vdash \quad xz(yz) : γ$$
The following flag notation derivation confirms the λ-term is legal.
The λ-term is legal because there exists a context such that the term has a type (is type-able).
(b) We're given $x:(α →β) →β$, so let's set $y:B, z:C$. Since $y$ is applied to $z$, we have $B=C \to D$. And since $x$ is applied to $(yz)$ we have $(α →β) →β = D \to E$. So $E=β$ and $D=(α→β)$. Considering $B$ again, we have $B=C \to (α→β)$.
In summary, and renaming the variables, we have
$$ y: γ → (α →β), z: γ \quad \vdash \quad λx : (α →β) →β. x(yz) : ((α →β) →β) → β$$
The following flag notation derivation confirms the λ-term is legal.
(c) We're given $y : α$ and $z : β →γ$, so let's set $x:A$. Since $x$ is applied to $y$, we have $A=α →B$. We have $xy$ applied to $y$ which means $B=α→D$. Finally, $z$ is applied to $(xyy)$ so $β→γ$ must be the same as $D→γ$. This means $D=β$, $B=α→β$, and $A=α→α→β$.
In summary, and renaming variables, we have
$$ x:α→α→β \quad \vdash \quad λy : α. λz : β →γ. z(xyy) : α→(β →γ) →γ $$
The following flag notation derivation confirms the λ-term is legal.
(d) We're given $x:α→β$, so let's set $y:B, z:C$. Since $x$ is applied to $z$ we have $C=α$. Since $y$ is applied to $(xz)$ we have $B=β→D$. Finally $y(xz)$ is applied to $z$ we have $D=α→E$.
In summary, and renaming variables, we have
$$ λy: β→α→γ, z:α \quad \vdash \quad λx:α→β.y(xz)z: (α→β)→γ $$
The following flag notation derivation confirms the λ-term is legal.
