free type variables in λ2 terms

Stream: new members

[rzeta0]

I'm working my way through Type Theory and Formal Proof, based in a recommendation here some months ago because I wanted to under how proof assistants like Lean work.

I'm stuck on the last exercise of Chapter 3 (second order lambda calculus). I'd welcome feedback on my attempted solution.

---

Exercise 3.21

Give a recursive definition for $FTV(A)$, the set of free type variables in $A$, for an expression $A$ in $\mathbb{T}2$ or in $Λ_{\mathbb{T}2}$.

Let's remind ourselves of the recursive definition for free variables in untyped λ-terms.

Definition 1.4.1 ($FV$, the set of free variables of a λ-term)

(1) (Variable) $FV(x) = \{x\}$

(2) (Application) $FV(MN) = FV(M)∪FV(N)$

(3) (Abstraction) $FV(λx. M) = FV(M) \{x\}$

Let's also remind ourselves of the sets $\mathbb{T}2$ and $Λ_{\mathbb{T}2}$.

$\mathbb{T}2 = \mathbb{V} |(\mathbb{T}2 →\mathbb{T}2) |(Π\mathbb{V} : ∗. \mathbb{T}2)$

$Λ_{\mathbb{T}2} = V|(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})|(Λ_{\mathbb{T}2}\mathbb{T}2)|(λV : \mathbb{T}2. Λ_{\mathbb{T}2})|(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$

Our recursive definition will need to cover all these cases. In the following section we'll consider each case, before rationalising the final definition.

---

$A$ in $\mathbb{T}2$, the λ2 Types

Let's consider the syntax cases for λ2 types.

$\mathbb{V}$. These are type variables, for which we usually use lower case greek symbols, eg $α, β, γ$. In this case the type variable is free, and so $$$$FTV(α)=\{α\}$$$$
$(\mathbb{T}2 →\mathbb{T}2)$. These are arrow types between other type variables, for example $α→β$. In this case the free type variables are those in the "from" and "to" expressions. So $$$$FTV(M→N)=FTV(M) \cup FTV(N)$$$$
$(Π\mathbb{V} : ∗. \mathbb{T}2)$. These are the abstractions over a single type variable. An example is $Πα:*.α→Mα$. In this case, the abstracted variable is bound, not free, and so $$$$FTV(Πα:*.M) = FTV(M) \setminus \{α\}$$$$

$A$ in $Λ_{\mathbb{T}2}$, the Pre-Typed λ2 Terms

Let's now consider the syntax cases for the pre-typed λ2-terms.

$V$. This is the simple case of a single term variable annotated with a type, eg $x$. These variables are pre-typed, and so the expression $x$ has no type variables in it. This means $$$$FTV(x)=\emptyset$$$$
$(Λ_{\mathbb{T}2}Λ_{\mathbb{T}2})$. This is the application of one term to another, for example $MN$. Here we have $$$$FTV(MN)=FTV(M) \cup FTV(N)$$$$
$(Λ_{\mathbb{T}2}\mathbb{T}2)$. This is the application of a term to a type, for example $Mα$. In this case $α$ is free, and so we have $$$$FTV(Mα)=FTV(M) \cup \{α\}$$$$
$(λV : \mathbb{T}2. Λ_{\mathbb{T}2})$. This is an abstraction over a term variable, for example $λx.M$. Since $x$ is not a type variable, we have $$$$FTV(λx.M)=FTV(M)$$$$
$(λ\mathbb{V} : ∗. Λ_{\mathbb{T}2})$. This is an abstraction over a type variable, for example $λα.M$. Here $α$ is not free, and so $$$$FTV(λα.M) = FTV(M) \setminus \{α\}$$$$

---

My Attempt At A Recursive Definition

Consolidating the above observations we have

(Type Variable) $FTV(α)=\{α\}$
(Term Variable) $FTV(x)=\emptyset$
(Arrow Type) $FTV(M→N)=FTV(M) \cup FTV(N)$
(Application) $FTV(MN)=FTV(M) \cup FTV(N)$
(Abstraction) $FTV(λα.N) = FTV(N) \setminus \{α\}$
(Abstraction) $FTV(Πα:*.M) = FTV(M) \setminus \{α\}$

[rzeta0]

Apologies in advance if the above is a little muddled. I'm self-teaching with no degree in maths / cs.

[rzeta0]

(deleted)

[rzeta0]

I've updated mu original question with my latest attempt at a solution, after some sleep and a walk.