A Formalization of the Theory of Pure Type Systems in Coq

Robin Adams

University of Manchester

                           radams@cs.man.ac.uk

Abstract. We describe a recent formalization of several results from the metatheory of Pure Type Systems (PTSs) in Coq, including Subject Reduction, Uniqueness of Types in a functional PTS, and the difficult proof of Strengthening. The terms of the PTS are represented by an inductive family of types: ”term n” is the type of all terms with at most n free variables. This representation of terms has often been used to study syntax and substitution, but not the metatheory of a formal system. We show how it requires many metatheorems to be stated in a somewhat unfamiliar ”big-step” form, but then allows for very elegant and direct proofs.

1 Introduction

About six months ago, late in 2004, I decided to formalise a technically complex proof of a result of mine in the theory of Pure Type Systems (PTSs) [1], in order to guarantee its correctness. I looked around for formalizations of the metatheory of PTSs or similar type systems that I could use or adapt. I found two major developments [2, 3], and was dissatisfied with both of them. To use either would have involved spending much time on technical details that were irrelevant to the main proof ideas. While this is inevitable to some extent whenever one formalises a piece mathematics, it seemed worth spending some time searching for another approach with which the technicalities would be fewer.

There came to my mind an idea I had first been introduced to in a talk by Peter Aczel [4]: that of representing the terms of the lambda calculus, or any syntax with binding, as a nested data type. I decided to experiment with a formalization based on such a representation of the grammar. To my delight, I found myself making very rapid progress: the technicalities involved were indeed fewer, or at least were better handled by Coq’s automation.

The formalization often dealt more easily with what I came to call “big-step” operations and theorems, as opposed to the “small-step” form which was usually more familiar. For example, I quickly found that it is much easier to define the operation of substituting for all variables simultaneously, rather than for a single variable. The Substitution Lemma was also more easily proven when stated in these terms. So some thought was often necessary as to the best form for a definition or theorem to take; however, once the correct form for a theorem had been found, the proof usually proceeded very quickly, simply and directly.

Moreover, the formalization had to my mind a more type-theoretic flavour than either of the two cited above: the objects with which one was dealing were objects one might reasonably expect to find when dealing with the metatheory of a type theory, rather than low-level aspects of the mechanisms of the formalization.

Unfortunately, after formalizing many results in the basic theory of PTSs, I was not able to spare the time to complete the formal proof of the result in [1], although I do plan to return to this task when time permits. However, I hope that the work I have completed so far will be of interest to others — either those who wish a formalization of PTSs they can use, or those who wish to build a similar formalization of a different system. There may also be some independent interest in seeing what form the results in the metatheory of a formal system take when one represents the grammar of the system as a nested data type.

We shall not be too strict in this paper with accuracy when giving the details of the formalization: we shall freely mix Coq keywords with informal mathematical notation, and shall reverse the order of the arguments of a function if we feel it aids readability. (For example, the type we here denote by string m n would be the type string n m in the formalization.) This paper is a guide to the ideas used in the formalization, not a documentation of the formalization itself.

For those who wish to examine the formalization, the source code and doc-

umentation is available at http://www.cs.man.ac.uk/~radams/coqPTS.

2 Pure Type Systems

The theory of Pure Type Systems (PTSs) is a theory dealing with a large number of type theories — it is the closest thing yet developed to a general theory of type theories. It is not too much of an exaggeration to say that any theory whose only type constructor is Π can be defined as a PTS: this includes the simply-typed lambda calculus, the Calculus of Constructions, System F, and so forth.

The theory of PTSs is an excellent example of a beautiful mathematical theory. It begins with a simple set of definitions, from which follow a rich body of theorems, some basic, some deep. The way that a PTS is specified could not be simpler: a set, with a binary and ternary relation. The set of terms is then given by a grammar with just five constructors, and the derivable judgements given by just seven rules of deduction.

The best reference for the theory of PTSs is still Barendregt [5]. The formalization follows the development in this paper very closely. We prove all the results given there for arbitrary PTSs, from Lemma 5.2.8 to Corollary 5.2.22. (Lemma 5.2.7, the Free Variables Lemma, follows automatically from the way we define syntax.) We also prove the Strengthening Lemma, following the proof given in van Bentham Jutting [6].

3 Terms as a Nested Data Type

