Some Lambda Calculus and Type Theory Formalized^{∗}

James McKinna

             jhm@dcs.ed.ac.uk

Robert Pollack

                                   rap@dcs.ed.ac.uk

Laboratory for Foundations of Computer Science The King’s Buildings, University of Edinburgh, EH9 3JZ, Scotland

1 Introduction

“This paper is about our hobby.” That is the first sentence of [MP93], the first report on our formal development of lambda calculus and type theory, written in autumn 1992. We have continued to pursue this hobby on and off ever since, and have developed a substantial body of formal knowledge, including Church-Rosser and standardization theorems for beta reduction, and the basic theory of Pure Type Systems ( PTS ) leading to the strengthening theorem and type checking algorithms for PTS . Some of this work is reported in [MP93, vBJMP94, Pol94b, Pol95]. In the present paper we survey this work, including some new proofs, and point out what we feel has been learned about the general issues of formalizing mathematics. On the technical side, we describe an abstract, and simplified, proof of standardization for beta reduction, not previously published, that does not mention redex positions or residuals. On the general issues, we emphasize the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts.

The LEGO Proof Development System [LP92] was used to check the work in an implementation of the Extended Calculus of Constructions (ECC) with inductive types [Luo94]. LEGO is a refinement style proof checker, publicly available by ftp and WWW, with a User’s Manual [LP92] and a large collection of examples. Section 1.3 contains information on accessing the formal development described in this paper. Other interesting examples formalized in LEGO include program specification and data refinement [Luo91], strong normalization of System F [Alt93], synthetic domain theory [Reu95, Reu96], and operational semantics for imperative programs [Sch97].

∗Submitted to Journal of Automated Reasoning

1.1 Why?

PTS have a beautiful meta-theory, developed informally in [Bar92, Ber90, GN91, vBJ93, Geu93]. These papers are unusually clear and mathematical, and there is little doubt about the correctness of their results, so why write a machine-checked development? The informal presentations leave many decisions unspecified and many facts unproved. They are far from the detail of representation needed to write a computer program for typechecking PTS , and the lemmas needed to prove correctness of such a program. At the start, our long-term goal was to fill these gaps in order to increase confidence in proofchecking programs (such as LEGO) based on type theory. That goal is largely met in [Pol95]. Also, while the basic informal theory of PTS is well understood, the difficulties of formalization suggested reformulations which clarify the presentation.

Another goal of the project is to develop a realistic example of formal mathematics. In mathematics and computer science we do not prove one big theorem and then throw away all the work leading up to that theorem; we want to build a body of formal knowledge that can continually be extended. This suggests some design criteria for formalization. Representations and definitions must be suitable for the whole development, not specialized for a single theorem. The theory should be structured, like computer programs, by abstraction, providing “isolation of components” so that several parts of the theory can be worked on simultaneously, perhaps by several workers, and so that the inevitable wrong decisions in underlying representations can later be fixed without affecting too seriously a large theory that depends on them. The body of knowledge we want to formalize is itself still growing, e.g. [vBJMP94] reports advances on typechecking for PTS done later than our original formalization, that became part of our formal development. The work on typechecking benefited from the basic formalization of PTS , since proofs about several related systems could be easily adapted from proofs already done for PTS . Further, new subjects were included; e.g. the standardization theorem, not used in the type theory, was formalized by the first author. On the other hand, we do not claim that type theory is a realistic example for all formal mathematics: it is especially suitable for formalization because the objects are inductively constructed, their properties are proved by induction over structure, and there is little equality reasoning.

Perhaps the most compelling reason for our continuing fascination with this work is the lure of completely concrete, yet simple, proofs of results whose conventional presentation seems to require some notions that are “messy” to formalize, e.g. the standardization theorem discussed in section 3.4. We see such proofs as beautiful, both by their simplicity and their concreteness. There is a tendency in formalization to throw simplicity to the winds in frustration to get the proof to work at all; but once it is checked, it can be beautified relatively easily, as improved definitions and arguments are mechanically checked, easily pointing out new glitches and suggesting how to fix them. Also, a formal development is easy to come back to a year later, as all the details you would not otherwise have written down are explicit, and don’t have to be rediscovered.

1.2 Related Work

There are many formalizations of the Church–Rosser theorem [Sha85, Hue94, Nip96, Pfe92]; the only formalization of a standardization theorem we know of is [Coq96a], for lazy combinator expressions. Formalizations of type theory include [DB93, Bar95]; both of these address limited aspects of very special type theories (essentially the Calculus of Constructions), although [Bar95] is very interesting work in which the program extraction mechanism of Coq is used to extract an executable typechecker from a proof of decidability of typechecking. In contrast to all the cited work except [Bar95], our development hasn’t been terminated by reaching one specified theorem, but continues to grow in various directions guided by our interests, and by other work we come across that we feel needs checking. For example, both authors have checked parts of type theory papers we were asked to referee.

A novelty in our presentation is the use of named variables. Most of the formalizations of type theory or lambda calculus that we know of use de Bruijn indices (“nameless variables”) [Sha85, Alt93, Hue94, Nip96, Bar95] or higher order abstract syntax [Pfe92] to avoid formalizing the renaming of variables to prevent unintended capture during substitution. While de Bruijn notation is concrete and suitable for formalization, there are reasons to formalize the theory with named variables. For one thing, implementations must use names at some level, whether internally or only for parsing and printing; in either case this use of names must be formally explained. More interesting is the insight to be gained into the meaning of binding. Many researchers agree that de Bruijn representation “really is” what we informally mean by lambda terms, in the sense that there is no need to quotient terms by alpha-conversion, i.e. intensional equality on de Bruijn terms corresponds with what is informally meant by identity of terms. Nonetheless, de Bruijn representation is a coding of the informal notion of binding, and doesn’t address at all the relationship between free and bound variables, namely how free variables become bound. In our formalization, syntactic terms using named variables are themselves concrete: the names of bound variables actually occur (parametrically) in meta-formulas containing them, just as the names of free variables do. This is done using a formulation suggested by Coquand [Coq91], based on syntactically distinguishing free from bound variables^{1}. Other work on formalization of binding and substitution using names includes [Coq96b, GM96, Owe95, Sat83, Sto88], but these do not work out any large examples using their binding notions. It would be interesting to compare our development with some similar example using the terms up-to alpha conversion of [GM96]. A presentation of type theory based on treating terms with named variables concretely is Martin-Löf’s calculus of explicit substitutions [Tas93], but this presentation is not closed under alpha-conversion, as our presentation is (section 5.5.3), and we view this as a failure of concreteness of Martin-Löf’s system.

1.3 This paper and the formal development

The source files for the development described in this paper, along with a README file explaining how to check them, is available on the

LEGO WWW homepage http://www.dcs.ed.ac.uk/home/lego/.

LEGO uses a module system (described in [JP93]) based on Cardelli’s mock modules [Car91]. Each source file is a module, and each module has a header saying which modules it depends on. Thus the directory of modules associated with this paper contains parallel, and even incompatible, developments. If you type Load strengthening, the file strengthening.l (which contains the proof of strengthening for PTS ) will be loaded, preceeded by every module it depends on^{2}.

There are over 70 proof source files with extension .l^{3} containing over 1500 definitions and lemmas. This is a large amount of formal knowledge, which we can only survey here. This paper uses informal mathematical notation, but almost every definition and lemma that we mention is given with its formal name in typewriter font (often in parentheses). You can then use grep to find the file in which it is defined and the files in which it is used. This is not particularly elegant, but it’s how we do it too. Keeping track of a large amount of formal knowledge is a serious problem that we have not addressed very well.

1This distinction is already present in Gentzen [Gen69, pages 71–2, 116–7, 141, 216–7] and Prawitz [Pra65]

2The dependencies are determined from the module headers, not by examining the actual dependencies in the files.

3The .l files are the ones we wrote; LEGO generates “compiled” files with a .o

1.3.1 About notation

As mentioned, this paper uses informal notation, which is arrived at by manually translating from the formal LEGO notation into L^{A}TEX. Further, the translation is not purely syntactical; we chose to surpress some technical details to have a readable presentation. Errors are quite likely, arising from both our translation and your interpretation. This paper may be an informative outline of the formal work, but if you want to believe one of our results you must read its formal statement, and all the formal definitions used in its statement; see [Pol96] for discussion of believing a large formal development.

In [MP93] we used formal notation, verbatim text manually extracted from LEGO source files; no translation errors occur, but there is no reason to believe the verbatim text in the paper actually appears in the files. Indeed, the the document and the files drifted apart over time. In [Pol94b] we again used formal notation, mechanically extracting marked sections of the source files, following the idea of Knuth’s WEB. We could rerun the extraction to update the document to the formal source, but many readers complained the document was as unreadable as the formal source. Presenting a formal development is a serious problem. Perhaps mechanical extraction with mechanical translation to informal notation is the right direction to pursue.

For better or worse, we have sanitised this presentation so that very little purely formal detail shows through. For example, we mostly surpress the distinction between boolean values and propositional values. However, we don’t want to hide the fact that formalization requires many details that don’t appear in informal presentations.

A few basic notations The development uses LEGO’s built-in library of impredicative definitions for the usual logical connectives and their properties; we use standard notation for these connectives. Quantifiers are typed in ECC, but we reserve symbols to range over certain types, and drop the type labels almost everywhere; e.g. p will be reserved to range over parameters, PP , so we write ∀p … instead of ∀p:PP . . ..

extension. These are the fully annotated λ -terms generated by the LEGO tactics called in the .l file.

Well known computer science notations are used, e.g. if ( , , ) as if-then-else, list( ) for the type of lists over , @ (or sometimes just concatenation) for list append. All funtions of ECC are total (as opposed to functions in the object theory of lambda terms and PTS ), so some operations take extra arguments for a “failure value”, e.g. (assoc a b l) returns b if a is not the first element of a pair occurring in l.

2 Pure Languages

In this section we discuss a formalization of the language of PTS , including terms, occurrences and substitution. We derive a strong induction principle for well-formed terms.

A Pure Language ( PL ) is a triple (PP, VV, SS) where

• PP is an infinite set of parameters, ranged over by p, q, r; these are the global, or free, variables.

• VV is an infinite set of variables, ranged over by v, x, y; these are the local, or bound, variables.

• SS is a set of sorts, ranged over by s, t u; these are the constants.

PP , VV and SS have decidable equality. That PP and VV are infinite is captured by the assumption that for every list of parameters (variables) there exists a parameter (variable) not occurring in the list; e.g.^{4}:

