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).