Some Lambda Calculus and Type Theory Formalized.
We survey a substantial body of knowledge about lambda calculus and Pure Type Systems, formally developed in a constructive type theory using the LEGO proof system. On lambda calculus, we work up to an abstract, simplified proof of standardization for beta reduction that does not mention redex positions or residuals. Then we outline the meta theory of Pure Type Systems, leading to the strengthening lemma. One novelty is our use of named variables for the formalization. Along the way we point out what we feel has been learned about general issues of formalizing mathematics, emphasizing the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts.
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
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
Submitted to Journal of Automated Reasoning
y A version of this paper appears as technical report ECS-LFCS-97-359, University
of Edinburgh.
z Laboratory for Foundations of Computer Science, University of Edinburgh
x Basic Research in Computer Science, University of Aarhus. Centre of the Danish
National Research Foundation.
information on accessing the formal development described in this pa-
per. 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].
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 re-
sults, 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 under-
stood, 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 grow-
ing, 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 math-
ematics: 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, Bar96]; both of these address
limited aspects of very special type theories (essentially the Calculus of
Constructions), although [Bar96] 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 [Bar96], 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, Bar96] 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-of'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-of'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 .
This distinction is already present in Gentzen [Gen69, pages 71-2, 116-7, 141,
216-7] and Prawitz [Pra65]
2 The dependencies are determined from the module headers, not by examining
There are over 70 proof source files with extension .l
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.
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 T E X.
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 [Pol97] 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 sur-
press 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.
the actual dependencies in the files.
3 The .l files are the ones we wrote; LEGO generates "compiled" files with a .o
extension. These are the fully annotated -terms generated by the LEGO tactics
called in the .l file.
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
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 .
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
ffl PP is an infinite set of parameters, ranged over by p , q , r ; these
are the global, or free, variables.
ffl VV is an infinite set of variables, ranged over by v , x , y ; these
are the local, or bound, variables.
ffl 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.
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.
4 In 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
atoms: variable, parameter, sort
binders: lambda, pi
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 fv:AgB
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 hv:Aia 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