The idea of representing terms as a nested data type first appeared in Bellegarde and Hook [7]. It has been used several times for the study of syntactic properties and operations, such as substitution and β-reduction; see, for example, Altenkirch and Reus [8] or Bird and Paterson [9], the latter of which even deals with the simply-typed lambda calculus. However, this representation of syntax seems never before to have been used in the metatheory of a typing system where the typing judgements are given by a set of rules of deduction.

We shall briefly summarize the ideas behind this representation here; more details can be found in the three papers cited above. We wish to represent, in some type theory, the terms of some formal system whose syntax involves one or more binding constructor. Rather than defining one type whose objects are to represent these terms, we define a family of types

T_{V}

for every type V in some universe. The objects of type T_{V} represent those terms that can be formed using the objects of type V as free variables.

For example, let us assume we have defined, for every type X, a type X_{⊥} consisting of a copy ↑ x of each x : X, together with one extra object, ⊥. We can then represent the terms of the untyped lambda calculus by the inductive family T_{V} whose constructors are as follows.

{x : V \atop var x : T_{V}}  {M : T_{V_{⊥}} \atop λM : T_{V}}  {M : T_{V} N : T_{V} \atop MN : T_{V}}

The constructor λ takes a term M whose free variables are taken from V_{⊥}, binds the variable ⊥, and returns a term λM whose free variables are taken from V.

The definition of substitution takes the following form. We aim to define, for every term M : T_{U} and every substitution function σ : U → T_{V}, the term M[σ] : T_{V}, the result of substituting for each variable u : U the term ρ(u) : T_{V}. This is our first encounter with a theme that shall appear many times in this formalization: it is easier to deal with every variable in a given type V at once (“big-step” operations and theorems) than with a single variable.(“small-step” operations and theorems). The small-step version can always be recovered later as a special case of the big-step version.

The definition of substitution that we would naturally write down is as follows.

x[σ] ≡ σ(x)
(MN)[σ] ≡ M[σ]N[σ]
(λM)[σ] ≡ λM [ \begin{matrix}⊥ & ↦ & ⊥ \\ ↑ x & ↦ & σ(x)[y ↦↑ y] \end{matrix} ]

(Here and henceforth, we are omitting the constructor var.)

It is possible to prove that this recursion terminates. However, this definition cannot be made directly in Coq, as it is not a definition by structural recursion. But we can define the special case where ρ always returns a variable. We thus define the operation of replacement; given a term M : T_{U} and a renaming function ρ : U → V, we define the term M{ρ} : T_{V}, the result of replacing each variable u : U with ρ(u) : V, thus:

x{ρ} ≡ ρ(x)
(MN){ρ} ≡ M{ρ}N{ρ}
(λM)\{ρ\} ≡ λM \{ \begin{matrix}⊥ & ↦ & ⊥ \\ ↑ x & ↦ & ↑ ρ(x) \end{matrix} \}

Substitution can then be defined as follows: for σ : U → T_{V},

x[σ] ≡ σ(x)
(MN)[σ] ≡ M[σ]N[σ]
(λM)[σ] ≡ λM [ \begin{matrix}⊥ & ↦ & ⊥ \\ ↑ x & ↦ & ρ(x)\{y ↦↑ y\} \end{matrix} ]

Altenkirch and Reus [8] show how the type operation T , the variable constructor var, and the substitution operation [ ] form a Kleisli triple, a concept closely related to that of a monad. Bird and Paterson [9] give the monadic structure explicitly: the substitution operation can be split into a mapping T_{U} → T_{T_{V}}, followed by a “folding” operation T_{T_{V}} → T_{V}; the type operator T , together with the constructor var, the replacement operation { } and this folding operation, form a monad.

For this formalization, we modify this constuction slightly. Rather than allowing any type V : Set to be used as the type of variables, we only use the members of a family F_{n} of finite types, F_{n} having n distinct canonical members. We then define the type T_{n} of terms that use the objects of F_{n} as free variables. We shall refer to this representation of syntax as “nat-indexed terms”. As the objects of F_{n} come in a canonical order, the result syntax is very close to de Bruijn notation.

4 Description of the Formalization

4.1 Grammar

We define a family of finite types F_{n} (n : IN), F_{n} having exactly n distinct canonical objects. This could be defined directly as an inductive family:

{n : IN \atop ⊥ : F_{n+1}}  {x : F_{n} \atop ↑ x : F_{n+1}}

However, it was found that case analysis on an object of type F_{n} is easier in Coq if F is instead defined as a recursive function thus:

F_{0} = ∅
F_{n+1} = (F_{n})_{⊥}

Here, ∅ (empty) is the empty type, and X_{⊥} (option X) is a type consisting of a copy ↑ x of each object x : X together with one extra object ⊥; both of these are provided by the Coq library. (In general, when working with Coq, it seems to be advisible to use several simple inductive definitions rather than one complex one. We shall be faced with a similar choice when we come to define the types of contexts.)

We then define the family of types T_{n} of terms using the objects of type F_{n} as free variables, for n : IN:

{x : F_{n} \atop x : T_{n}}  {s : S \atop s : T_{n}}  {M : T_{n} N : T_{n} \atop MN : T_{n}}  {A : T_{n} B : T_{n+1} \atop ΠAB : T_{n}}  {A : T_{n} M : T_{n+1} \atop λAM : T_{n}}

We proceed to define the replacement operation { } and the substitution operation [ ], as discussed in the previous section. We can then prove the following versions of the Substitution Lemma.

Lemma 1. Let M : T_{m}; ρ : F_{m} → F_{n}; ρ′ : F_{n} → F_{p}; σ : F_{m} → T_{n}; and σ′ : F_{n} → T_{p}. Then

M{ρ}{ρ′} ≡ M{ρ′ ∘ ρ}
M{ρ}[σ′] ≡ M[σ′ ∘ ρ]
M[σ]{ρ′} ≡ M[x ↦ σ(x){ρ′}]
M[σ][σ′] ≡ M[x ↦ σ(x)[σ′]]

4.2 Reduction and Conversion

We define the relation of parallel one-step reduction, ▷, which has type Πn : IN.T_{n} → T_{n} → Prop, thus:

{x : F_{n} \atop x ▷ x}  {s : S \atop s ▷ s}  {M ▷ M′ N ▷ N′ \atop MN ▷ M′N′}

{A ▷ A′ B ▷ B′ \atop ΠAB ▷ ΠA′B′}  {A ▷ A′ M ▷ M′ \atop λAM ▷ λA′M′}  {M ▷ M′ N ▷ N′ \atop (λAM)N ▷ M′[N′]}

The relation of reduction, ↠, is defined to be the transitive closure of ▷, and the relation of convertibility, ≃, is defined to be the symmetric, transitive closure of ▷.

We are then able to prove that ▷ satisfies the diamond property, and deduce the two forms of the Church-Rosser Theorem:

Lemma 2. For M, N, P : T_{n}, if M ▷ N and M ▷ P, then there exists Q : T_{n} such that N ▷ Q and P ▷ Q.

Theorem 1. For M, N, P : T_{n}, if M ↠ N and M ↠ P, then there exists Q : T_{n} such that N ↠ Q and P ↠ Q.

Theorem 2. For M, N : T_{n}, if M ≃ N, then there exists P : T_{n} such that M ↠ P and N ↠ P.

4.3 Pure Type Systems

Contexts. We now define the type C_{n} of contexts with domain F_{n}. Just as for F_{n}, in order to make case analysis easier, we do not define this as an inductive family, but rather by recursion on n as follows:

C_{0} = 1
C_{n+1} = C_{n} × F_{n}

Here, 1 (unit) is a type with a unique canonical element ∗ (tt), and A × B (prod A B) is the Cartesian product of A and B, both provided by the Coq library.

We can define the function typeof, with type Πn : IN.F_{n} → C_{n} → T_{n}, which looks up the type of the variable x : F_{n} in the context Γ : C_{n}. We write Γ (x) for typeof x Γ. Thus, the situation that we would describe on paper by “x : A ∈ Γ ” is expressed in our formalization by Γ (x) ≡ A.

The typeof function is defined by recursion on n as follows (the case n = 0 being vacuous):

⟨Γ, A⟩(⊥) ≡ A{↑}
⟨Γ, A⟩(↑ x) ≡ Γ (x){↑}

Rules of Deduction. We declare the axioms A and rules R of the arbitrary PTS with which we are working as parameters:

                    Parameter A : S → S → Prop
                  Parameter R : S → S → S → Prop

We are now finally able to defined the typing relation ⊢ of the PTS. This relation has type

Πn : IN.C_{n} → T_{n} → T_{n} → Prop

When given a context Γ : C_{n} and terms M, A : T_{n}, it returns the proposition “The judgement Γ ⊢ M : A is derivable”. It is defined as an inductive relation, and its constructors are simply the rules of deduction of a PTS (see Fig. 1).