∀l∈ list(PP) . ∃p . ¬ member(p, l)  (PPinf)

We are not assuming mathematical principles, but working parametrically in types PP , VV and SS having the stated properties. These can be instantiated with particular types that provably do have these properties, e.g. the natural numbers, or lists over some finite enumeration type. By working parametrically we are preserving abstractness: only the stated properties are used in our proofs.

4In this formula, member(p, l) is decidable because PP has decidable equality.

2.1 Terms

The terms of a PL , Trm , ranged over by M, N, A, …, E, a, b, are given by the grammar

M ::= v | p | s  atoms: variable, parameter, sort
| [v:M]M | {v:M}M binders: lambda, pi
| M M  application

To be precise, Trm is inductively generated by six constructors: every term can be thought of as a well-founded tree whose leaves are variables, parameters and sorts, and whose interior nodes are lambda and pi (having three branches each) and application (having two branches). We often define functions on Trm by structural (primitive) recursion over this inductive definition. As usual, we intend [v:A]B and {v:A}B to bind v in B but not in A. However the intended binding structure is not determined by the definition of Trm , but is made explicit by the definitions of substitution and occurrence below. Equality on terms is defined by recursion over Trm ; it inherits decidability from PP , VV and

SS .

Remark 2.1 (Notation) Often when doing case analysis by term structure, we want to say that the binders, lambda and pi, behave the same way. We introduce a notation ⟨v:A⟩a to allow combining these cases. The actual formalization does not have such a notation, but this would have saved much cutting and pasting in developing the proofs.

The length of a term is used as a measure for well-founded induction.

    lngth(α)  ≜ 1  α ∈ PP, VV, SS

lngth(⟨v:A⟩a) ≜ 1 + lngth(A) + lngth(a)

    lngth(a b)  ≜ 1 + lngth(a) + lngth(b)

Two properties of this measure are used applications: if A is a proper subterm of B then lngth(A) < lngth(B) (used in induction on the length of terms), and every term has positive length (used in reasoning about PTS by induction on the sum of the lengths of the terms in a context).

2.2 Occurrences of Parameters and Sorts

The list of parameters occurring in a term is computed by primitive recursion over term structure, and the boolean judgement whether or not a given parameter occurs in a given term is decided by the member function on this list of parameters.

params(p)  ≜ [p]

     params(α)  ≜ []  α ∈ VV, SS
     params(⟨v:A⟩a) ≜ params(A) @ params(a)
     params(a b)  ≜ params(a) @ params(b)
     p ∈ A  ≜ member(p, params(A))

Similarly sorts(A) and s ∈ A are defined.

2.3 Substitution

For the machinery on terms, we need two kinds of substitution, for parameters and for variables, both defined by primitive recursion over term structure. Write [a/p]M (formally psub) for substitution of a for a parameter, p, in M. This is entirely textual, not preventing capture. Since parameters have no binding instances in terms, there is no hiding of a parameter name by a binder.

[a/p]q  ≜ if(p=q, a, q)
[a/p]α ≜ α α ∈ VV, SS
[a/p]⟨v:B⟩b ≜ ⟨v:[a/p]B⟩[a/p]b
[a/p](M N) ≜ [a/p]M [a/p]N

Substitution of a for a variable, v, in M, written [a/v]M (formally vsub), does respect hiding of bound instances from substitution, but does not prevent capture.

[a/v]x  ≜ if(v=x, a, x)
[a/v]α ≜ α α ∈ PP, SS
[a/v]⟨x:B⟩b ≜ ⟨x:[a/v]B⟩if(v=x, b, [a/v]b)
[a/v](M N) ≜ [a/v]M [a/v]N

[ /p] and [ /v] will be used only in safe ways in the type theory and the theory of reduction and conversion, so as to prevent unintended capture of variables. Note that these operations are total functions, and do not rename variables. Also, occurrences of a in [a/ ] are shared, regardless of whether they occur within different binding scopes, in contrast to the situation with de Bruijn indices.

Some important lemmas can now be proved:

p ∉ M ⇒ [N/p] [p/v]M = [N/v]M , (vsub is psub alpha)

Vcl-atom Vclosed(α)  α ∈ PP ∪ SS

Vcl-bind

            Vclosed(A)  Vclosed( [p/v]B)

Vclosed( ⟨v:A⟩B)

Vcl-app

            Vclosed(A)  Vclosed(B)
                  Vclosed( A B)

Table 1: Inductive definition of the relation Vclosed .

and we have a ready supply of terms of the shape [p/v]M , with p ∉ M :

∀p, M.∃v, M′. M = [p/v]M′ ∧ p ∉ M′  (shape lemma)

Many other properties of these operations are proved in the formal development.

2.4 No Free Occurrences of Variables

Intuitively parameters are the free names in terms; variables are intended to be the bound names, and we do not consider terms with free variables to be well formed. We define inductively a predicate Vclosed (variable-closed) over terms (table 1). This is analagous to the way a typing relation specifies another kind of well-formedness. (It will turn out that every PTS -typable term is Vclosed ). Thus Vclosed is used as an induction principle over well formed terms. As this relation is a simple case of ideas that recur many times in what follows, we will discuss it at some length.

Of course all terms of form s and p are Vclosed (rule Vcl-atom), and no terms of shape v are Vclosed (there is no rule to introduce Vclosed(v) ), but how do we define Vclosed for binders? The approach to “going under binders” is a central idea of our formal handling of names: for ⟨v:A⟩a to be Vclosed , we require Vclosed(A) and Vclosed( [p/v]a) for some parameter p. That is, to go under a binder, first fill the hole with parameter, p. But p doesn’t appear in the conclusion of rule Vcl-bind; which parameter are we to use? In the definition of Vclosed we say that any parameter will do, but there is another possible choice: that Vclosed( [p/v]B) be derivable for all p. This is not a formal question; it is one of the tasks of a reader of formal mathematics to decide if the formalisation correctly captures her informal understanding. But a formaliser can help readers by pointing out alternatives, and formally proving some relationship between them. This is especially interesting when alternative definitions lead to easier proofs in some cases. We will see this below for Vclosed .

Remark 2.2 Vclosed is equivalent to having no free variables

(Vclosed vclosed, vclosed Vclosed). This observation may be of

informal interest (“the definition of Vclosed is reasonable”), but we do not use it formally because Vclosed allows us to avoid all talk of free variables.

Vclosed Generation Lemmas Suppose you have a proof of Vclosed( ⟨v:A⟩B) ; without examining it you know it must be constructed by Vcl-bind from proofs of Vclosed(A) and Vclosed( [p/v]B) , because no other rule for Vclosed has a conclusion of shape Vclosed( ⟨v:A⟩B) . The very fact that a relation is inductively defined means that its judgements can only be derived by using its rules. This is often called case analysis, and more generally, the lemmas that express such properties are called generation lemmas [Bar92], or inversion principles [DFH^{+} 93]. Note that inversion principles are determined by the shape of a definition, not by its extension. LEGO has new and very useful tactics to automate the use of inversion [McB96], but most of what we describe in this paper was done before the tactics were available. We will frequently use inversion on inductive definitions in the rest of this paper without further comment.

The generation lemmas from the definition of Vclosed are

     Vclosed(v) ⇒ absurd

Vclosed(⟨v:A⟩B) ⇒ Vclosed(A) ∧ ∃p . Vclosed([p/v]B)

     Vclosed(A B) ⇒ Vclosed(A) ∧ Vclosed(B)

Notice how the existential quantifier in the case for binders expresses the failure of the subformula property in Vclosed .

2.4.1 A better induction principle for Vclosed .

Here are three “obvious” facts about Vclosed (alpha Vclosed lem,

Vclosed alpha).

Vclosed(⟨v:A⟩B) ⇒ Vclosed(A) ∧ ∀p . Vclosed([p/v]B)
∀M.Vclosed(M) ⇒ ∀q, v.[q/v]M = M
∀B, p, v.Vclosed([p/v]B) ⇒ ∀q.Vclosed([q/v]B)

They are all directly provable, but appear to need length induction (which appeals to well-founded induction and then subsidiary case analysis; e.g. the proof of claim aVclosed alpha below), for the usual reason that statements about change of names are proved by length induction rather than structural induction: e.g. [q/v]M is not generally a subterm of ( M N) , but it is shorter than ( M N) . We will derive a new induction principle which packages up such arguments once and for all.

Consider an alternative definition, called aVclosed , differing only in the rule for binders, in which the right premise requires aVclosed( [p/v]B) for every p:

aVcl-bind

            aVclosed(A)  ∀p . aVclosed( [p/v]B)

                     aVclosed( ⟨v:A⟩B)

We will show that Vclosed and aVclosed derive the same judgements. Induction over aVclosed is the principle which Melham and Gordon rediscovered as a consequence of their Axiom 4 (Unique Iteration) [GM96, Section 3.2].

It is worth saying that Vclosed is a type of finitely branching well-founded trees; i.e. Vcl-atom are the leaves, and Vcl-bind and Vcl-app are binary branching nodes. On the other hand, aVclosed contains infinitely branching well-founded trees, where aVcl-bind creates a branch for each parameter p. Notice also that for any term, A, there is at most one derivation of aVclosed(A) , while there may be many derivations of Vclosed(A) , differing in the parameters used in the left premises of instances of aVcl-bind.

Equivalence of Vclosed and aVclosed (aVclosed Vclosed,
Vclosed aVclosed)
             ∀A . aVclosed(A) ⇔ Vclosed(A) .

Both directions follow easily by structural inductions once we have the following claim (aVclosed alpha):

∀B, p, v . aVclosed( [p/v]B) ⇒ ∀q . aVclosed( [q/v]B)

Proof. The claim is proved by induction on lngth(B) . This works because every term appearing in a premise of a rule of aVclosed is shorter than the term appearing in its conclusion; the typing relations to be considered later do not have this property, and more subtle proofs will be required (section 5.2.1).

By well-founded induction on lngth(B) , we have the goal

∀A . (∀X . lngth(X) < lngth(A) ⇒

∀p, v . aVclosed([p/v]X) ⇒ ∀q . aVclosed([q/v]X)) ⇒

∀p, v . aVclosed([p/v]A) ⇒ ∀q . aVclosed([q/v]A)

Now using term structural induction on A, we have cases for sort, variable, parameter, binder and application (only case analysis is necessary here; we don’t use the structural induction hypotheses). Consider the case for binder: we must show aVclosed( [q/v] ⟨n:A⟩B ) , i.e.

aVclosed( ⟨n: [q/v]A ⟩if (v=n, B, [q/v]B) )

