Course Notes for Topics in Type Theory

Healfdene Goguen

23 April 1996

In this lecture I’ll finish the proof of strong normalization for System F. You can also find a proof of this in Girard’s book [1].

1 Typing for System F

1.1 Types and Terms

\begin{aligned}A, B, C & ∈ & Ty & ::= & α | A → B | Πα.B \\ M, N, P & ∈ & Tm & ::= & x | λx:A.M | M(N) | Λα.M | M(A) \end{aligned}

We also take X, Y, Z to be variables ranging over terms or types, and Σ to range over sets of type variables.

The free variables in M, FV(M), are those not bound by abstractions λx:A.M. The free type variables in M, FTV(M), are those not bound by type abstractions Λα.M. We write [N/x]M for the non-capturing term substitution of N for x in M, and [B/α]A for the non-capturing type substitution of B for α in A.

A pre-context Γ is a sequence of pairs of variables and types, Γ = x_{1}:A_{1}, …, x_{n}:A_{n}. A context Γ under Σ, notation ⊢_{Σ}Γ, is a pre-context such that the x_{i} are distinct and FTV(Γ) ⊆ Σ.

1.2 Judgements and Derivations

We formulate System F with a single judgement form, Γ ⊢_{Σ} M : A.

(Var) \frac{⊢_{Σ}Γ}{Γ ⊢_{Σ} x : A}  (λ) \frac{Γ, x:A ⊢_{Σ} M : B}{Γ ⊢_{Σ} λx:A.M : A → B}
(App)  \frac{Γ ⊢_{Σ} M : A → B Γ ⊢_{Σ} N : A}{Γ ⊢_{Σ} M(N) : B}
(Λ) \frac{Γ ⊢_{Σ∪\{α\}} M : A}{Γ ⊢_{Σ} Λα.M : Πα.A} (Ext) \frac{Γ ⊢_{Σ} M : Πα.B}{Γ ⊢_{Σ} M(A) : [A/α]B}

2 The Interpretation

We prove that any well-typed term in System F is strongly normalizing by constructing a model for the well-typed terms. In this section we give the basic definitions for the interpretation of types and show some simple lemmas about the interpretation.

We define strong normalization as before, as the least relation satisfying the rule:

\frac{∀N.M ⊳ N implies SN(N)}{SN(M)}

Let SN be the set of strongly normalizing terms.

We now give several properties that need to hold for the interpretation of types in our model construction.

(S1) If M ∈ S then SN(M).

(S2) If M ≡ xX_{1} … X_{n} and SN(M) then M ∈ S.

(S3) If M ≡ (λx:A.N)P X_{1} … X_{n}, SN(M) and ([P/x]N)X_{1} … X_{n} ∈ S then M ∈ S. If M ≡ (Λα.N)AX_{1} … X_{n}, SN(M) and ([A/α]N)X_{1} … X_{n} ∈ S then M ∈ S.

Following the literature, we call a set S which satisfies these properties a saturated set. We write SAT for the set of saturated sets. The first condition simply says that the set is indeed a set of strongly normalizing terms. The second condition says that variables are in saturated sets, which will allow us to descend beneath λ-abstractions. The third condition says that the set is closed under outermost expansions if the expansion is strongly normalizing. This is important because every reduction can be expressed as a sequence of outermost reductions, which is not used explicitly in this proof but is a crucial underlying motivation for the definition of saturated sets.

It is trivial to show that the set SN of strongly normalizing terms is a saturated set. Notice that elements of saturated sets are not necessarily well-typed, and saturated sets are not closed under reduction. The properties we require are only the minimal ones to get the proof to go through. Our saturated set conditions for System F are the same as they were for the simply typed lambda calculus, except that in (S3) we have two different β-expansions, one for abstraction over terms and the other for abstraction over types.

Again, we are thinking of saturated sets as potential interpretations of a type. We shall interpret types A under an assignment ρ of saturated sets to a finite set of type variables, where ρ(α) is the intended interpretation of α. We say that an assignment ρ of saturated sets to type variables covers A if FTV(A) ⊆ dom(ρ). We define the interpretation of any type A under ρ such that ρ covers A by induction on its structure:

[[α]]ρ =_{df} ρ(α)
[[A → B]]ρ =_{df} {M | SN(M) and ∀N ∈ [[A]]ρ.M(N) ∈ [[B]]ρ}
[[Πα.A]]ρ =_{df} {M | SN(M) and ∀B.∀R ∈ SAT .M(B) ∈ [[A]]ρ[α:=R]}

The definition of [[A → B]]ρ is the same as the interpretation of functions in the simply typed lambda calculus. The definition of [[Πα.A]]ρ requires some explanation. First, we again require that every term in the interpretation be strongly normalizing, so that property (S1) is trivial. Next, if ρ covers Πα.A then ρ[α:=R] covers A, where we can assume that α ∉ dom(ρ). Finally, we construct the interpretation according to the ways terms of that type can be used: an element of the interpretation of the quantification over types Πα.A is a term which when applied to types B yields a term in the interpretation of [B/α]A. However, we cannot actually write [[[B/α]A]]ρ, because that may not yet be defined, and indeed even [[B]]ρ may not yet be defined. Instead, we choose an arbitrary possible interpretation for B, the set R, and interpret A as though this were the interpretation of B. Notice that this requires a stronger logic than our proof of strong normalization for the simply typed lambda calculus, because we are quantifying over sets.

We first want to show that the interpretation of types has the properties we need in the proof.

Lemma 2.1 Let A be a type and let ρ be an assignment of saturated sets to type variables which covers A. Then [[A]]ρ is a saturated set.

Proof By induction on the structure of A:

• α. ρ(α) is a saturated set by assumption.

• A → B. As for the simply typed lambda calculus.

• Πα.A. (S1) holds trivially.

(S2). Suppose M ≡ xX_{1} … X_{n}, SN(M), and let B be a type and R be a saturated set. Then SN(M(B)), which implies M(B) ∈ [[A]]ρ[α:=R], so M ∈ [[Πα.A]]ρ.

(S3). Suppose M ≡ (λx:A.N)P X_{1} … X_{n}, SN(M) and ([P/x]N)X_{1} … X_{n} ∈ [[Πα.A]]ρ, and let B be a type and R be a saturated set. By inductive hypothesis we know that [[A]]ρ[α:=R] is a saturated set. Then SN(M(B)) by induction on SN(M), and ([P/x]N)X_{1} … X_{n}B ∈ [[A]]ρ[α:=R], so M(B) ∈ [[A]]ρ[α:=R] by inductive hypothesis, and hence M ∈ [[Πα.A]]ρ.

3 Substitution

We have introduced the new notion in System F of substitution on types, which did not exist in the simply typed lambda calculus. We need to show that the two possible interpretations of [B/α]A, namely [[[B/α]A]]ρ and [[A]]ρ[α:=[[B]]ρ], are the same. We need this in the proof of soundness when we come to the rule (Ext).

Lemma 3.1 Let A be a type and let ρ and ρ′ be assignments which cover [B/α]A such that ρ(α) = ρ′(α) for α ∈ FTV(A). Then [[A]]ρ = [[A]]ρ′.

Proof An easy induction on A.

Lemma 3.2 Let A and B be types and let ρ cover [B/α]A. Then [[[B/α]A]]ρ = [[A]]ρ[α:=[[B]]ρ].

Proof The proof follows by induction on A.

• α. Then [[[B/α]α]]ρ = [[B]]ρ.

• β, where α ≠ β. Then [[[B/α]β]]ρ = [[β]]ρ.

• C → D. By inductive hypothesis [[[B/α]C]]ρ = [[C]]ρ[α:=[[B]]ρ] and [[[B/α]D]]ρ = [[D]]ρ[α:=[[B]]ρ]. Hence

[[[B/α](C → D)]]ρ
= {M | SN(M) and ∀N ∈ [[[B/α]C]]ρ.M(N) ∈ [[[B/α]D]]ρ}
= {M | SN(M) and ∀N ∈ [[C]]ρ[α:=[[B]]ρ].M(N) ∈ [[D]]ρ[α:=[[B]]ρ]}
= [[C → D]]ρ[α:=[[B]]ρ]

• Πβ.C. We can assume that α ≠ β. By inductive hypothesis [[[B/α]C]]ρ′ = [[C]]ρ′[α:=[[B]]ρ′] for any assignment ρ′ which covers C. Hence