Subcontext Relation. The definition of the subcontext relation is the first place where our formalization differs significantly from the informal

When we use named variables, the subcontext relation is defined as follows: the context Γ is a subcontext of Δ iff, for every variable x and type A, if x : A ∈ Γ then x : A ∈ Δ. We could think of a function giving, for each entry x : A in Γ, the position at which x : A occurs in Δ. (See Fig. 2 (a).)

If Γ is of length m and Δ of length n, then we can write the definition in the following form:

Γ is a subcontext of Δ iff there exists a function ρ : {1, …, m} → {1, …, n} such that, if the ith entry of Γ is x : A, then the ρ(i)th entry of Δ is x : A.

axioms :  ∗ ⊢ s : t  (A s t)

start :  {Γ ⊢ A : s \atop Γ, A ⊢ ⊥ : A\{↑\}}

weakening :  {Γ ⊢ A : B Γ ⊢ C : s \atop Γ, C ⊢ A\{↑\} : B\{↑\}}

product :  {Γ ⊢ A : s_{1} Γ, A ⊢ B : s_{2} \atop Γ ⊢ ΠAB : s_{3}}  (R s_{1} s_{2} s_{3})

application :  {Γ ⊢ M : ΠAB Γ ⊢ N : A \atop Γ ⊢ MN : B [ \begin{matrix}⊥ & ↦ & N \\ ↑ x & ↦ & x \end{matrix} ]}

abstraction : {Γ, A ⊢ M : B Γ ⊢ A : s_{1} Γ, A ⊢ B : s_{2} \atop Γ ⊢ λAM : ΠAB} (R s_{1} s_{2} s_{3})

conversion :  {Γ ⊢ M : A Γ ⊢ B : s \atop Γ ⊢ M : B}  (A ≃ B) .

Fig. 1. Rules of deduction of a Pure Type System

In our formalization, we cannot use the same definition, as the variables of F_{n} come in a fixed order: ⊥, ↑ ⊥, ↑↑ ⊥, …. But we can still talk of functions mapping positions in one context to positions in another: these are the renaming functions ρ : F_{m} → F_{n}. (See Fig. 2 (b).)

We can therefore define the relation: Γ is a subcontext of Δ under the renaming ρ. This means that, if we identify each variable x in Γ with the variable ρ(x) in Δ, then the entry with subject x in Γ is the same as the entry with subject ρ(x) in Δ. More precisely:

Γ is a subcontext of Δ under ρ, Γ ⊆_{ρ} Δ,‘ iff, for each variable x in F_{n}, if x : A occurs in Γ, then ρ(x) : A{ρ} occurs in Δ.

In terms of the typeof function, this becomes:

Definition 1. Let Γ : C_{m}, Δ : C_{n}, and ρ : F_{m} → F_{n}. Γ is a subcontext of Δ under ρ, Γ ⊆_{ρ} Δ, iff

(∀x : F_{m})Δ(ρ(x)) ≡ Γ (x){ρ}

Note that the relation we have defined allows contraction: ρ may map two different variables x and y to the same variable in F_{n} (in which case x and y must have the same type in Γ). If we wish to exclude contraction, we shall use the relation “Γ ⊆_{ρ} Δ ∧ ρ is injective”.

With this definition, the Weakening Lemma becomes:

Named Variables — Γ ⊆ Δ:

∀x, A(x : A ∈ Γ ⇒ x : A ∈ Δ)

[figure: Γ ≡ x : A, y : B, …, z : C; Δ ≡; …,; x : A,; …,; z : C,; …,; y : B]

Nat-indexed Terms — Γ ⊆_{ρ} Δ:

∀x Γ (x){ρ} ≡ Δ(ρ(x))

[figure: Γ ≡  ↑^{n} ⊥ : A, ↑^{n−1} ⊥ : B,  …,  ⊥ : C; ρ; Δ ≡; …,; ρ(↑^{n} ⊥) : A{ρ},; …,; ρ(↑^{n−1} ⊥) : C{ρ},; …,; ρ(⊥) : B{ρ}]

Fig. 2. The definition of subcontext

Lemma 3. If Γ ⊆_{ρ} Δ, Γ ⊢ M : A, and Δ is valid, then Δ ⊢ M{ρ} : A{ρ}.

Just as we are using big-step notions of replacement and substitution, so our Weakening Lemma takes a big-step form. The corresponding small-step form is