under the assumptions

ih : ∀X . lngth(X) < lngth(⟨n:A⟩B) ⇒

∀p, v . aVclosed([p/v]X) ⇒ ∀q . aVclosed([q/v]X)

vclp : aVclosed([p/v]⟨n:A⟩B)
(i.e. aVclosed(⟨n:[p/v]A⟩if(v=n, B, [p/v]B)))

By aVclosed inversion applied to assumption vclp we also know

h1 : aVclosed([p/v]A)
h2 : ∀r . aVclosed([r/n]if(v=n, B, ([p/v]B)))

By aVcl-bind, it suffices to show

aVclosed( [q/v]A) and ∀r . aVclosed( [r/n]if (v=n, B, [q/v]B) )

Noticing that [p/v] doesn’t change lngth, the first of these holds by ih and h1. For the second, let r be an arbitrary parameter, and consider cases. If v = n then we are done by h2; i.e. [q/v]B doesn’t actually appear in the goal, and [p/v]B doesn’t actually appear in h2. Finally the interesting case: if v ≠ n we use a straightfoward lemma

(alpha commutes alpha)

∀v, w . v ≠ w ⇒ ∀r, q, A . [r/v] [q/w]A = [q/w] [r/v]A

to rewrite the goal to aVclosed( [q/v] [r/n]B ) . By ih it suffices to show aVclosed( [p/v] [r/n]B ) , which follows by h2 after again rewriting the order of substituting p and r.

What have we gained? By defining aVclosed and showing it to be extensionally equivalent to Vclosed , we can view the induction principle of aVclosed as an induction principle for the extension of Vclosed , and this is clearly stronger than the induction principle of Vclosed . We insist on extension to point out that aVclosed-induction may be used to prove statements about the judgement Vclosed , but not about derivations of the judgement.

Notice that we could directly prove the analogue of claim aVclosed alpha for Vclosed (the proof outlined above works), but it is not just the stronger premises of aVclosed we are after (i.e. the generation lemmas), it is the stronger induction hypotheses.

2.5 A Technical Digression: Renamings

[ /p] and [ /v] are sequential operations; we have not used a notion of simultaneous substitution, except in the following special case. A renaming is a finite function from parameters to parameters. Renamings are represented formally by their graphs as lists of ordered pairs.

rp  ≜ PP × PP  (renaming pair)

           Renaming ≜ list(rp)

ρ and σ range over renamings. The action of a renaming (renTrm) on parameters is by lookup in the representing list, and is extended compositionally to all terms.

ρp  ≜ (assoc p p ρ)
ρα ≜ α (α ∈ VV, SS)
ρ⟨v:A⟩a ≜ ⟨v:ρA⟩ρa
ρ(M N) ≜ ρ(M) ρ(N)

This is a “tricky” representation. First, if there is no pair (p, q) in ρ, (assoc p p ρ) returns p, so the action of a renaming is always total, with finite support. Also, while there is no assumption that renamings are the graphs of functional relations, the action of a renaming is functional, because assoc finds the first matching pair. Conversely, consing a new pair to the front of a renaming will “shadow” any old pair with the same first component. We do not formalize these observations.

Renamings commute with substitution in a natural way:

∀ρ, M, N, v. ρ( [N/v]M) = [ρN/v]ρM . (vsub renTrm commutes)

Renaming is iterated substitution. We can analyse the action of a renaming in terms of substitution (renTrm is conjugated psub):

∀r, M, ρ, p, q . r ∉ M ∧ r ∉ ρ ⇒ ((p, q)::ρ)M = [q/r](ρ( [r/p]M))

From this lemma it is easy to show that renaming respects any relation that substitution of parameters respects (psub resp renTrm resp):

      ∀R : Trm→Trm→Prop .

(∀A, B . R(A, B) ⇒ ∀q, p . R([q/p]A, [q/p]B)) ⇒

∀A, B . R(A, B) ⇒ ∀ρ . R(ρA, ρB)

Similar results hold for n -ary relations R.

Injective and Surjective Renamings It is useful to have bijective renamings (e.g. in Section 5.2.1). The definitions are standard:

inj(ρ) ≜ ∀p, q . ρp = ρq ⇒ p = q , sur(ρ) ≜ ∀p ∃q . ρq = p

It is surprisingly difficult to construct bijective renamings in general because of the trickiness of the representation mentioned above. However it’s clear that any renaming that only swaps parameters is bijective (swap sur, swap inj), and this is enough for our purposes:

swap(p, q) ≜ [(p, q), (q, p)]
∀p, q . sur(swap(p, q)) ∧ inj(swap(p, q))

3 Reduction and Conversion

In this section we outline the theory of reduction and conversion of Pure Languages. The main results are the Church-Rosser and standardization theorems.

As in the definition of Vclosed (Section 2.4), the interesting point in defining reduction is how the relation goes under binders. To understand how reduction works, consider informally one-step beta-reduction of untyped lambda calculus. In our style the β and ξ rules are:

β  (λx.M) N → [N/x]M  Vclosed(N)
ξ  \begin{matrix}[q/x]M → [q/y]N \\ λx.M → λy.N \end{matrix}  q ∉ M, q ∉ N

The substitution [N/x]M on the RHS of β does not prevent capture, so some restriction is required. It is obvious that no capture can occur if N is closed in the usual informal sense, but because we distinguish between parameters and variables it is enough that N be Vclosed . This is no actual restriction: we will only want to reason about Vclosed terms anyway, as these are the “well-formed” terms.

To use β under a binder, as allowed by ξ, we must preserve the invariant that β is only applied to Vclosed terms: we fill the “holes” left by stripping off the binder with a fresh parameter. Here is an instance of ξ where incorrect capture might occur (contracting the underlined redex):

\begin{matrix}[q/x]\underline{(λv.λx.v) x} = \underline{(λv.λx.v) q} → λx.q = [q/y]λx.y \\ λx.(\underline{(λv.λx.v) x}) → λy.λx.y \end{matrix}

After removing the outer binder λx, replacing its bound instances by a fresh parameter, q, and contracting the Vclosed redex thus obtained, we must re-bind the hole now occupied by q. (Since q was fresh, all instances of q mark holes that should be re-bound). According to ξ, we require a variable, y, and a term, N, such that [q/y]N is the contractum of the Vclosed redex, λx.q in the example. Such a pair is y, λx.y (the one we have used above), as is z, λx.z for any z ≠ x. However ξ does not derive the incorrect judgement

λx.(\underline{(λv.λx.v) x}) → λx.λx.x

because

[q/x]λx.x = λx.x ≠ λx.q.

Thus incorrect capture is avoided.

3.1 Parallel Reduction

Rather than use ordinary β -reduction, we take parallel reduction (à la Tait–Martin-Löf) as the basic reduction relation. Parallel reduction is convenient for the Church-Rosser and standardization theorems, as emphasised by Takahashi in her beautiful account [Tak95]. Our development follows that of [Tak95], with some refinements.

3.1.1 One-step parallel reduction

This relation, → (par red1), is defined in Table 2. As in Vclosed above, the dependence of the congruence rule for binders on the choice of a parameter p is only apparent. However, something new arises here, namely the side conditions p ∉ B , p ∉ B′ . These are eigenvariable

pr1-atom α → α  α ∈ PP ∪ SS

pr1-beta \begin{matrix}A → A′ & [p/u]B → [p/v]B′ \\ ( [u:U]B) A & → & [A′/v]B′ \end{matrix}  \begin{matrix}p ∉ B, p ∉ B′ \\ Vclosed(U) \end{matrix}

pr1-bind \begin{matrix}A → A′ & [p/u]B → [p/v]B′ \\ ⟨u:A⟩B & → & ⟨v:A′⟩B′ \end{matrix}  p ∉ B , p ∉ B′

pr1-app \begin{matrix}A → A′ & & B → B′ \\ A B & → & A′ B′ \end{matrix}

Table 2: 1-Step Parallel Reduction

conditions^{5}, which ensure that the parameter p correctly indicates the position of the bound variables in the compound terms.

Only Vclosed terms participate in → (par red1 Vclosed)

∀A, B. A → B ⇒ Vclosed(A) ∧ Vclosed(B) ,

and → is reflexive on Vclosed terms (par red1 refl)

∀A . Vclosed(A) ⇒ A → A .

A stronger induction principle for → The rules pr1-atom, pr1bind and pr1-app are the congruence rules for our language. As with Vclosed (section 2.4.1), we introduce a strong congruence rule for binders

p̃r1 -bind \begin{matrix}A ˜→A′  ∀p. [p/u]B ˜→ [p/v]B′ \\ ⟨u:A⟩B & ˜→ & ⟨v:A′⟩B′ \end{matrix}

and prove that → and ˜→ are extensionally equivalent, giveing us stronger induction and inversion principles. Because of the eigenvariable conditions in pr1-bind, a technique using renamings is required to show the equivalence. We omit the details, but a similar argument is used in section 5.2.1.

5Kleene [Kle52, §78, on the notion of “pure variable” proof] explains how to treat such conditions; however, to do so he must explicitly consider operations on derivations, hence dependent elimination, whereas our methods require only rule induction, i.e. non-dependent elimination. The second author is grateful to N.

Shankar for this reference.

The strong induction principle is used to show that → is closed under substitution (par red1 psub):

\begin{matrix}M→M′ & & N→N′ \\ [N/p]M & → & [N′/p]M′ \end{matrix}

Many-step parallel reduction → → (par redn), is the transitive closure of →. It inherits properties par redn Vclosed and par redn refl from the corresponding properties of → mentioned above.

3.1.2 Alpha-Conversion

We define α -conversion, ∼^{α}, to be the least congruence, i.e. ∼^{α} is exactly → without the rule pr1-beta, so ∼^{α} ⊆ →. This definition is symmetric, by inspection. To show that it is transitive requires the stronger induction principle for ∼^{α}, which we prove in the same way as above. Hence ∼^{α} is an equivalence relation^{6}. It is decidable for Vclosed

terms (decide alpha conv):
   ∀A, B. Vclosed(A) ⇒ Vclosed(B) ⇒ decidable( A ∼^{α} B)

with a straightfoward but messy proof, by double induction on

aVclosed(A) and aVclosed(B) .

Informally, alpha-conversion is used for changing the names of variables. We do not have ⟨x:A⟩B ∼^{α} ⟨y:A⟩( [y/x]B) because [y/x]B does not prevent capture. However, we do have (true alpha conv pi):

∀v, A, B . Vclosed( ⟨v:A⟩B) ⇒ ∀x∃C . ⟨v:A⟩B ∼^{α} ⟨x:A⟩C