[[[B/α](Πβ.C)]]ρ
= {M | SN(M) and ∀D.∀R ∈ SAT .M(D) ∈ [[[B/α]C]]ρ[β:=R]}
= {M | SN(M) and ∀D.∀R ∈ SAT .M(D) ∈ [[C]]ρ[β:=R][α:=[[B]]ρ[β:=R]]}
= {M | SN(M) and ∀D.∀R ∈ SAT .M(D) ∈ [[C]]ρ[α:=[[B]]ρ][β:=R]}
= [[Πβ.C]]ρ[α:=[[B]]ρ]

where the third equality holds by Lemma 3.1 and because ρ[α:=R][β:=S] = ρ[β:=S][α:=R] if α ≠ β.

4 Soundness

We again introduce the interpretation of contexts Γ = x_{1}:A_{1}, …, x_{n}:A_{n}, [[Γ]]ρ, as parallel substitutions γ such that M_{i} ∈ [[A_{i}]]ρ. We also say that a tuple of the form σ = <α_{1} = A_{1}, …, α_{m} = A_{m}> is a type substitution for {α_{1}, …, α_{m}}, and we write M[σ] for the parallel substitution of types for type variables,

We can now show that we have a model for System F:

Theorem 4.1 If Γ ⊢_{Σ} M : A, ρ ∈ Σ → SAT , σ is a type substitution for Σ, and γ ∈ [[Γ]]ρ then M[σ][γ] ∈ [[A]]ρ.

Proof By induction on derivations Γ ⊢_{Σ} M : A.

• (Var). We know that x[σ][γ] = x[γ] ∈ [[A]]ρ by definition.

• (λ). As for the simply typed lambda calculus.

• (App). As for the simply typed lambda calculus.

• (Λ). Let ρ ∈ Γ → SAT , let σ = <α_{1} = A_{1}, …, α_{m} = A_{m}> for Σ = {α_{1}, …, α_{m}}, and let γ ∈ [[Γ]]ρ.

We first need to show that SN((Λα.M)[σ][γ]). Clearly ρ[α:=SN] covers Σ ∪ {α}, so by inductive hypothesis M[σ[α:=β]][γ] ∈ [[A]]ρ[α:=SN] for β fresh in Σ. Hence SN(M[σ[α:=β]][γ]) by (S1), so SN(Λβ.(M[σ[α:=β]][γ])), and Λβ.(M[σ[α:=β]][γ]) ≡ (Λα.M)[σ][γ].

Now, suppose B is a type and R is a saturated set. Then ρ[α:=R] covers Σ ∪ {α}, so M[σ[α:=B]][γ] ∈ [[A]]ρ[α:=R]. Hence (Λα.M)[σ][γ](B) ∈ [[A]]ρ[α:=R] by (S3), so (Λα.M)[σ][γ] ∈ [[Πα.A]]ρ.

• (Ext). Let ρ ∈ Σ → SAT , let σ = <α_{1} = A_{1}, …, α_{m} = A_{m}> for Σ = {α_{1}, …, α_{m}}, and let γ ∈ [[Γ]]ρ.

We know by inductive hypothesis that M[σ][γ] ∈ [[Πα.B]]ρ. Also, [[A]]ρ is a saturated set, so since ρ covers [A/α]B and ρ covers A, then ρ[α:=[[A]]ρ] covers B. Hence

(M(A))[σ][γ] = (M[σ][γ])(A[σ]) ∈ [[B]]ρ[α:=[[A]]ρ] = [[[A/α]B]]ρ

by definition of [[Πα.B]]ρ and the substitution lemma.

Corollary 4.2 If Γ ⊢_{Σ} M : A then SN(M).

Proof Suppose Γ = x_{1}:A_{1}, …, x_{n}:A_{n}. Let ρ be the function which for α ∈ FTV(Γ) ∪ FTV(A) returns SN, and let σ =_{df} <α_{1} = α_{1}, …, α_{m} = α_{m}> where Σ = {α_{1}, …, α_{m}}. Since SN is saturated, we know ρ ∈ Γ → SAT . Notice that the identity parallel substitution γ =_{df} <x_{1} = x_{1}, …, x_{n} = x_{n}> is in [[Γ]]ρ by (S2) and the definition of [[Γ]]ρ. Hence M[σ][γ] ≡ M ∈ [[A]]ρ, so SN(M) by (S1).

References

[1] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.