If Γ, Δ ⊢ M : A and Γ ⊢ B : s, then Γ, x : B, Δ ⊢ M : A (where x is not free in Δ, M or A).

The particular instances of the small-step Weakening Lemma that we need to use in later proofs are easily derived as special cases of the big-step version.

The big-step version of the Weakening Lemma is not particularly novel: it appears in many informal and formal developments. The form that the next result takes is probably more surprising:

Substitution Lemma. What form should the Substitution Lemma take, given that we are using substitution mappings σ : F_{m} → T_{n}? A moment’s thought will show that, with named variables, the result would read as follows:

If x_{1} : A_{1}, …, x_{m} : A_{m} ⊢ M : B and
Γ ⊢ σ(x_{1}) : A_{1}[σ]
⋮
Γ ⊢ σ(x_{m}) : A_{m}[σ]
then Γ ⊢ M[σ] : B[σ].

(For the case m = 0, we would need to add the hypothesis “Γ is valid”.)

It is now quite clear how the result should read with nat-indexed terms. Let us define the relation Γ ⊧ σ :: Δ (σ satisfies the context Δ under Γ) to mean

∀x : F_{m}.Γ ⊢ σ(x) : Δ(x)[σ] .

Then our big-step Substitution Lemma reads:

Lemma 4 (Substitution). If Δ ⊢ M : B, Γ ⊧ σ :: Δ, and Γ is valid, then Γ ⊢ M[σ] : B[σ].

This is proven by induction on the derivation of Δ ⊢ M : B.

Subject Reduction. Subject Reduction similarly takes a big-step form. Subject Reduction is traditionally stated in the form:

If Γ ⊢ M : A and M ↠ N, then Γ ⊢ N : A.

In our formalization, the most convenient form in which to prove Subject Reduction is as follows. We extend the notion of parallel one-step reduction to contexts, by making the following definition:

Definition 2. Define the relation of parallel one-step reduction, ▷, on C_{n} as follows: Γ ▷ Δ iff ∀x : F_{n}.Γ (x) ▷ Δ(x).

We can now prove:

Theorem 3 (Subject Reduction). If Γ ⊢ M : A, Γ ▷ Δ and M ▷ N, then Δ ⊢ N : A.

This is proven directly by induction on Γ ⊢ M : A. The usual form of Subject Reduction follows quite simply.

Other Results. The formalization also contains proofs of Context Conversion, the Generation lemmas, Type Validity, Predicate Reduction and the Uniqueness of Types result for functional PTSs. There is little to say about any of these results: Context Conversion takes the expected big-step form, while the others take the same form, and the proofs follow the same lines, as the paper development.

4.4 The Proof of the Strengthening Theorem

The proof of the Strengthening Theorem in van Bentham Jutting’s paper [6] is a technically complex proof, and a very good, tough test of any formalization of the theory of PTSs.

Perhaps surprisingly, the feature that makes the proof most difficult to formalise when using nat-indexed terms is the use of terms of the form

ΛΔ.M and ΠΔ.M

where Δ is a string of abstractions

Δ ≡ ⟨x_{1} : A_{1}, …, x_{n} : A_{n}⟩

We shall need to build the type of strings in such a way that these operations Λ and Π can be defined. A closer look at the proofs in [6] reveals that we shall also need an operation for concatenating a context with a string; that is, given a context Γ and a string Δ, producing a context (Γ, Δ). We must also be able to apply a substitution to a string.

Several different approaches to these definitions were tried before the ones described below were found. As a general principle, it was found to be important to avoid arithmetic within types at all costs. Once addition appeared within the type of some operator, one inevitably found oneself, sooner or later, in some impossible situation, such as requiring a term to have type T_{m+Sn} at one point in a formula and type T_{Sm+n} at another point in the same formula.

For example, there are zeveral possible ways to define the family of types of strings. We could define

– string1 m p — the type of all strings of length p whose initial term has type T_{m}

– string2 n p — the type of all strings of length p whose final term has type T_{n}

– string3 m n — the type of all strings whose initial term has type T_{m} and whose final term has type T_{n−1}. (It follows necessarily that m ≤ n and the string has length n − m.)

Only with the third choice can we avoid arithmetic in the type of the Π and Λ operators. For example, if we chose to use string1, the Π operator would need to have the type

Πm, p : IN.string1 m p → T_{m+p} → T_{m} .

