Course Notes for Topics in Type Theory

Healfdene Goguen

April 23, 1996

1 Typing for λ^{→}

In this section we introduce the syntax of types and terms for the simply typed lambda calculus and present the judgements and rules of inference for the system λ^{→}. Mitchell [8] gives a thorough introduction to this system.

1.1 Types and Terms

We first introduce the types of the simply typed lambda calculus. We assume that there is only one base type o. For any two types A and B, we have the type A → B of functions from A to B.

We assume the existence of an infinite set V of variables. We use the usual language of terms for the simply typed lambda calculus: variables x if x ∈ V, abstraction λx:A.M, and application M(N). We identify terms which are equivalent up to the renaming of bound variables and write M ≡ N if M and N are equal in this way. We write FV(M) for the free variables in a term M, those variables not bound by abstractions. We denote the substitution of N for the free variable x in M by [N/x]M, where this substitution is defined to avoid the capture of free variables.

A pre-context is a sequence Γ = x_{1}:A_{1}, …, x_{n}:A_{n} of pairs of variables x_{i} ∈ V and types A_{i}. We denote the empty pre-context by (). We write dom(Γ) for the set {x_{1}, …, x_{n}}. A context is a pre-context where the x_{i} are distinct.

1.2 Judgements and Derivations

We have one judgement form in our presentation of the simply typed lambda calculus: Γ ⊢ M : A, meaning that the term M has type A in context Γ. The rules of inference for the system are given in Fig. 1.

(Var)  \frac{Γ context x:A ∈ Γ}{Γ ⊢ x : A}
(λ) \frac{Γ, x:A ⊢ M : B}{Γ ⊢ λx:A.M : A → B} (App) \frac{Γ ⊢ M : A → B Γ ⊢ N : A}{Γ ⊢ M(N) : B}

Figure 1: Typing Rules

2 Typed Operational Semantics

A typed operational semantics presents type theory from the perspective of computation instead of that of logical inference: we still need the full type information to derive the well-typedness of any term, but we replace the logical rules for application and abstraction by rules which instead express the reduction behavior of these terms in the calculus.

2.1 Standard Reduction

Standard reduction [3] is an important notion in the untyped lambda calculus: any reduction sequence can be expressed as a standard, or left to right, reduction sequence. In this section we introduce the system λ^{S}, a synthesis of this reduction and the semantic presentation λ^{→}. We shall use this system to study the metatheory of the simply typed lambda calculus. Because the reduction used in λ^{S} is universal with respect to reductions, the important results about the relationship between typed terms and reduction follow easily by reasoning in this system.

2.2 Judgements and Derivations

We now define the calculus λ^{S}. The judgement forms for λ^{S} and their intuitive meanings are:

• Γ ⊢^{S} M →^{nf} P : A, meaning that M has normal form P of type A in context Γ.

• Γ ⊢^{S} M →^{wh} N : A, meaning that M weak head reduces to N of type A in context Γ.

We write Γ ⊢^{S} J for an arbitrary judgement in λ^{S}. We also use the abbreviation Γ ⊢^{S} M : A for Γ ⊢^{S} M →^{nf} P : A when the normal form P is not important.

The typed operational semantics λ^{S} is defined by the rules of inference in Figs. 2 and 3.

(S-Base) \frac{Γ ⊢^{S} M_{i} →^{nf} P_{i} : A_{i} (1 ≤ i ≤ n)}{Γ ⊢^{S} x(M_{1}, …, M_{n}) →^{nf} x(P_{1}, …, P_{n}) : B} if x:A_{1} → … → A_{n} → B ∈ Γ

(S-λ)  \frac{Γ, x:A ⊢^{S} M →^{nf} P : B}{Γ ⊢^{S} λx:A.M →^{nf} λx:A.P : A → B}

(S-WH)  \frac{Γ ⊢^{S} M →^{wh} N : A Γ ⊢^{S} N →^{nf} P : A}{Γ ⊢^{S} M →^{nf} P : A}

Figure 2: Canonical Forms

(W-β) \frac{\begin{matrix}Γ ⊢^{S} λx:A.M : A → B_{1} → … → B_{n} → C & Γ ⊢^{S} N : A \\ Γ ⊢^{S} P_{i} : B_{i} (for 1 ≤ i ≤ n) \end{matrix}}{Γ ⊢^{S} (λx:A.M)(N, P_{1}, …, P_{n}) →^{wh} [N/x]M(P_{1}, …, P_{n}) : C}