Closure under α -conversion One of Coquand’s original motivations for distinguishing between variables and parameters was to avoid the need to reason about α -conversion; many of the arguments below (Church-Rosser, standardisation, subject reduction) achieve this goal.

Name-carrying syntax is regarded as an abbreviation for a quotient modulo α -conversion, so that when we formalise a relation R such as parallel reduction above, we really intend R modulo the quotient structure, i.e. ∼^{α}∘ R∘∼^{α} . We say a relation R is: closed under α if α∘R ⊆ R∘α ; strongly closed, if α∘R ⊆ R ; full wrt α if R∘α ⊆ α∘R ; strongly full, if R∘α ⊆ R .

6This should be contrasted with Gallier’s meticulous but long-winded treatment in [Gal90].

Remark 3.1 → is strongly closed under α -conversion: the proof is the same as that for transitivity of ∼^{α}, with the additional case of a redex handled by observing that an α -variant of a redex is a redex. However → is not full w.r.t. ∼^{α} -classes. For example

( [x:q] x x ) ( [w:q]w) → ( [y:q]y) ( [y:q]y)  for every y,

but no α -variant of the LHS → -reduces to ( [y_{1}:q]y_{1} ) ( [y_{2}:q]y_{2} ) where y_{1} ≠ y_{2} , although this is an α -variant of the RHS.

3.1.3 A Church-Rosser Theorem

Using the argument of Tait and Martin-Löf, as modernized in [Tak95], we prove the first CR theorem (par redn DP):

∀M, M′, M′′. M → → M′ ∧ M → → M′′ ⇒ ∃N. M′ → → N ∧ M′′ → → N

by the usual strip lemma argument and the diamond property of →

(comp dev par red1 DP).

To do so, we introduce an inductive characterisation of complete development, ⟶, (comp dev)^{7}. It is given by the same rules as →, except for the application rule:

cd-app  \begin{matrix}A ⟶ A′ & & B ⟶ B′ \\ A B & ⟶ & A′ B′ \end{matrix}  A is not a lambda

The side condition in cd-app forces contraction of all redexes: we have a deterministic sub-relation of →.

The theorem on finiteness of developments now becomes the combination of:

• induction on the definition of ⟶, which we may think of as a partial correctness assertion;

• the existence (for Vclosed terms) of complete developments, (comp dev exists), which we may think of as a termination argument.

7cf. the definition of ⟶ as a function by structural recursion on terms [Tak95]

This separation of concerns gives us an advantage over Takahashi’s informal proofs, in that we do not have to consider, in each proof about ⟶, a subsidiary induction (case-analysis) to resolve the redex/nonredex distinction in the case of an application. This is handled once and for all in the existence proof, while induction on the definition of ⟶ already delineates the redex/non-redex distinction. The price we pay is that we no longer work with an object-level function, but rather a functional relation.

Of course, we have simplified matters by considering developments of the entire set of redexes in a term: this is sufficient for our purposes, but a more refined analysis (e.g. [Hue94]) would take us beyond our simple datastructure of terms.

The diamond property (comp dev par red1 DP) follows easily from the following “Takahashi” lemma (comp dev preCR):

∀M, N, M′. M→N , M⟶M′ ⇒ N→M′

whose proof is by induction on M⟶M′, with inversion of M→N. As usual, the interesting case, of a redex/redex, appeals to par red1 psub.

Remark 3.2 These proofs do not make any appeal to α -conversion. This is because both the → and ⟶ relations are strongly closed under α -conversion. Indeed, we may show the following two properties, which

strengthen comp dev exists, namely comp dev unique:

M⟶M′ , M⟶M′′ ⇒ M′∼^{α}M′′ ;

and comp dev exists unique:

M∼^{α}M′ ⇒ ∃M′′. M⟶M′ , M⟶M′′

3.2 Conversion

We define conversion, ≃ (conv), as the symmetric and transitive closure of → →. It inherits properties conv Vclosed and conv refl from those of → → mentioned above.

The second Church-Rosser theorem is now straightfoward to prove for conversion (convCR):

∀M, M′. M ≃ M′ ⇒ ∃N. M→ →N ∧ M′→ →N

3.3 Normal Forms

A term is beta normal (beta norm), if it has no beta redexes . This may be defined with the same rules as aVclosed , except the rule for application, which is

bn-app

           beta norm (A)  beta norm (B)

                  beta norm ( A B)

A is not a lambda

All beta norm terms are Vclosed (beta norm Vclosed). A relation

of reduction to normal form is defined:

        A ↓ N ≜ beta norm (N) ∧ A → → N  (normal form)

→ → is reflexive, so there is reduction from a normal form, but every reduct of a normal form is a normal form (par_redn_bnorm_is_bnorm)

∀A, B . A → → B ⇒ beta norm (A) ⇒ beta norm (B)

Any reduct of a normal form alpha-converts with that normal form

(par_redn_bnorm_is_alpha_conv)

∀A, B . A → → B ⇒ beta norm (A) ⇒ A ∼^{α} B .

Hence, by Church-Rosser, normal forms of a term are unique up to alpha-conversion (nf_unique). Since ∼^{α} ⊆ →, the converse also holds

(nf_alpha_class)

∀A, M, N. A ↓ M ⇒ ( A ↓ N ⇔ M ∼^{α} N ) .

Thus the class of normal forms of a ( Vclosed ) term is either empty or exactly an alpha-conversion equivalence class.

Deciding conversion Conversion is decidable for normalizing terms. The proof of this depends on Church-Rosser; since normal forms are unique only up to alpha-conversion, it also depends on decidability of alpha-conversion (Section 3.1.2).

3.4 The Standardization Theorem

Our work on type-checking requires us to go beyond theorems such as Church-Rosser in the analysis of reduction. In particular, to talk of syntax-directed systems, we must consider deterministic reduction relations, of which weak-head reduction is the simplest. A typical

wh1-app \begin{matrix}A →_{wh} A′ \\ A B & →_{wh} & A′ B \end{matrix}

wh1-beta ( [v:V]B) A →_{wh} [A/v]B

Table 3: One step of weak-head reduction

property required of such a relation is the following counterpart to the quasi-normalisation theorem (wh standardisation lemma):

A → → B, whnf(B) ⇒ ∃C.A ↠_{wh} C, whnf(C), C → → B

Takahashi showed how to approach such theorems with an analysis of parallel reduction into head reduction followed by internal reduction, a so-called semi-standardization lemma [Mit79]. We adapted her methods to the case of weak-head reduction, and the corresponding modified notion of internal reduction. In doing so we simplify them somewhat, in particular by removing the need for the complex invariant M ⋆ N. Moreover, the arguments we employed can be replicated in the context of head reduction and internal reduction in their classical senses.

Recently, we rounded off this line of development by proving a standardization theorem for pure languages. The main novelty here is the removal of any mention of residuals (so the reader may be unconvinced that we have formalised the standardization theorem). The other thing to observe is that all the desirable consequences of standardization, which we required to analyse type-checking, such as the lemma above, are already corollaries to the semi-standardization lemma.

There are three main ingredients to the theorem: weak-head reduction, internal parallel reduction, and standard reduction itself.

3.4.1 Weak-head reduction

One step of weak-head reduction (wh red1) is shown in Table 3. By inversion, we see that there are no weak-head reducts of a lambda, so we may assume without loss of generality that A is not a lambda in the rule wh1-app. We have not built any Vclosed assumptions into the definition, as this will always be used in a context in which all terms

are Vclosed .

The reader may validate such a definition by considering the weakhead normal forms (Table 4), and various lemmas relating →_{wh} and

wh-atom whnf(α)  α ∈ PP ∪ SS
wh-bind whnf( ⟨v:A⟩B)
wh-app  whnf(A) ; whnf( A B)  A is not a lambda

Table 4: Weak-head normal forms

ip1-atom α→_{i}α  α ∈ PP ∪ SS

ip1-bind \begin{matrix}A→A′ & [p/u]B → [p/v]B′ \\ ⟨u:A⟩B & →_{i} & ⟨v:A′⟩B′ \end{matrix}  p ∉ B , p ∉ B′

ip1-app  \begin{matrix}A→_{i}A′ & & B→B′ \\ A B & →_{i} & A′ B′ \end{matrix}

Table 5: One step of internal parallel reduction

whnf (wh red1 determin, wh nf is nf1, alpha conv resp wh nf).

Many-step weak-head reduction, ↠_{wh}, (wh redn) is defined as the reflexive transitive closure of →_{wh}. It is closed under renamings, substitution (psub resp wh redn), and application on the right

(wh redn app):

\begin{matrix}∀M, M′.M ↠_{wh} M′ ⇒ [N/p]M ↠_{wh} [N/p]M′ \\ ∀M, M′.M ↠_{wh} M′ ⇒ M N ↠_{wh} M′ N \end{matrix}

3.4.2 Internal parallel reduction

The classical notion of head reduction leads to a notion of “internal” redex, as any non-head redex. We adapt such a notion to weak-head reduction, which gives us the definition of internal parallel reduction, →_{i}, (ipar red1) as shown in Table 5. We allow arbitrary parallel reduction in each compound term, except in the rator position of applications, where we restrict to internal reduction.

It is immediate by structural induction that internal parallel reductions are parallel reductions. We also have the important abstract property (ipar red1 refl wh nf) that →_{i} preserves and reflects weakhead normal forms, and a fortiori, the shape (outermost constructor) of a term. This reflection of weak-head normal forms, together with the lemma below, is the key to the proof of the quasi-normalisation result with which we opened this discussion.

Semi-standardization (par red1 wh redn ipar red1)

∀M, M′. M→M′ ⇒ ∃M_{w}. M ↠_{wh} M_{w}→_{i}M′

Proof. The proof proceeds by induction on M→M′. The only tricky case is that of the parallel β step. By inductive hypothesis, we obtain (introducing Skolem constants A_{w}, B_{w})

\begin{aligned}ihA & : & A ↠_{wh} A_{w}→_{i}A′ \\ ihB & : & [p/u]B ↠_{wh} [p/w]B_{w}→_{i}[p/v]B′ \end{aligned}

and we are required to show that there exists some M_{w} such that

( [u:U]B) A ↠_{wh} M_{w}→_{i} [A′/v]B′

Since

( [u:U]B) A →_{wh} [A/u]B = [A/p] [p/u]B ↠_{wh} [A/p] [p/w]B_{w}

by psub resp wh redn and psub is vsub alpha, we may conclude the

