Exercise 2.7
(a) Prove the following by giving a kind of derivation, with the rules (func-appl) and (func-abst) described in Example 2.4.8:
If $f : A \to B$ and $g : B \to C$, then $g \circ f : A \to C$.
Note: $g \circ f$ is the composition of $f$ and $g$, being the function mapping $x$ to $g(f x)$.
(b) Give a derivation in natural deduction of the following expression, using the rules ⇒-elim and ⇒-intro described in Example 2.4.9:
$$(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$$
(c) Prove that the following pre-typed λ-term is legal, using the flag format:
$$λz : α. y(xz)$$
(d) Indicate the similarities between the derivations in (a), (b) and (c).
(a) We read $f : A \to B$ as $f$ is a member of the set $A \to B$, the set of all functions from $A$ to $B$.
We start by introducing a variable $x \in A$. This means we can apply the (func-appl) rule.
$$ (func-appl) : \frac{f: A \to B \; \land \; x \in A}{f(x) \in B} $$
This rules lets us conclude that $f(x)$ is a member of $B$.
Next we read $g : B \to C$ as $g$ is a member of the set $B \to C$, the set of all functions from $B$ to $C$. Since w now have $f(x) \in B$, we can use this in the next application of the (func-appl) rule.
$$ (func-appl) : \frac{g: B \to C \; \land \; f(x) \in B}{g(f(x)) \in C} $$
This tells us $g \circ f$ maps from $A \to C$.
(b) To show $P \implies Q$ we assume $P$ and derive $Q$.
Here this means we assume $(A \implies B)$ and derive $(B \implies C) \implies (A \implies C)$.
But to derive $(B \implies C) \implies (A \implies C)$ we assume $(B \implies C$ is true and derive $(A \implies C)$. And to do that, we assume $A$ is true and derive $C$.
We can do that because $A$ and $(A \implies B)$ gives us $B$ by the elimination rule. Similarly $B$ and $(B \implies C)$ gives us $C$ by the elimination rule.
So we have $(A \implies C)$ by the introduction rule, and $(B \implies C) \implies (A \implies C)$ by introduction again. One more introduction gives us $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$.
The above argument is a little informal. More properly, we need to keep track of assumptions and discharging them with the elimination rule.
The following proof tree provides this clarity.
(c) To prove the pre-typed λ-term is legal, we need to show there exists a context $Γ$ such that $Γ⊢M:ρ$ where $M$ is the term and $ρ$ is the type.
Let's consider the following context.
$$Γ := y: \beta \to \gamma, x: \alpha \to \beta, z:\alpha$$
We then apply the derivation rules from Definition 2.4.5:
$(i) \quad y: \beta \to \gamma, \; x: \alpha \to \beta, \; z:\alpha \quad \vdash \quad z:\alpha \quad $ (var)
$(ii) \quad y: \beta \to \gamma, \; x: \alpha \to \beta, \; z:\alpha \quad \vdash \quad x:\alpha \to \beta \quad $ (var)
$(iii) \quad y: \beta \to \gamma, \; x: \alpha \to \beta, \; z:\alpha \quad \vdash \quad xz: \beta \quad $ (appl) on (i) and (ii)
$(iv) \quad y: \beta \to \gamma, \; x: \alpha \to \beta, \; z:\alpha \quad \vdash \quad y:\beta \to \gamma \quad $ (var)
$(v) \quad y: \beta \to \gamma, \; x: \alpha \to \beta, \; z:\alpha \quad \vdash \quad y(xz):\gamma \quad $ (apppl) on (iv) and (iii)
$(vi) \quad y: \beta \to \gamma, \; x: \alpha \to \beta \quad \vdash \quad \lambda z:\alpha.y(xz) : \alpha \to \gamma \quad $ (var)
Thus we have shown the λ-term is legal because there exists a context, $Γ$ from which the λ-term is derivable and has a type $\alpha \to \gamma$.
The following shows this in flag format (click to enlarge).
(d) TODO