Figure 3: Weak Head Reduction

3 Metatheory

In this section we present the essential metatheoretic properties for the simply typed lambda calculus. Our presentation is influenced by Luo’s thesis [7] and developments of Pure Type Systems [4, 9], although the formal system is considerably different. Since we shall eventually show the equivalence of λ^{S} and λ^{→}, all of the results for λ^{S} will transfer to λ^{→} as well.

3.1 Basic Definitions

We first introduce the basic notions of reduction and parallel substitution. The untyped reduction rules β and η are defined as usual:

\begin{matrix}(β) & (λx:A.M)(N) & β & [N/x]M \\ (η) & λx:A.M(x) & η & M & if x ∉ FV(M) \end{matrix}

If R is a relation on terms then we denote its compatible closure (allowing reduction to pass through all of the term constructors) by M ⊳_{R} N, its transitive closure by R^{+} and its reflexive and transitive closure by R^{∗}. Untyped reduction, M ⊳ N, is the compatible closure of βη.

A term M is normal if it has no reductions, that is if there is no N such that M ⊳ N. A term M satisfies the diamond property if M ⊳^{∗} N and M ⊳^{∗} P imply that there is a Q such that N ⊳^{∗} Q and P ⊳^{∗} Q.

A term is strongly normalizing if all reduction sequences starting from that term terminate. We therefore define the relation SN as the least relation satisfying the rule of inference:

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

We get the following induction principle for SN:

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

A pre-substitution for a finite set of variables S is a function from S to terms. We write a pre-substitution δ as <x_{1} := δ(x_{1}), …, x_{n} := δ(x_{n})>, for S = x_{1}, …, x_{n}. If δ is a pre-substitution for dom(Γ) then we write M[δ] for the result of simultaneously substituting the values for the variables in the domain of δ:

M[δ] =_{df} [δ(x_{1}), …, δ(x_{n})/x_{1}, …, x_{n}]M

If ϕ is a pre-substitution for Φ then the composition of ϕ and δ, ϕ ∘ δ, is

(ϕ ∘ δ)(x) =_{df} δ(x)[ϕ]

We write δ[x:=M] for the extended pre-substitution for dom(Γ, x:A). If Δ has all components of Γ then we define the substitutions weak_{Γ}^{Δ}(x) =_{df} x for x ∈ dom(Γ), and id_{Γ} =_{df} weak_{Γ}^{Γ}.

A substitution δ from Δ to Γ is a pre-substitution for dom(Γ) such that Δ ⊢^{S} δ(x) : A for each x:A ∈ Γ. A renaming δ from Δ to Γ is a substitution from Δ to Γ such that δ(x) = y, where y ∈ V, for each x:A ∈ Γ.

An important property of renamings is that if δ is a renaming from Δ to Γ and ϕ is a renaming from Φ to Δ then ϕ ∘ δ is a renaming from Φ to Γ. This property is not straightforward for arbitrary substitutions, and we shall only know it as a consequence of our final soundness theorem.

3.2 Basic Metatheory

In this section we state the basic metatheoretic properties of λ^{S}. The results are for the system λ^{S}because we shall transfer the results from this system to λ^{→} by soundness and completeness results.

You can find the proofs in [5, 6].

Lemma 3.1 (Free Variables) If Γ ⊢^{S} M →^{nf} P : A then FV(M) ⊆ dom(Γ) and FV(P) ⊆ dom(Γ).

Lemma 3.2 (Generation) Any judgement which is derivable in λ^{S} has a uniquely determined last rule of inference.

Lemma 3.3 (Uniqueness of Normal Forms) If Γ ⊢^{S} M →^{nf} P : A and Γ ⊢^{S} M →^{nf} Q : B then P ≡ Q and A = B.

This lemma states that the operational semantics is deterministic. The system also has the stronger property of being syntax directed, meaning that for each context Γ and term M there are at most one term M and type A such that Γ ⊢^{S} M →^{nf} P : A, but we do not need this fact explicitly.

Lemma 3.4 (Context) If Γ ⊢^{S} J then Γ is a context.

Lemma 3.5 (Completeness) If Γ ⊢^{S} M →^{nf} P : A then Γ ⊢ M : A and Γ ⊢ P : A.