result by stitching weak-head reduction sequences together, provided we can establish the following claim, which is the easy base case of Lemma 2.4 in [Tak95] (wh ipar red1 psub):

\begin{matrix}M→_{i}M′ & N ↠_{wh} N_{w}→_{i}N′ N→N′ \\ ∃P . [N/p]M ↠_{wh} P →_{i} [N′/p]M′ \end{matrix}

This is proved in the same way as we showed closure of parallel reduction under substitution, by induction on M→_{i}M′. A detail to observe here is that we must explicitly assume that the reduction from N to N′ is parallel. Takahashi builds this into her ⋆ invariant, whereas in the use of wh ipar red1 psub, we obtain this assumption for free as the premise associated with reduction in A.

We show the case of an application M = A B , where A→_{i}A′ and B→B′. By induction hypothesis, there exists some P_{A} such that [N/p]A ↠_{wh} P_{A}→_{i} [N′/p]A′ . The proof of the claim, and hence of the whole lemma, is completed by taking P =_{def} P_{A} ( [N/p]B) , and appealing once more to psub resp wh redn, ipar red1 app and

par red1 psub.

To establish the full semi-standardization result for → →, we must also show the commutation result (ipar wh redn commutes):

M→_{i} M_{w} ↠_{wh} M′ ⇒ ∃M′_{w}. M ↠_{wh} M′_{w}→_{i}M′

This is a corollary (by induction on M_{w} ↠_{wh} M′) of the following

lemma (ipar wh red1 commutes):

∀M, M_{w}, M′. M→_{i} M_{w} →_{wh} M′ ⇒ ∃M′_{w}. M ↠_{wh} M′_{w}→_{i}M′

Proof. Induction on M→_{i}M_{w}, and inversion of the ancillary hypothesis M_{w} →_{wh} M′. All cases are trivial, except that of application M = A B , where M_{w} = A′ B′ , A→_{i}A′ and B→B′. We show the case of a wh-redex, where we have: M_{w} = ( [v:V]A′′) B′ and M′ = [B′/v]A′′ . We use the fact that ipar red1 reflects the weak-head normal form A′ = [v:V]A′′ to infer that A = [u:U]A′′′ . Moreover, since A→_{i}A′, we obtain by inversion that U→V and ∀p. [p/u]A′′′ → [p/v]A′′ . Choosing p ∉ A′′ , p ∉ A′′′ , and applying pr1-sub, we obtain [B/u]A′′′ → [B′/v]A′′ . Now we appeal to Lemma 3.4.2, finally to conclude that for some P , we have

M = ( [u:U]A′′′) B →_{wh} [B/u]A′′′ ↠_{wh} P →_{i} [B′/v]A′′ = M′

as required.

Throughout we used induction on the definitions of the various reduction relations to establish these lemmas. This is by contrast with Takahashi’s treatment, where induction is on the term structure (with inversion of the relational hypotheses). This leads to slightly weaker arguments, and consequently to the need for stronger inductive invariants. Such refinements to these arguments would be inconceivable without machine support.

3.4.3 Standard Reduction

The property of being a standard reduction, ⟶_{s}, is usually stated (e.g. by Mitschke [Mit79]) in terms of a highly intensional geometric definition on λ -terms. To formalise this definition directly, we would have to enrich the datatype of terms in order to be able to speak of

std-atom α⟶_{s}α  α ∈ PP ∪ SS

std-bind \begin{matrix}A⟶_{s}A′ & [p/u]B ⟶_{s} [p/v]B′ \\ ⟨u:A⟩B & ⟶_{s} & ⟨v:A′⟩B′ \end{matrix}  p ∉ B , p ∉ B′

std-app \begin{matrix}A⟶_{s}A′ & B⟶_{s}B′ \\ A B & ⟶_{s} & A′ B′ \end{matrix}

std-wh  \begin{matrix}A ↠_{wh} B & B⟶_{s}C \\ A⟶_{s}C \end{matrix}

Table 6: Standard reduction, standard (adapted from Plotkin)

redex positions in a term. Such an approach has been taken in [Hue94]; we have chosen instead a presentation (table 6), adapted from Plotkin’s notion of standard sequence [Plo75]. The essence of this presentation is to define standard reduction as the least congruence closed under prefixing by weak-head reductions. We leave implicit the sequence of redexes contracted, as this may be computed by recursion, and its “left-to-right” character, and thus avoid mention of residuals or redex positions.

Remark 3.3 We have defined standard reductions of arbitrary length once and for all, and without any considerations of reduction to normal form; note furthermore, however, that we may easily achieve this end by adding the side condition A′ ≠ λ to the std-app rule, and whnf(B) to the std-wh rule. Also, this definition is both strongly closed under α -conversion, and strongly full.

Our final aim is the following standardization theorem

(the standardisation lemma):

∀A, B. A → → B ⇒ A⟶_{s}B

Induction on A → → B suffices if we can show that our notion of standard reduction absorbs single steps of parallel reduction:

A→ B⟶_{s}C ⇒ A⟶_{s}C .

By our Lemma 3.4.2, and std-wh, it suffices to prove the following lemma, that standard reduction absorbs single steps of internal parallel

reduction (standard absorbs ipar red1):

A→_{i} B⟶_{s}C ⇒ A⟶_{s}C .

Proof. The proof is by induction on B⟶_{s}C. This avoids reconsidering the tricky application case of the commutation lemma above, and we may exploit the fact that →_{i} preserves and reflects the shape of terms. The price we pay is the need for strong induction on B⟶_{s}C, as the ancillary hypothesis A→_{i}B is then an expansion step. In each non-atomic case, we make a subsidiary appeal to semi-standardization, in order to be able to exploit the induction hypotheses. This gives a rather mechanical and “abstract nonsense” flavour to the argument, emphasising once more that the real complexity lies in the the proof of Lemma 3.4.2.

We focus on the case of a binder, where we have as hypotheses:

premA : A⟶_{s}A′
premB : B⟶_{s}B′
ihA  : ∀C.C→_{i}A ⇒ C⟶_{s}A′
ihB  : ∀p.∀C.C→_{i}[p/u]B ⇒ C⟶_{s}[p/v]B′
H  : C→_{i}⟨u:A⟩B

By inversion of H, we conclude that C = ⟨w:A_{c}⟩B_{c} , where A_{c}→A and ∀p. [p/w]B_{c} → [p/u]B . But now by semi-standardization, A_{c} ↠_{wh} A_{w}→_{i}A and [p/w]B_{c} ↠_{wh} B_{w}→_{i} [p/u]B . So by induction hypothesis ihA, we have A_{w}⟶_{s}A′, and using std-wh to fold back the weak-head reductions A_{c} ↠_{wh} A_{w}, we finally obtain A_{c}⟶_{s}A′. In exactly the same way, modulo the choice of a parameter p ∉ B_{c}, B, B′ , we obtain [p/w]B_{c} ⟶_{s} [p/v]B′ . But now C⟶_{s} ⟨v:A′⟩B′ by construction.

This concludes the proof that standard reduction absorbs internal reduction, and hence parallel reduction, and so finally we may conclude that every (parallel) β -reduction sequence may be standardized.

4 Pure Type Systems

PTS is a class of type theories given by a set of derivation rules (table 7) parameterized by a PL , (PP, VV, SS) , and by two relations

• axioms, ax ⊆ SS × SS , written informally as ax(s_{1}:s_{2})

Ax  • ⊢ s_{1} : s_{2}  ax(s_{1}:s_{2})

Start \begin{matrix}Γ ⊢ A : s \\ Γ[p:A] ⊢ p : A \end{matrix}  p ∉ Γ

Weak \begin{matrix}Γ ⊢ α : C & Γ ⊢ A : s \\ Γ[p:A] ⊢ α : C \end{matrix}  α ∈ PP ∪ SS , p ∉ Γ

Pi  \begin{matrix}Γ ⊢ A : s_{1} & Γ[p:A] ⊢ [p/x]B : s_{2} \\ Γ ⊢ \{x:A\}B : s_{3} \end{matrix}  \begin{matrix}p ∉ B \\ rl(s_{1}, s_{2}, s_{3}) \end{matrix}

Lda \begin{matrix}Γ[p:A] ⊢ [p/x]M : [p/y]B & Γ ⊢ \{y:A\}B : s \\ Γ ⊢ [x:A]M : \{y:A\}B \end{matrix}  \begin{matrix}p ∉ M \\ p ∉ B \end{matrix}

App \begin{matrix}Γ ⊢ M : \{x:A\}B & Γ ⊢ N : A \\ Γ ⊢ M N : [N/x]B \end{matrix}

tConv \begin{matrix}Γ ⊢ M : A & Γ ⊢ B : s \\ Γ ⊢ M : B \end{matrix}  A ≤ B

Table 7: The Typing Rules of PTS (formal name gts)

• rules, rl ⊆ SS × SS × SS , written informally as rl(s_{1}, s_{2}, s_{3}) .

We usually intend ax and rl to be decidable, but this assumption is not used in the basic theory of PTS . When we are interested in algorithms for typechecking ([Pol94b, Pol95]), even stronger assumptions about decidability are needed.

The typing judgement has the shape Γ ⊢ M : A, meaning that in context Γ , term M has type A. (The formal name of this relation is gts, from the old name “Generalized Type Systems”.) We call M (or (Γ, M) ) the subject and A the predicate of judgement. Contexts, ranged over by Γ , Δ , bind parameters to types:

Γ ::= • | Γ[p:A] (null, cons).

Contexts are formalized as lists over PP × Trm . If Γ participates in some derivable judgement, Γ ⊢ M : A, we say Valid(Γ) .

4.1 A Generalization: Abstract Conversion

We have further generalized PTS by parameterizing the rules of table 7 on another relation, ≤ (called abstract conversion), occurring in the side condition of rule tConv. In conventional presentations of PTS [Bar92], the actual relation of beta-conversion ( ≃) is used for ≤.

There are several reasons to be interested in parameterizing PTS on its conversion relation. For one thing, the type theory ECC, implemented in LEGO, is not actually a PTS because it uses a generalized notion of conversion called cumulativity. ECC is of special interest to us, so we formalize an extension of PTS which includes ECC. Our formal development includes a typechecking algorithm for ECC [Pol94b]. Even for PTS , there is a notorious open problem, the Expansion Postponement problem [vBJMP94, Pol94b], which asks if the conversion relation in table 7 can be replaced by beta-reduction without changing the typability of any terms. We know of one other work on PTS using an abstract conversion relation: [BM].