With substitution, it is far more difficult to find a set of definitions that avoids the need for addition within some type. A subtle solution was eventually found, and is described below.

Strings. We define the inductive family of types string. If n ≤ m, the type string m n is the type of all strings

Δ ≡ ⟨A_{m}, A_{m+1}, A_{m+2}, …, A_{n−1}⟩

such that A_{m} : T_{m}, A_{m+1} : T_{m+1}, …, A_{n−1} : T_{n−1}. If n = m, the type.has only one member (the empty string); and if n > m, string m n is empty.

Inductive string

m : IN n : IN

     string m n : Set

n : IN

                        ⟨⟩ : string n n

A : T_{m} Δ : string m + 1 n
A :: Δ : string m n

We can define destructors

head : Πm, n : IN.(m < n) → string m n → T_{m}
tail : Πm, n : IN.(m < n) → string m n → string m + 1 n

Using a standard technical trick in Coq CITE, we can prove that ⟨⟩ is the only object of type string n n, and every object Δ in string m n has the form head Δ :: tail Δ if m < n.

We define the operations Π and Λ that operate on strings and terms, and the operation of concatenation that appends a string to a context. The types for these operations are as follows:

– If Δ : string m n and A : T_{n}, then ΠΔ.A : T_{m}.

– If Δ : string m n and A : T_{n}, then ΛΔ.A : T_{m}.

– If Γ : C_{m} and Δ : string m n, then Γˆ Δ : C_{n}.

These operations are all defined by recursion on the string Δ as follows:

Π⟨⟩.B ≡ B  Λ⟨⟩.B ≡ B  Γˆ ⟨⟩ ≡ Γ
Π(A :: Δ).B ≡ ΠA(ΠΔ.B) Λ(A :: Δ).B ≡ λA(ΛΔ.B) Γˆ (A :: Δ) ≡ (Γ, A)ˆ Δ

Substitution in Strings. The definition of substitution on strings is very tricky. One natural suggestion would be to define an operation with type

Πm, n, p : IN.string m n → (F_{m} → T_{m+p}) → string (m + p) (n + p) .

However, as mentioned above, it proved necessary to find a definition that would not involve addition within any type.

After many such false starts, the following solution was arrived at. We define a relation on pairs of natural numbers, which we call matching:

⟨m, n⟩ ∼ ⟨p, q⟩

(read: “⟨m, n⟩ matches ⟨p, q⟩”). This relation is equivalent to m ≤ n ∧ n − m = q − p. If ⟨m, n⟩ ∼ ⟨p, q⟩, then it is possible to apply a substitution F_{m} → T_{p} to a string in string m n to obtain a string of type string p q.

(We actually place the type ⟨m, n⟩ ∼ ⟨p, q⟩ in Set, as we shall need to define substitution by recursion on the proof that ⟨m, n⟩ ∼ ⟨p, q⟩.)

Definition 3. Define the relation ⟨m, n⟩ ∼ ⟨p, q⟩ inductively as follows:

{m : IN p : IN \atop ⟨m, m⟩ ∼ ⟨p, p⟩}  {⟨m + 1, n⟩ ∼ ⟨p + 1, q⟩ \atop ⟨m, n⟩ ∼ ⟨p, q⟩}

We can now define the substitution operation on strings:

Definition 4. Suppose ⟨m, n⟩ ∼ ⟨p, q⟩. We define, for each Δ : string m n and ρ : F_{m} → T_{p}, the string Δ[ρ] : string p q, by recursion on the proof of ⟨m, n⟩ ∼ ⟨p, q⟩ as follows:

– The base case is ⟨m, m⟩ ∼ ⟨p, p⟩. For Δ : string m m and σ : F_{m} → T_{p},

Δ[σ] ≡ ⟨⟩ : string p p

– Suppose ⟨m, n⟩ ∼ ⟨p, q⟩ was deduced from ⟨m + 1, n⟩ ∼ ⟨p + 1, q⟩. For Δ : string m n and σ : F_{m} → T_{p},

Δ[σ] ≡ (head Δ)[σ] :: (tail Δ) [ \begin{matrix}⊥ & ↦ & ⊥ \\ ↑ x & ↦ & σ(x)\{↑\} \end{matrix} ] : string p q

Proof of Strengthening. Now that these operations are in place, it is a straightforward, albeit lengthy, task to formalise van Bentham Jutting’s proof of Strengthening.

