Monday, 21 July 2025

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.