The only properties of ≤ necessary to prove the substitution lemma (section 5.4) are reflexivity, transitivity, and invariance under substitution:

     cnv refl  ∀A . Vclosed(A) ⇒ A ≤ A

cnv trans  ∀A, D, B . A ≤ D ⇒ D ≤ B ⇒ A ≤ B
psub resp cnv  \begin{matrix}∀N, A, B, p . Vclosed(N) ⇒ \\ A ≤ B ⇒ [N/p]A ≤ [N/p]B \end{matrix}

To prove the subject reduction theorem (section 5.5), we finally need that conversion is related to contraction of redexes, and has an “internal” Church-Rosser property:

   cnv conv ≃ ⊆ ≤

cnvCR pi  \begin{matrix}∀u, v, A, a, B, b . \\ \{u:A\}B ≤ \{v:a\}b ⇒ a ≤ A ∧ ∀q . [q/u]B ≤ [q/v]b \end{matrix}

Notice the contravariance in the last property. It is easy to prove that ≃ has these properties, so we can formally instantiate ≤ by ≃ (or by the cumulativity of ECC) and discharge all these assumptions; we are working abstractly, not making assumptions.

≃ is an equivalence relation, but ≤ is a partial order (which is why we use an asymmetric symbol for ≤). Other significant properties of ≃ that do not generally hold for ≤ include:

s_{1} ≃ s_{2} ⇒ s_{1} = s_{2} ,  A ≃ s ⇒ A → → s ,  A → → s ⇒ s ∈ A .

Some differences between abstract-conversion- PTS and β -conversion-PTS are detailed in [Pol94b]. This kind of analysis, of which properties are actually used in some body of work, is greatly aided by formalization.

4.2 Are the rules a formalization of PTS ?

Leaving aside abstract conversion, the rules of table 7 differ from the standard informal presentation [Bar92] in several ways. First, the handling of parameters and variables in the Pi and Lda rules, is similar to that in the rules of table 2. Other differences are restriction of weakening to atomic subjects, and the Lda rule.

Binding and substitution The treatment of operating under binders in table 7 is analogous to that in the reduction relations considered above. (See discussion of the rule Lda below.) As the substitution used in rule App may cause capture of variables, we must show that

N is Vclosed . In fact we have (gts Vclosed lem)

∀Γ, M, A . Γ ⊢ M : A ⇒ Vclosed(M) ∧ Vclosed(A)

by structural induction. It also follows easily that a Valid context is Vclosed in an obvious sense.

Atomic Weakening The standard presentation of weakening in PTS allows any term as subject

(weakening)  \begin{matrix}Γ ⊢ M : C & Γ ⊢ A : s \\ Γ[p:A] ⊢ M : C \end{matrix}  p ∉ Γ

where we restrict to atomic terms, α (see rule Weak). Our rules derive the same judgements (weakening is seen to be admissible in section 5.3), but allow fewer derivations (those derivations where weakening is pushed to the leaves). This gives a cleaner meta theory, as induction over derivations treats fewer cases. For example, given a judgement, Γ ⊢ M N : B, with an application as its subject, there is no confusion whether it is derived by App or Weak. Thus, with atomic weakening, any judgement may only be derived by tConv or by exactly one of the remaining rules.

The Lambda Rule For the rule for typing a lambda in informal presentations [Bar92, Geu93] is

λ  \begin{matrix}Γ[x:A] ⊢ M : B & Γ ⊢ \{x:A\}B : s \\ Γ ⊢ [x:A]M : \{x:A\}B \end{matrix}

The conventional understanding is that the bound variable, x, doesn’t really occur in the conclusion of rule λ, as the notations “ [x:A]M ” and “ {x:A}B ” refer to alpha-equivalence classes^{8}. Thus, in concrete notation, the subject and predicate of the lambda rule may bind different variables, which we formalize in our rule Lda. One might, instead, formalize rule λ as

Lda’ \begin{matrix}Γ[p:A] ⊢ [p/x]M : [p/x]B & Γ ⊢ \{x:A\}B : s \\ Γ ⊢ [x:A]M : \{x:A\}B \end{matrix}  \begin{matrix}p ∉ M \\ p ∉ B \end{matrix}

This was our first attempt, and surprisingly, this system derives the same judgements as the system of table 7 (lemmas rlts gts and gts rlts). However, using Lda’, the subject reduction theorem is difficult to prove, and derivations are distorted by the need to use the conversion rule for alpha-conversion. See [Pol94b] for more details.

5 PTS With Abstract Conversion

We survey the development leading to the subject reduction theorem. The main difference between this section and the presentation in [Bar92] is our use of the atomic weakening rules (section 4.2), and our simpler proof of subject reduction (section 5.5).

5.1 Some basic facts

Here is a sample of the many small facts that had to be established, usually by simple structural induction. Parameter lemmas All parameter occurrences in a judgement are bound in the context, and the binding instances in a Valid context are distinct parameters:

\begin{matrix}(Γ ⊢ M : A ∧ p ∉ Γ) ⇒ p ∉ M ∧ p ∉ A \\ Γ[p:B] ⊢ M : A ⇒ p ∉ Γ \end{matrix} (free params lem1)

                                              (CxtCorrect0)

8However, in the left premise of rule λ, all free instances of the actual symbol “ x ” in M and B are intended to refer to the context entry [x:A] . Thus the conventional reading of this rule doesn’t make sense as concrete notation.

Start Lemmas Every axiom is derivable in every valid context, and the global bindings of a valid context are all derivable:

(Γ ⊢ M : A ∧ ax(s_{1}:s_{2})) ⇒ Γ ⊢ s_{1} : s_{2}
Γ[p:B]Δ ⊢ M : A ⇒ Γ[p:B]Δ ⊢ p : B

                                                (sStartLem) (vStartLem)

5.2 A Better induction principle for PTS

As for previous relations, we define an alternative typing relation, ⊢_{a} (apts), that identifies all those derivations of each ⊢ judgement that are inessentially different because of parameters occurring in the derivation but not in its conclusion. ⊢_{a} differs from ⊢ only in the right premise of the Pi rule and the left premise of the Lda rule.

aPi  \begin{matrix}Γ ⊢_{a} A : s_{1}  ∀ p ∉ Γ . Γ[p:A] ⊢_{a} [p/x]B : s_{2} \\ Γ ⊢_{a} \{x:A\}B : s_{3} \end{matrix} rl(s_{1}, s_{2}, s_{3})

aLda \begin{matrix}∀ p ∉ Γ . Γ[p:A] ⊢_{a} [p/x]M : [p/y]B  Γ ⊢_{a} \{y:A\}B : s \\ Γ ⊢_{a} [x:A]M : \{y:A\}B \end{matrix}

In these premises we avoid choosing a particular parameter by requiring the premise to hold for all parameters for which there is no reason it should not hold, that is, for all “sufficiently fresh” parameters. As before, we will show that ⊢ and ⊢_{a} derive the same judgements.

It is interesting to compare the side conditions of Pi with those of aPi. In Pi we need the side condition p ∉ B so that no unintended occurrences of p (i.e. those not arising from occurrences of the variable x) are bound in the right premise; we do not need p ∉ Γ because the validity of Γ[p:A] is obvious from the right premise. In aPi, we cannot require the right premise for all p, but only for those such that Γ[p:A] remains valid, i.e. those p not occurring in Γ . However the condition p ∉ B is not required because of “genericity”, that is, the right premise of aPi must hold for the infinitely many parameters not occurring in Γ , while only finitely many of these instances can occur in B.

5.2.1 ⊢_{a} is equivalent to ⊢

As with previous relations, this equivalence will give us a stronger induction principle, and stronger generation (inversion) lemmas for ⊢.

∀Γ, M, A . Γ ⊢_{a} M : A ⇔ Γ ⊢ M : A  (apts gts, gts apts)

Proof. Direction ⇒ is straightfoward by structural induction on Γ ⊢_{a} M : A.

To prove direction ⇐, first prove a lemma that bijective renamings

respect ⊢_{a} (bij ren resp apts)

∀ρ, Γ, M, A . Bij(ρ) ⇒ Γ ⊢_{a} M : A ⇒ ρΓ ⊢_{a} ρM : ρA

by ⊢_{a} -structural induction^{9}.

Now we proceed to prove Γ ⊢ M : A ⇒ Γ ⊢_{a} M : A by structural induction on a derivation of Γ ⊢ M : A. All cases are trivial except for the rules Pi and Lda. Consider the case for Pi: we must prove Γ ⊢_{a} {n:A}B : s_{3} under the assumptions

sc  : rl(s_{1}, s_{2}, s_{3})
noccB : p ∉ B
l prem : Γ ⊢ A : s_{1}
r prem : Γ[p:A] ⊢ [p/n]B : s_{2}
l ih  : Γ ⊢_{a} A : s_{1}
r ih  : Γ[p:A] ⊢_{a} [p/n]B : s_{2}

By rule aPi (using l ih) it suffices to show Γ[r:A] ⊢_{a} [r/n]B : s_{2} for arbitrary parameter r ∉ Γ . Thus, using the free parameter lemmas of section 5.1, we know

noccG : r ∉ Γ
norA : r ∉ A from l prem and noccG
nopG : p ∉ Γ from r prem
nopA : p ∉ A from r prem

Taking ρ = swap(r, p) , we have ρ(Γ[p:A]) ⊢_{a} ρ( [p/n]B) : ρs_{2} is derivable using bij_ren_resp_apts to rename r ih. (Recall from section 2.5 that swap(p, q) is always bijective.) Thus we are finished if we can show

ρ(Γ[p:A]) = Γ[r:A]  ∧  ρ( [p/n]B) = [r/n]B .

It is clear that the first equation holds from nopG, noccG, norA and nopA. For the second equation, notice that if r = p then we are done trivially, so assume r ≠ p, and hence r ∉ [p/n]B (from r prem and noccG). Now, using vsub renTrm commutes (section 2.5) we have

ρ([p/n]B) = {p ↦ r}([p/n]B)  (r ∉ [p/n]B)
= [{p ↦ r}p/n]({p ↦ r}B)) (vsub renTrm commutes)
= [r/n]B  (noccB)

9Actually injectivity of a renaming is enough for it to preserve ⊢_{a} , but we cannot prove this until after we know ⊢_{a} = ⊢ .

as required.

5.3 The Thinning Lemma and Weakening

The Thinning Lemma is important to our formulation because it shows that full weakening (weakening) is admissible in our system, justifying our use of atomic weakening in the definition of ⊢ (section 4.2).

The subcontext relation is defined