The proof involves the partitioning of the terms of a PTS into two sets T_{V} and T_{S}. We represent these in the formalization by two functions

                     varlike : Πn : IN.T_{n} → bool
                    sortlike : Πn : IN.T_{n} → bool

varlike M being true if M ∈ T_{V} and false otherwise, and sortlike representing T_{S} in the same way.

The proof also involves a set of sorts Σ(Γ, M) for every context Γ and term M. We represent this in the formalization by a function

Σ : Πn : IN.C_{n} → T_{n} → S → Prop .

Neither definition presents any problems.

We can proceed to prove the results of van Bentham Jutting’s paper one by one. None of the results requires a significant change, and the proof of each follows the proof given in the paper closely.

We note in passing that the only results that require the use of the strings that we went to such trouble to define are these:

Lemma 5 (Typing Lemma).

If a ∈ T_{S} and Γ ⊢ a : A and Γ ⊢ a : B, then ∃s_{1}, s_{2}, C_{1}, …, C_{n}[A ↠ Πx_{1} : C_{1}. · · · .Πx_{n} : C_{n}.s_{1} ∧ B ↠ Πx_{1} : C_{1}. · · · .Πx_{n} : C_{n}.s_{2}] (n ≥ 0).

In our formalization, we found that the following weaker result was all that was required for the proof of Strengthening:

∀Γ, M, A.sortlike M → Γ ⊢ M : A → ∃Δ, s.A ↠ ΠΔ.s

Theorem 4. If a ∈ T_{S}, Γ ⊢ a : A and A ↠ Πx_{1} : A_{1}. · · · .Πx_{n} : A_{n}.s, then s ∈ Σ(Γ, A).

In our formalization:

∀Γ, a, A, Δ, s.sortlike a → Γ ⊢ a : A → A ↠ ΠΔ.s → Σ Γ a s .

the latter of which is only needed to prove Corollary 1. If A ∈ T_{S}, Γ ⊢ A : s, then s ∈ Σ(Γ, A).

In our formalization:

∀Γ, a, s.sortlike a → Γ ⊢ a : s → Σ Γ a s .

The proof of Strengthening in van Bentham Jutting’s paper is concluded by proving the following lemma:

Lemma. If Γ_{1}, x : A, Γ_{2} ⊢ b : B and x ∉ F V (Γ_{2}) ∪ F V (b), then ∃B′(B ↠ B′ ∧ Γ_{1}, Γ_{2} ⊢ b : B′).

Theorem. If Γ_{1}, x : A, Γ_{2} ⊢ b : B and x ∉ F V (Γ_{2}) ∪ F V (b), then Γ_{1}, Γ_{2} ⊢ b : B. We instead prove the following big-step versions:

Lemma 6. If Γ ⊢ b{ρ} : B, Δ is valid, ρ is injective, and Δ ⊆_{ρ} Γ, then there exists B′ such that B ↠ B′{ρ} and Δ ⊢ b : B′.

Theorem 5. If Γ ⊢ b{ρ} : B, Δ is valid, ρ is injective, and Δ ⊆_{ρ} Γ, then there exists B′ such that B ≡ B′{ρ} and Δ ⊢ b : B′.

Corollary 2. If Γ ⊢ b{ρ} : B{ρ}, Δ is valid, ρ is injective, and Δ ⊆_{ρ} Γ, then Δ ⊢ b : B.

5 Related Work

McKinna and Pollack [2] produced a large formalization of many results in the theory of PTSs, based on a representation of syntax that uses named variables. They use two separate types: V for the bound variables, and P for the free variables, or parameters.

From our point of view, this formalization has two principal disadvantages. Firstly, we are often dealing with operations renaming variables, or replacing a variable with a parameter or vice versa; we would prefer not to have to deal with these technicalities. Secondly, we have objects that do not correspond to any term in the syntax — namely, those in which objects of type V occur free. We need frequently to check that every object of type V is bound in the terms with which we are dealing — that they are closed, in McKinna and Pollack’s terminology.

If one has a reason to use named variables — if one wishes to stay as close as possible to an implementation, if one wishes to check proofs about α-conversion, or if one simply wishes, in McKinna and Pollack’s phrase, to “take symbols seriously” — then this is a very good formalization to look at. However, if one’s sole concern is to check a proof of a metatheoretic result, then a more abstract representation of syntax simplifies matters greatly.

Barras has produced a formalization in Coq, entitled “Coq in Coq” [3, 10], of the metatheory of the Calculus of Constructions, representing the terms with de Bruijn notation, using Coq’s natural numbers for the free and bound variables.