Two properties of this measure are used applications: if A is a proper
subterm of B then (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(hv:Aia) , params(A) @ params(a)
Similarly 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]ff , ff ff 2 VV; SS
[a=p]hv:Bib , hv:[a=p]Bi[a=p]b
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]ff , ff ff 2 PP; SS
[a=v]hx:Bib , hx:[a=v]Biif(v=x; b; [a=v]b)
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:
Vcl-atom Vclosed(ff) ff 2 PP [ SS
Vcl-bind

Table

1: Inductive definition of the relation Vclosed .
and we have a ready supply of terms of the shape [p=v]M , with
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 hv:Aia 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
Vclosed Generation Lemmas Suppose you have a proof of
examining it you know it must
be constructed by Vcl-bind from proofs of Vclosed(A) and
no other rule for Vclosed has a conclusion
of shape Vclosed( hv:AiB ) . 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
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).
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
aVcl-bind
We will show that Vclosed and aVclosed derive the same judgements.
Induction over aVclosed is the principle which Melham and Gordon
rediscovered [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)
Both directions follow easily by structural inductions once we have the
following claim (aVclosed alpha):
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
Now using term structural induction on A , we have cases for sort, vari-
able, 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] hn:AiB ) , i.e.
under the assumptions
(i.e. aVclosed(hn:[p=v]Aiif(v=n; B; [p=v]B)))
By aVclosed inversion applied to assumption vclp we also know
By aVcl-bind, it suffices to show
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 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 6= n we use a straightfoward lemma
(alpha commutes alpha)
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
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 \Theta PP (renaming pair)
Renaming , list(rp)
ae and oe 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.
aep , (assoc p p ae)
aeff , ff (ff 2 VV; SS)
aehv:Aia , hv:aeAiaea
ae(M N) , ae(M) ae(N)
This is a "tricky" representation. First, if there is no pair (p; q) in ae ,
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 func-
tional, 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:
Renaming is iterated substitution. We can analyse the action of
a renaming in terms of substitution (renTrm is conjugated psub):
From this lemma it is easy to show that renaming respects any relation
that substitution of parameters respects (psub resp renTrm resp):
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:
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:
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 fi and - rules are:
The substitution [N=x]M on the RHS of fi 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 fi under a binder, as allowed by - , we must preserve the
invariant that fi 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):
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 6= x .
However - does not derive the incorrect judgement
because
Thus incorrect capture is avoided.
3.1 Parallel Reduction
Rather than use ordinary fi -reduction, we take parallel reduction ('a
la Tait-Martin-L-of) 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 62 . These are eigenvariable
pr1-atom ff ![
pr1-beta
A ![
Vclosed(U)
pr1-bind
A ![
pr1-app
A ![

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)
and ![
is reflexive on Vclosed terms (par red1 refl)
A stronger induction principle for ![
The rules pr1-atom, pr1-
bind 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
~
pr1 -bind
A ~
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
5 Kleene [Kle52, x78, 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.
to show the equivalence. We omit the details, but a similar argument
is used in section 5.2.1.
The strong induction principle is used to show that ![
is closed
under substitution (par red1 psub):
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 ff -conversion, ff
- , to be the least congruence, i.e. ff
- is exactly
without the rule pr1-beta, so ff
. This definition is
symmetric, by inspection. To show that it is transitive requires the
stronger induction principle for ff
- , which we prove in the same way as
above. Hence ff
- is an equivalence relation 6 . It is decidable for Vclosed
terms (decide alpha conv):
ff
with a straightfoward but messy proof, by double induction on
and aVclosed(B) .
Informally, alpha-conversion is used for changing the names of vari-
ables. We do not have hx:AiB ff
does
not prevent capture. However, we do have (true alpha conv pi):
Closure under ff -conversion One of Coquand's original motivations
for distinguishing between variables and parameters was to avoid
the need to reason about ff -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 ff -conversion, so that when we formalise a relation R such
as parallel reduction above, we really intend R modulo the quotient
structure, i.e. ff
- . We say a relation R is:
6 This should be contrasted with Gallier's meticulous but long-winded treatment
in [Gal90].
closed under ff if ffffiR ' Rffiff ; strongly closed, if ffffiR ' R ;
full wrt ff if Rffiff ' ffffiR ; strongly full, if Rffiff ' R .
Remark 3.1 ![
is strongly closed under ff -conversion: the proof is
the same as that for transitivity of ff
- , with the additional case of a
redex handled by observing that an ff -variant of a redex is a redex.
However ![
is not full w.r.t. ff
-classes. For example
but no ff -variant of the LHS ![
-reduces to ( [y 1 :q]y 1
although this is an ff -variant of the RHS.
3.1.3 A Church-Rosser Theorem
Using the argument of Tait and Martin-L-of, as modernized in [Tak95],
we prove the first CR theorem (par redn DP):
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, \Gamma![
, (comp dev)
7 . It is given by the same rules as ![
except for the application rule:
cd-app
A \Gamma![
AB \Gamma![
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:
ffl induction on the definition of \Gamma![
, which we may think of as a
partial correctness assertion;
ffl the existence (for Vclosed terms) of complete developments,
(comp dev exists), which we may think of as a termination argument

7 cf. the definition of \Gamma![
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
\Gamma![
, a subsidiary induction (case-analysis) to resolve the redex/non-
redex distinction in the case of an application. This is handled once
and for all in the existence proof, while induction on the definition of
\Gamma![
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):
whose proof is by induction on M \Gamma![ M 0 , 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 ff -conversion.
This is because both the ![
and \Gamma![
relations are strongly closed under
ff -conversion. Indeed, we may show the following two properties, which
strengthen comp dev exists, namely comp dev unique:
and comp dev exists unique:
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):
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 ( AB )
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 !
(normal
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)
Any reduct of a normal form alpha-converts with that normal form
(par-redn-bnorm-is-alpha-conv)
Hence, by Church-Rosser, normal forms of a term are unique up to
alpha-conversion (nf-unique). Since ff
, the converse also holds
(nf-alpha-class)
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
A !wh A 0

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):
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 reduc-
tion, 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 weak-
head normal forms (Table 4), and various lemmas relating !wh and
wh-atom whnf(ff) ff 2 PP [ SS
wh-bind
A is not a lambda

Table

4: Weak-head normal forms
ip1-atom ff![
ip1-bind

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, iwh , (wh redn) is defined as
the reflexive transitive closure of !wh . It is closed under renam-
ings, substitution (psub resp wh redn), and application on the right
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 re-
duction, which gives us the definition of internal parallel reduction, ![
(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 ![
preserves and reflects weak-
head 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)
Proof. The proof proceeds by induction on M![
. The only tricky
case is that of the parallel fi step. By inductive hypothesis, we obtain
(introducing Skolem constants Aw ; Bw )
and we are required to show that there exists some Mw such that
Since
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):
This is proved in the same way as we showed closure of parallel reduction
under substitution, by induction on M![
. A detail to observe
here is that we must explicitly assume that the reduction from N to
N 0 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
and B![
. By induction hypothesis, there exists some PA such
that [N=p]A iwh PA![
. The proof of the claim, and hence
of the whole lemma, is completed by taking P= def PA ( [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):
This is a corollary (by induction on Mw iwh M 0 ) of the following
lemma (ipar wh red1 commutes):
Proof. Induction on M![
of the ancillary hypothesis
All cases are trivial, except that of application
. We show
the case of a wh-redex, where we have:
and We use the fact that ipar red1 reflects the
weak-head normal form A to infer that A = [u:U ]A 000 .
Moreover, since A![
by inversion that U![
V and
8p: [p=u]A 000 ![
[p=v]A 00 . Choosing p 62 A 00 ; p 62 A 000 , and applying
pr1-sub, we obtain [B=u]A 000 ![
Now we appeal to
Lemma 3.4.2, finally to conclude that for some P , we have
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 in-
variants. Such refinements to these arguments would be inconceivable
without machine support.
3.4.3 Standard Reduction
The property of being a standard reduction, \Gamma! 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 ff\Gamma! s ff ff 2 PP [ SS
std-bind
std-app
std-wh

Table

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
note furthermore, however, that we may easily achieve this end
by adding the side condition A 0 6= - to the std-app rule, and whnf(B)
to the std-wh rule. Also, this definition is both strongly closed under
ff -conversion, and strongly full.
Our final aim is the following standardization theorem
(the standardisation lemma):
Induction on A !
suffices if we can show that our notion of standard
reduction absorbs single steps of parallel reduction:
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):
Proof. The proof is by induction on B \Gamma! s C . This avoids reconsidering
the tricky application case of the commutation lemma above, and
we may exploit the fact
preserves and reflects the shape of
terms. The price we pay is the need for strong induction on B \Gamma! s C ,
as the ancillary hypothesis A![
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:
By inversion of H, we conclude that
A
and 8p: [p=w]B c ![
[p=u]B . But now by semi-standardization,
A c iwh Aw![
. So by induction
hypothesis ihA, we have Aw \Gamma! s A 0 , and using std-wh to fold back the
reductions A c iwh Aw , we finally obtain A c \Gamma! s A 0 . In exactly
the same way, modulo the choice of a parameter
we obtain [p=w]B c \Gamma! s [p=v]B 0 . But now C \Gamma! s hv:A 0 iB 0 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) fi -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
informally as ax(s 1 :s 2 )
Start
Weak
Lda
App

Table

7: The Typing Rules of PTS (formal name gts)
ffl rules, rl ' SS \Theta SS \Theta SS , written informally as rl(s
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 meaning that in
has type A . (The formal name of this relation
is gts, from the old name "Generalized Type Systems".) We call M
(or (\Gamma; M) ) the subject and A the predicate of judgement. Contexts,
ranged over by \Gamma , \Delta , bind parameters to types:
Contexts are formalized as lists over PP \Theta Trm . If \Gamma participates in
some derivable judgement,
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 trans 8A;
To prove the subject reduction theorem (section 5.5), we finally need
that conversion is related to contraction of redexes, and has an "inter-
nal" Church-Rosser property:
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:
Some differences between abstract-conversion- PTS and fi -conversion-
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)
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)
where we restrict to atomic terms, ff (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
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
The conventional understanding is that the bound variable, x , doesn't
really occur in the conclusion of rule - , as the notations "
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,
rule - as
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 theo-
rem. 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:
(free params lem1)
8 However, in the left premise of rule - , all free instances of the actual symbol
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:
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.
aLda
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 62 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 \Gamma[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 \Gamma[p:A]
remains valid, i.e. those p not occurring in \Gamma . However the condition
not required because of "genericity", that is, the right premise
of aPi must hold for the infinitely many parameters not occurring in
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 ' .
(apts gts; gts apts)
Proof. Direction ) is straightfoward by structural induction on
To prove direction ( , first prove a lemma that bijective renamings
respect ' a
(bij ren resp apts)
by ' a
-structural induction 9 .
Now we proceed to prove
by structural
induction on a derivation of All cases are trivial except
for the rules Pi and Lda. Consider the case for Pi: we must prove
under the assumptions
l prem
prem
By rule aPi (using l ih) it suffices to show \Gamma[r:A] ' a
arbitrary parameter r 62 \Gamma . Thus, using the free parameter lemmas of
section 5.1, we know
A from l prem and noccG
prem
prem
Taking
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
It is clear that the first equation holds from nopG, noccG, norA and
nopA. For the second equation, notice that if then we are done
trivially, so assume r 6= p , and hence r 62 [p=n]B (from r prem and
noccG). Now, using vsub renTrm commutes (section 2.5) we have
9 Actually 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
We also say \Delta extends \Gamma . 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):
A naive attempt to prove the thinning lemma by structural induction
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
(substitution lemma)
is proved by induction on the derivation of \Gamma[p : From
this we get the commonly used case (cut rule) by instantiating \Delta 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):
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).
Subject Reduction Theorem: Closure Under Reductio

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
usually called the subject reduction theorem. Our naive strategy is
to show that one step of reduction preserves typing, by induction on
. 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 fi -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
where ! is ordinary one-step fi -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 non-overlapping
reduction, no
(no red1), is defined by the same rules as ![
(table 2) except for the fi -rule, which is modified to prevent overlapping
redexes:
nor1-beta ( [u:U ]B ) A no
no
, so from the assumed property cnv conv (section 4.1),
we have
A no
We extend no
compositionally to contexts (red1Cxt), and to
pairs of a context and a term (red1Subj), writing \Gamma no
h\Gamma; Mi no
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)
Proof. By structural induction on We show the interesting
case, from rule App. Given
l prem
prem
red
we must show . By induction hypotheses
By type correctness of gtsDM, for some s
By the pi-generation lemma, for some s 2 and p 62 B
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)
Now there are two subcases
!M 0 and L no
The goal is rule App and the induction hypotheses
we easily have Use rule tCnv and gts-
DBsub to expand L 0 in the predicate back to L as required (this uses
cnv-conv).
The goal is
by the lambda-generation lemma, for some w , B 0 and s 0
By (cnvCR-pi c') (this is the only time it is used in this proof)
By a generation lemma on gtsDpi'
By (tCnv cnvA gtsDL gtsDA')
By tCnv, cnvB and gtsDBsub, it suffices to show
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
Finally, extending !
compositionally to contexts 10 , ' is closed under
beta-reduction (gtsAllRed)
This relation is equivalent to transitively closing the compositional extension of
of no
! to contexts.
There is a trivial but useful lemma (predicate conv):
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 ff
, it follows that ' judgements are preserved by ff
(gts alpha closed). Hence an implementation may typecheck a
judgement as stated by a user, rather than searching for an alpha-
equivalent judgement which is derivable. See [Pol94b, Pol94a].
5.6 Another Presentations of PTS
In several rules of ' the context \Gamma occurs more then once in the list
of premises; in order to build a complete derivation, \Gamma 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-of [Mar71], and is used in [Hue89].
This system has two judgements, a type judgment of shape
(lvtyp), and a validity judgement of shape \Gamma ' 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):
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].
lvLda
lvCons

Table

8: The system of locally valid contexts (lvtyp, lvcxt)
6 PTS with fi -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 fi -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 Jut-
ting [vBJ93]:
\Gamma[q:C
(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 ,
ae
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 ,
For fi -conversion PTS we prove
Functional ) conv unique types (types unicity)
by structural induction on
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 fi - PTS with uniqueness of types also has
a subject expansion property (subject expansion):
conv unique types )
While subject reduction says that terms don't lose types under reduc-
tion, this lemma says terms don't gain types under reduction. In this
A is the principal premise, and is a well-formedness
premise. There are examples of two different ways subject
expansion can fail for non-functional PTS in [vBJMP94].



--R

A formalization of the strong normalization proof for System F in LEGO.
Lambda calculi with types.
Coq en Coq.
Type Dependence and Constructive Mathemat- ics
On the subject reduction property for algebraic type systems.
F-sub, the system.
An algorithm for testing conversion in type theory.
Combinator shared reduction and infinite objects in type theory.
An algorithm for type-checking dependent types
Towards checking proof checkers.

On Girard's
The Collected Papers of Gerhard Gentzen.
Logics and Type Systems.
Five axioms of alpha con- version
A modular proof of strong normalization for the calculus of constructions.
The constructive engine.
Residual theory in
Incremental changes in LEGO:
Introduction to Metamathematics.
LEGO proof development sys- tem: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King's Buildings
Program specification and data refinement in type theory.
Computation and Reasoning: A Type Theory for Computer Science.
Per Martin-L-of
Inverting inductively defined predicates in LEGO.
The standardisation theorem for
Pure Type Systems for- malized
More Church-Rosser proofs (in isabelle/hol)
Coding binding and substitution explicitly in Is- abelle
A proof of the Church-Rosser theorem and its representation in a logical framework

Closure under alpha-conversion
The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions.
A verified typechecker.
How to believe a machine-checked proof
Natural Deduction
Program Verification in Synthetic Domain The- ory
Synthetic domain theory in type theory: Another logic of computable functions.
Theory of symbolic expressions
Auxiliary variables and recursive procedures.
A mechanical proof of the Church-Rosser theorem
Substitution revisited.
Parallel reductions in
Formulation of Martin-L-of's theory of types with explicit substitutions. Master's thesis


--TR

--CTR
Michael Norrish, Mechanising Hankin and Barendregt using the Gordon-Melham axioms, Proceedings of the ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-7, August 26, 2003, Uppsala, Sweden
Christian Urban , Michael Norrish, A formal treatment of the barendregt variable convention in rule inductions, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.25-32, September 30-30, 2005, Tallinn, Estonia
Yasuhiko Minamide , Koji Okuma, Verifying CPS transformations in Isabelle/HOL, Proceedings of the ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-8, August 26, 2003, Uppsala, Sweden
Michael Norrish, Mechanising -calculus using a classical first order theory of terms with permutations, Higher-Order and Symbolic Computation, v.19 n.2-3, p.169-195, September 2006
S. J. Ambler , R. L. Crole , Alberto Momigliano, A definitional approach to primitivexs recursion over higher order abstract syntax, Proceedings of the ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-11, August 26, 2003, Uppsala, Sweden
Dimitri Hendriks, Proof Reflection in Coq, Journal of Automated Reasoning, v.29 n.3-4, p.277-307, 2002
Jonathan Ford , Ian A. Mason, Formal Foundations of Operational Semantics, Higher-Order and Symbolic Computation, v.16 n.3, p.161-202, September
Conor McBride , James McKinna, Functional pearl: i am not a number--i am a free variable, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA
James Cheney, Scrap your nameplate: (functional pearl), ACM SIGPLAN Notices, v.40 n.9, September 2005
Thierry Coquand , Randy Pollack , Makoto Takeyama, A Logical Framework with Dependently Typed Records, Fundamenta Informaticae, v.65 n.1-2, p.113-134, January 2005
Ren Vestergaard , James Brotherston, A formalised first-order confluence proof for the -calculus using one-sorted variable names, Information and Computation, v.183 n.2, p.212-244, 15 June
Andrew M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, v.186 n.2, p.165-193, 01 November
Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004
Riccardo Pucella, SIGACT news logic column 14, ACM SIGACT News, v.36 n.4, December 2005
type theory;LEGO proof checker;formal mathematics;lambda calculus;Pure Type Systems