Γ ⊑ Δ ≜ ∀b : PP × Trm . b ∈ Γ ⇒ b ∈ Δ

We also say Δ extends Γ . This is the definition used informally in [Bar92, GN91, vBJ93]; a much more complicated definition is required to express this property in a representation using de Bruijn indices for global variables. Now we can state (thinning lemma):

∀Γ, Δ, M, A . Γ ⊢ M : A ⇒ ( Γ ⊑ Δ ∧ Valid(Δ) ) ⇒ Δ ⊢ M : A

A naive attempt to prove the thinning lemma by structural induction on Γ ⊢ M : A encounters serious difficulties with parameter side conditions (see [MP93, Pol94b] for discussion), but a proof is straightfoward using ⊢_{a} -induction, justified by the previous section. The full weakening rule is a corollary of thinning lemma.

5.4 Cut and type correctness

The substitution lemma

\begin{matrix}Γ ⊢ N : A & Γ[p:A]Δ ⊢ M : B \\ Γ( [N/p]Δ ) ⊢ [N/p]M : [N/p]B \end{matrix} (substitution lemma)

is proved by induction on the derivation of Γ[p : A]Δ ⊢ M : B. From this we get the commonly used case (cut rule) by instantiating Δ to the empty context.

Among the correctness criteria for type systems is that every type is itself well formed. In PTS we have the theorem (type correctness):

∀Γ, M, A . Γ ⊢ M : A ⇒ ∃s . A = s ∨ Γ ⊢ A : s

The proof is by structural induction; the only non-trivial case is rule App, which uses the substitution lemma and vsub_is_psub_alpha (section 2.3).

5.5 Subject Reduction Theorem: Closure Under Reduction

An important property of type systems is that a term does not lose types under reduction, thus types are a classification of terms preserved by computation. In fact we will show entire ⊢ -judgements are closed under reduction. We now need all five properties of abstract conversion (section 4.1).

5.5.1 Non-Overlapping Reduction

Our goal is to prove

Γ ⊢ M : A ⇒ M → → M′ ⇒ Γ ⊢ M′ : A  (gtsSR)

usually called the subject reduction theorem. Our naive strategy is to show that one step of reduction preserves typing, by induction on Γ ⊢ M : A. The critical case is rule App, when the application is actually a redex that is contracted. In order to simplify that case, we want to avoid overlapping redexes, as allowed in the β -rule of →. We want some reduction relation with no overlapping, whose transitive closure is equal to → →.

Another difficulty is that in rules Pi and Lda, a subterm of the subject of the conclusion (the type-label) appears in the context part of a premise; thus in these cases of an induction argument, a reduction in the subject of the conclusion may result in a reduction in the context of a premise. This suggests that the induction hypothesis should be strengthened to simultaneously treat reduction in the context and the subject, leading to the goal

\begin{matrix}G ⊢ M : A ⇒ \\ (M → M′ ⇒ G ⊢ M′ : A) ∧ (G → G′ ⇒ G′ ⊢ M : A) \end{matrix}

where → is ordinary one-step β -reduction. This approach is used in [GN91, Bar92], and produces a large number of case distinctions, based on which subterm of the subject contains the one redex which is contracted; all of these subcases are inessential except to isolate the one non-trivial case where the redex contracted is the application constructed by rule App. This simultaneous treatment of one reduction in either the context or the subject suggested to us that the proof would be smoother using a reduction relation that is congruent simultaneously in all branches, while forbidding overlapping of redexes. One step nonoverlapping reduction, →^{no} (no red1), is defined by the same rules as → (table 2) except for the β -rule, which is modified to prevent overlapping redexes:

nor1-beta ( [u:U]B) A →^{no} [A/u]B  Vclosed( ( [u:U]B) A)

Clearly →^{no} ⊆ →, so from the assumed property cnv conv (section 4.1), we have

A →^{no} B ⇒ A ≤ B ∧ B ≤ A .

We extend →^{no} compositionally to contexts (red1Cxt), and to pairs of a context and a term (red1Subj), writing Γ →^{no} Δ and ⟨Γ, M⟩ →^{no} ⟨Δ, N⟩ . We also define → →^{no} (no redn), the transitive closure of →^{no} , and show → →^{no}= → → (no par redn, par no redn).

5.5.2 The Main Lemma (subject reduction lem)

Γ ⊢ M : A ⇒ ⟨Γ, M⟩ → →^{no} ⟨Γ′, M⟩′ ⇒ Γ′ ⊢ M′ : A

Proof. By structural induction on Γ ⊢ M : A. We show the interesting case, from rule App. Given

l prem : Γ ⊢ M : {x:A}B
r prem : Γ ⊢ L : A
l ih  : ∀Γ′, M′ . (⟨Γ, M⟩ →^{no} ⟨Γ′, M′⟩) ⇒ Γ′ ⊢ M′ : {x:A}B
r ih  : ∀Γ′, L′ . (⟨Γ, L⟩ →^{no} ⟨Γ′, L′⟩) ⇒ Γ′ ⊢ L′ : A
red subj : ⟨Γ, M L⟩ →^{no} ⟨Δ, R⟩

we must show Δ ⊢ R : [L/x]B . By induction hypotheses

gtsDM : Δ ⊢ M : {x:A}B
gtsDL : Δ ⊢ L : A

By type correctness of gtsDM, for some s

gtsDpi : Δ ⊢ {x:A}B : s

By the pi-generation lemma, for some s_{2} and p ∉ B

gtsDB : Δ[p:A] ⊢ [p/x]B : s_{2}

By the cut rule on gtsDL and gtsDB (we also use vsub_is_psub_alpha (section 2.3) here, and several more times in this case)

gtsDBsub : Δ ⊢ [L/x]B : s_{2}.

Now there are two subcases R = M′ L′ where M →^{no} M′ and L →^{no} L′. The goal is Δ ⊢ M′ L′ : [L/x]B ; by rule App and the induction hypotheses we easily have Δ ⊢ M′ L′ : [L′/x]B . Use rule tCnv and gts-DBsub to expand L′ in the predicate back to L as required (this uses

cnv_conv).

R = [L/v]b where M = [v:A′]b . The goal is Δ ⊢ [L/v]b : [L/x]B . By l ih Δ ⊢ [v:A′]b : {x:A}B and by the lambda-generation lemma, for some w, B′ and s′

gtsDpi’ : Δ ⊢ {w:A′}B′ : s′
gtsDb : ∀p ∉ Δ . Δ[p:A′] ⊢ [p/v]b : [p/w]B′
c’  : {w:A′}B′ ≤ {x:A}B