This formalization has the advantages that α-convertible terms are now provably equal, and that there are no objects that do not represent well-formed terms.

However, this formalization is still more complex than our own. It involves operations ↑_{k}^{n}, which raises every de Bruijn index after the kth by n places. We are frequently using lemmas about how these operations interact with each other, or with substitutions. Proofs often proceed by several case analyses involving comparisons of natural numbers, or arithmetical manipulation of the sub- and super-scripts of these operators.

These are the two major formal developments of metatheory of which the author is aware. Also worthy of mention is higher-order abstract syntax [11], which embeds the object theory one is studying within the type theory in which one is working, then takes advantage of the type theory’s binding and substitution operations. This did not seem suitable for our purposes; the author thought it important to maintain the separation between object theory and metatheory for this work.

Several other approaches to the representation of syntax have been developed relatively recently, including Gabbay and Pitts’ work [12], which develops variable binding as an operation in FM-set theory, and CINNI [13], a formal system which contains both named variable syntax and de Bruijn notation as subsystems. It would be very interesting to see a similar formal development of the metatheory of some system based on either of these.

6 Conclusion

We have formalised in Coq the proofs of many results in the metatheory of PTSs, using a slight variation of the nested data type representation of terms with binding. In the author’s opinion, the result is a very simple and elegant formalization. While some thought is often needed to find the correct form for definitions and theorems, the proofs are then short and direct, certainly in the early stages of the metatheory.

When we turn to the proof of Strengthening, this claim can no longer be made: the formalization does then become technically complex. It is difficult to compare this proof with other formalizations: McKinna and Pollack [2] use a different proof of Strengthening, and Barras [3] does not prove Strengthening at all. It is possible that the proof of Strengthening would be just as complex in other formalizations; or that some way of simplifying it in this formalization could be found.

The nested data type representation of syntax is the one the author prefers if one’s only interest in formalization is to obtain a guarantee of the correctness of a theorem. It is certainly worthy of being another tool which someone working in formal metatheory should be aware of, and consider using.

Lastly, we may speculate that there may be some theoretical interest in the form the metatheory takes when the nested data type representation of syntax is used. The substitution functions with which we have been dealing are precisely the arrows in the standard way of assigning categorical semantics to a type theory. Possibly the monadic structure of the syntax representation has some implications in this area? The correspondence between the subcontext relation and the satisfaction relation, and likewise between the Weakening Lemma and the Substitution Lemma, is striking. It suggests something along the lines of a fibred category, the base category using renaming operations as arrows, and the fibred category using substitution functios. It remains to be seen whether it is profitable to explore these ideas.

References

1. Adams, R.: Pure type systems with judgemental equality. (Submitted for publication in the Journal of Functional Programming)

2. McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reasoning 23 (1999) 373–409

3. Barras, B.: Auto-validation d’un sysème de preuves avec familles inductives. PhD thesis, Université Paris 7 (1999)

4. Aczel, P.: Nested data types in constructive type theory. (Talk given at Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy)

5. Barendregt, H.: Lambda calculi with types. In Abramsky, S., Gabbay, D.M., Maibaum, T.S.E., eds.: Handbook of Logic in Computer Science. Volume II. Oxford University Press (1992)

6. van Benthem Jutting, L.S.: Typing in pure type systems. Information and Computation 105 (1993) 30–41

7. Bellegarde, F., Hook, J.: Subsitution: A formal methods case study using monads and transformations. Sci. Comput. Program. 23 (1994) 287–311

8. Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: CSL ’99. Volume 1683 of LNCS., Springer-Verlag (1999) 453– 468

9. Bird, R.S., Paterson, R.: de Bruijn notation as a nested datatype. J. Functional Programming 9 (1999) 77–91

10. Barras, B.: A formalization of the calculus of constructions. (Web page)

http://coq.inria.fr/contribs/coq-in-coq.html.

11. Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI ’88: Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, New York, NY, USA, ACM Press (1988) 199–208

12. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13 (2002) 341–363

13. Stehr, M.O.: CINNI: A generic calculus of explicit substitutions and its application to lambda-, sigma- and pi-calculi. In: Third International Workshop on Rewriting Logic and its Applications (WRLA’2000), Kanazawa, Japan, September 18 – 20, 2000. Volume 36 of Electronic Notes in Theoretical Computer Science., Elsevier