Corollary 3.6 (Thinning) If Γ ⊢^{S} J and Δ is a context with all components of Γ then Δ ⊢^{S} J.

Lemma 3.7 (Strengthening) If Γ_{0}, z:C, Γ_{1} ⊢^{S} M →^{nf} P : A and z ∉ FV(M) then Γ_{0}, Γ_{1} ⊢^{S} M →^{nf} P : A.

3.3 λ^{S} and Reduction

The calculus λ^{S} is a synthesis of standard reduction and the typing rules from the simply typed lambda calculus, which makes it a powerful tool for showing results about the relationship between typing in λ^{S} and untyped reduction.

Lemma 3.8 (Adequacy for Reduction)

• If Γ ⊢^{S} M →^{nf} P : A then M ⊳^{∗} P and P is normal.

• If Γ ⊢^{S} M →^{wh} N : A then M ⊳_{β} N.

Corollary 3.9 If Γ ⊢^{S} M →^{nf} P : A and M is normal then M ≡ P.

We now prove a general lemma about the relationship between untyped reduction and the system λ^{S}. This lemma will imply the important properties of strong normalization, subject reduction and the diamond property.

Definition 3.10 The predicate S_{Γ}^{P,A}(M) is defined as the least relation such that S_{Γ}^{P,A}(M) holds if:

• Γ ⊢^{S} M →^{nf} P : A,

• M ⊳ N implies S_{Γ}^{P,A}(N) for all N.

This definition is closely related to the definition of strong normalization in Altenkirch’s thesis [1], although we have added type information. We have used this definition because of the similarity of the proofs of subject reduction, strong normalization and the diamond property in this setting.

Notice that S_{Γ}^{P,A}(M) has the following induction principle:

\frac{∀M.(Γ ⊢^{S} M →^{nf} P : A and ∀N.M ⊳ N implies (S_{Γ}^{P,A}(N) and P(N))) imply P(M)}{∀M.S_{Γ}^{P,A}(M) implies P(M)}

We can also show the following properties straightforwardly:

• If S_{Γ}^{P,A}(M) then Γ ⊢^{S} M →^{nf} P : A.

• Strong Normalization. If S_{Γ}^{P,A}(M) then SN(M).

• Subject Reduction. If S_{Γ}^{P,A}(M) and M ⊳ N then S_{Γ}^{P,A}(N).

• If S_{Γ}^{P,A}(M) and M ⊳^{∗} N then S_{Γ}^{P,A}(N).

• Church–Rosser. If S_{Γ}^{Q,A}(M), M ⊳^{∗} N and M ⊳^{∗} P then N ⊳^{∗} Q and P ⊳^{∗} Q.

Lemma 3.11 (Reduction)

• If Γ ⊢^{S} M →^{nf} P : A then S_{Γ}^{P,A}(M).

• If Γ ⊢^{S} M →^{wh} N : A and S_{Γ}^{P,A}(N) then S_{Γ}^{P,A}(M).

All of the important results about reduction are corollaries to Adequacy for Reduction, using the properties we established above.

Corollary 3.12 (Strong Normalization for λ^{S}) If Γ ⊢^{S} M →^{nf} P : A then M is strongly normalizing.

Corollary 3.13 (Subject Reduction for λ^{S}) If Γ ⊢^{S} M →^{nf} P : A and M ⊳^{∗} N then Γ ⊢^{S} N →^{nf} P : A.

Corollary 3.14 (Diamond Property for λ^{S}) If Γ ⊢^{S} M →^{nf} Q : A, M ⊳^{∗} N and M ⊳^{∗} P then N ⊳^{∗} Q and P ⊳^{∗} Q.

References

[1] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, Nov. 1993.

[2] D. Aspinall and A. Compagnoni. Subtyping dependent types, July 1996. To appear in LICS 1996.

[3] H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North Holland, revised edition, 1984.

[4] H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbai, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1991.

[5] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994.

[6] H. Goguen. Typed operational semantics. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 186–200. Springer–Verlag, 1995.

[7] Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, Nov. 1990.

[8] J. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. North Holland, 1990.

[9] L. van Benthem Jutting, J. McKinna, and R. Pollack. Typechecking in pure type systems. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programming. Springer–Verlag, 1993.