By (cnvCR_pi c') (this is the only time it is used in this proof)

cnvA : A ≤ A′
cnvB : ∀q . [q/w]B′ ≤ [q/x]B

By a generation lemma on gtsDpi’

gtsDA’ : Δ ⊢ A′ : s1′

By (tCnv cnvA gtsDL gtsDA')

gtsDL’ : Δ ⊢ L : A′

By tCnv, cnvB and gtsDBsub, it suffices to show Δ ⊢ [L/v]b : [L/x]B′ which follows by cut on gtsDL’ and gtsDb.

5.5.3 Closure Under Reduction

It is now easy to show the subject reduction theorem, gtsSR, and a useful corollary, predicate reduction

Γ ⊢ M : A ⇒ A → → A′ ⇒ Γ ⊢ M : A′ .  (gtsPR)

Finally, extending → → compositionally to contexts^{10}, ⊢ is closed under beta-reduction (gtsAllRed)

Γ ⊢ M : A ⇒ ( Γ → → Γ′ ∧ M → → M′ ∧ A → → A′ ) ⇒ Γ′ ⊢ M′ : A′ .

10This relation is equivalent to transitively closing the compositional extension of of →^{no} to contexts.

There is a trivial but useful lemma (predicate conv):

( Γ ⊢ M : A ∧ A ≃ s ) ⇒ Γ ⊢ M : s .

Unlike rule tCnv, we don’t ask for evidence that s has a type, but the side condition uses ≃, not ≤. To prove such a lemma with ≤ requires technical restrictions; e.g. ECC with its type hierarchy chopped off a finite level fails to have such a property because of the sort at the top of the hierarchy.

Closure Under Alpha-Conversion From gtsAllRed and the fact that ∼^{α} ⊆ →, it follows that ⊢ judgements are preserved by ∼^{α} (gts alpha closed). Hence an implementation may typecheck a judgement as stated by a user, rather than searching for an alphaequivalent judgement which is derivable. See [Pol94b, Pol94a].

5.6 Another Presentations of PTS

In several rules of ⊢ the context Γ occurs more then once in the list of premises; in order to build a complete derivation, Γ must be constructed (by Start and Weak) in each branch in which it appears. It is much more efficient to assume that we start with a valid context, and only check that when rules extend the context (i.e. the right premise of Pi and the left premise of Lda) they maintain validity. This is more in keeping with implementations which are actually used, where we work in a “current context” of mathematical assumptions. We present such a system in table 8, and show it is equivalent to ⊢. The idea is originally due to Martin-Löf [Mar71], and is used in [Hue89].

This system has two judgements, a type judgment of shape Γ ⊢_{lv} M : A (lvtyp), and a validity judgement of shape Γ ⊢_{lv} (lvcxt). Note that they are not mutually inductive: validity depends on typing, but not conversely.

We have proved that ⊢_{lv} characterizes ⊢ (iff gts lvcxt lvtyp):

∀Γ, M, A . Γ ⊢ M : A ⇔ ( Γ ⊢_{lv} M : A ∧ Γ ⊢_{lv} )

Direction ⇐ of the proof is subtle. Formally, it uses an auxiliary mutual inductive definition, and a well-founded induction requiring dependent elimination; this is the only place in the entire development that either mutual induction or dependent elimination are used. More abstractly, direction ⇐ claims termination of a function that replaces all the proof annotations omitted by ⊢_{lv} . As this is a fast-growing function, its termination is a strong result. The proof is described in [Pol94b].

lvSrt Γ ⊢_{lv} s_{1} : s_{2}  ax(s_{1}:s_{2})
lvPar Γ ⊢_{lv} p : A  [p:A] ∈ Γ

lvPi

Γ ⊢_{lv} A : s_{1}  Γ[p:A] ⊢_{lv} [p/x]B : s_{2}
Γ ⊢_{lv} {x:A}B : s_{3}

\begin{matrix}rl(s_{1}, s_{2}, s_{3}) \\ p ∉ B, p ∉ Γ \end{matrix}

lvLda

Γ[p:A] ⊢_{lv} [p/x]M : [p/y]B  Γ ⊢_{lv} {y:A}B : s
Γ ⊢_{lv} [x:A]M : {y:A}B

\begin{matrix}p ∉ M \\ p ∉ B, p ∉ Γ \end{matrix}

lvApp

Γ ⊢_{lv} M : {x:A}B  Γ ⊢_{lv} N : A
Γ ⊢_{lv} M N : [N/x]B

lvConv

Γ ⊢_{lv} M : A  Γ ⊢_{lv} B : s
Γ ⊢_{lv} M : B

A ≤ B

lvNil • ⊢_{lv}

lvCons \begin{matrix}Γ ⊢_{lv} \\ Γ[p:A] ⊢_{lv} \end{matrix}  p ∉ Γ , Γ ⊢_{lv} A : s

Table 8: The system of locally valid contexts (lvtyp, lvcxt)

6 PTS with β -conversion

It is remarkable how little about ≤ has been needed for the theory described so far (section 4.1). In [Pol94b] we pursue the theory of PTS with abstract conversion to a correct typechecking algorithm for cumulative PTS , including Luo’s system ECC. Here, we point out a more standard theory of PTS with β -conversion, i.e. we instantiate ≤ in the preceeding with the actual relation ≃. (In LEGO the command Cut executes the admissible rule substitution lemma of section 5.4.) This theory, leading to the strengthening theorem and typechecking algorithms for classes of PTS , is detailed in [vBJMP94].

6.1 Strengthening

Strengthening is a tricky result about PTS , first proved by Jutting [vBJ93]:

\begin{matrix}∀Γ, Δ, C, d, D, q . \\ (q ∉ d ∧ q ∉ D ∧ q ∉ Δ) ⇒ \\ Γ[q:C]Δ ⊢ d : D ⇒ ΓΔ ⊢ d : D \end{matrix}  (gts strengthening)

The development we formalize, in which strengthening is a corollary to work on typechecking, is described in detail in [vBJMP94]. We were particularly interested to prove strengthening because LEGO uses it in the Discharge command.

6.2 Functional PTS

Functional PTS are well behaved and are, perhaps, the only ones that are interesting in practice.

Functional ≜ \{ \begin{matrix}ax(s:t) ∧ ax(s:u) ⇒ t = u, and \\ rl(s_{1}, s_{2}, t) ∧ rl(s_{1}, s_{2}, u) ⇒ t = u. \end{matrix}

In a functional PTS , ax and rl are the graphs of partial functions, but we do not necessarily have procedures to compute these functions.

Uniqueness of Types The definition of functional PTS makes sense for abstract-conversion PTS , and is useful in that setting, as it gives a kind of uniqueness: when building a derivation of a typing judgement guided by the syntax of its subject, it is deterministic which axiom to use at each instance of Ax, and which rule to use at each instance of Pi [Pol94b]. The idea behind the definition of functional is that the uniqueness just mentioned propagates through whole derivations to give a property that types are unique up to conversion:

      conv unique types ≜

∀Γ, M, A, B . Γ ⊢ M : A ∧ Γ ⊢ M : B ⇒ A ≃ B

For β -conversion PTS we prove

       Functional ⇒ conv unique types  (types unicity)

by structural induction on Γ ⊢ M : A and inversion of Γ ⊢ M : B. However, this proof uses properties of ≃, and cannot be modified to prove any similar property of abstract-conversion PTS . types unicity is too linear for ≤, which is only a partial order; the correct generalization is a principal types lemma, saying that any type is above some principal type, but we cannot hope that every two types are comparable [Pol94b].

Subject Expansion Any β - PTS with uniqueness of types also has a subject expansion property (subject expansion):

conv unique types ⇒

∀Γ, M, N, A, B . (M → → N ∧ Γ ⊢ N : A ∧ Γ ⊢ M : B) ⇒ Γ ⊢ M : A

While subject reduction says that terms don’t lose types under reduction, this lemma says terms don’t gain types under reduction. In this reading, Γ ⊢ N : A is the principal premise, and Γ ⊢ M : B is a wellformedness premise. There are examples of two different ways subject expansion can fail for non-functional PTS in [vBJMP94].

References

[Alt93] Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA’93. Springer-Verlag, LNCS 664, March 1993.

[Bar92] Henk Barendregt. Lambda calculi with types. In Abramsky, Gabbai, and Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.

[Bar95] Bruno Barras. Coq en coq. Master’s thesis, DEA Informatique, Mathématiques et Applications, INRIA–Rocquencourt, October 1995.

[Ber90] Stefano Berardi. Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990.

[BM] Gilles Barthe and Paul-Andre Melliès. On the subject reduction property for algebraic type systems. Presented at CSL’96; submitted for the proceedings.

[Car91] Luca Cardelli. F-sub, the system. Technical report, DEC Systems Research Centre, 1991.

[Coq91] Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

[Coq96a] Caterina Coquand. Combinator shared reduction and infinite objects in type theory. Manuscript obtained from

http://www.cs.chalmers.se, March 1996.

[Coq96b] Thierry Coquand. An algorithm for type-checking dependent types. submitted, 1996.

[DB93] Gilles Dowek and Robert Boyer. Towards checking proof checkers. In Herman Geuvers, editor, Informal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, May 1993.

[DFH^{+} 93] Dowek, Felty, Herbelin, Huet, Murthy, Parent, Paulin-Mohring, and Werner. The Coq proof assistant user’s guide, version 5.8. Technical report, INRIA-Rocquencourt, February 1993.

[Gal90] Jean Gallier. On Girard’s ‘Candidats de reductibilité’. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 123–203. Academic Press, 1990.

[Gen69] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundations of Mathematics. North-Holland, 1969. editor M. Szabo.

[Geu93] Herman Geuvers. Logics and Type Systems. PhD thesis, Department of Mathematics and Computer Science, University of Nijmegen, 1993.

[GM96] Andrew Gordon and Tom Melham. Five axioms of alpha conversion. In International Conference on Theorem Proving in Higher Order Logics, Turku, Finland, 1996. To appear.

[GN91] Herman Geuvers and Mark-Jan Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155–189, April 1991.

[Hue89] Gérard Huet. The constructive engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.

[Hue94] Gérard Huet. Residual theory in λ -calculus: A formal development. Journal of Functional Programming, 4(3):371–394, July 1994.

[JP93] Claire Jones and Randy Pollack. Incremental changes in LEGO:

1993. See http://www.dcs.ed.ac.uk/home/lego/, May 1993.

[Kle52] Stephen C. Kleene. Introduction to Metamathematics. van Nostrand, Princeton, 1952.

[LP92] Zhaohui Luo and Robert Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, Scotland, May 1992. Updated

version. See http://www.dcs.ed.ac.uk/home/lego/

[Luo91] Zhaohui Luo. Program specification and data refinement in type theory. In TAPSOFT ’91 (Volume 1), number 493 in Lecture Notes in Computer Science, pages 143–168. Springer-Verlag, 1991.

[Luo94] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.

[Mar71] Per Martin-Löf. A theory of types. Technical Report 71-3, University of Stockholm, 1971.

[McB96] Conor McBride. Inverting inductively defined predicates in LEGO. Technical report, The University of Edinburgh, 1996. forthcoming.

[Mit79] Gerd Mitschke. The standardisation theorem for λ -calculus. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 25:29–31, 1979.

[MP93] James McKinna and Robert Pollack. Pure Type Systems formalized. In M.Bezem and J.F.Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA’93, Utrecht, number 664 in LNCS, pages 289–305. Springer-Verlag, March 1993.

[Nip96] Tobias Nipkow. More Church-Rosser proofs (in isabelle/hol). In Automated Deduction – CADE-13, volume 1104 of LNCS, pages 733–747. Springer-Verlag, 1996.

[Owe95] Chris Owens. Coding binding and substitution explicitly in Isabelle. In Proceedings of the Isabelle Users’ Workshop, 1995.

[Pfe92] Frank Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, Carnegie Mellon University, September 1992.

[Plo75] Gordon Plotkin. Call-by-name, call-by-value, and the λ -calculus. Theoretical Computer Science, 1, 1975.

[Pol94a] Robert Pollack. Closure under alpha-conversion. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs: International Workshop TYPES’93, Nijmegen, May 1993, Selected Papers, volume 806 of LNCS, pages 313–332. Springer-Verlag, 1994.

[Pol94b] Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.

ftp://ftp.dcs.ed.ac.uk/pub/lego/thesis-pollack.ps.Z.

[Pol95] Robert Pollack. A verified typechecker. In M.Dezani-Ciancaglini and G.Plotkin, editors, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TL-CA’95, Edinburgh. Springer-Verlag, LNCS 902, April 1995.

[Pol96] Robert Pollack. How to believe a machine-checked proof. Talk given at TYPES’96. Submitted for publication, 1996.

[Pra65] Dag Prawitz. Natural Deduction; A Proof-Theoretical Study. Stockholm Studies in Philosophy 3. Almqvist and Wiksell, 1965.

[Reu95] Bernhard Reus. Program Verification in Synthetic Domain Theory. PhD thesis, Ludwig-Maximilians-Universität München, 1995.

[Reu96] Bernhard Reus. Synthetic domain theory in type theory: Another logic of computable functions. In Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1125 of LNCS, pages 363–381. Springer-Verlag, 1996.

[Sat83] Masahiko Sato. Theory of symbolic expressions, I. Theoretical Computer Science, 22:19–55, 1983.

[Sch97] Thomas Schreiber. Auxiliary variables and recursive procedures. In TAPSOFT’97, LNCS. Springer-Verlag, 1997. To appear.

[Sha85] N. Shankar. A mechanical proof of the Church-Rosser theorem. Technical Report 45, Institute for Computing Science, University of Texas at Austin, March 1985.

[Sto88] A. Stoughton. Substitution revisited. Theoretical Computer Science, 17:317–325, 1988.

[Tak95] Masako Takahashi. Parallel reductions in λ -calculus (revised version). Information and Computation, 118(1):120–127, April 1995.

[Tas93] A. Tasistro. Formulation of Martin-Löf’s theory of types with explicit substitutions. Master’s thesis, Chalmers Tekniska Högskola and Göteborgs Universitet, May 1993.

[vBJ93] L.S. van Benthem Jutting. Typing in Pure Type Systems. Information and Computation, 105(1):30–41, July 1993.

[vBJMP94] L.S. van Benthem Jutting, James McKinna, and Robert Pollack. Checking algorithms for Pure Type Systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs: International Workshop TYPES’93, Nijmegen, May 1993, Selected Papers, volume 806 of LNCS, pages 19–61. Springer-Verlag, 1994.