We will now define a small formal system for deriving * typing relations*
such as **in** .
To this end we have in mind the following two classes of expression.
A * type expression * has the form of a type variable (an
example of an * atomic* type) or the form , where
and are type expressions.
If we omit parentheses then arrow associates to the right; thus
is .
An * object expression* has the form of a variable, , an
abstraction, or of an application, , where **a** and **b** are
object expressions.
We say that **b** is the * body*
of and the * scope* of , a
binding operator.

In general, a variable **y** is * bound* in a term **t** if **t** has a subterm of
the form .
Any occurrence of **y** in **b** is bound.
A variable occurrence in **t** which is not bound is called * free *.
We say that a term **a** is * free for a variable x in a term t*
as long as no
free variable of

denotes the * simultaneous substitution * of for .
We agree that two terms which differ only in their bound variable
names will be treated as equal everywhere in the theory, so
will denote the same term inside the theory regardless of
capture.
Thus, for example,
=
and
=
and
= .

When we write
we mean that
names a
function whose type is .
To be more explicit about the role of **A**, namely that it
is a type variable,
we * declare * **A** in a context or environment.
The environment has the single declaration , which is read
``**A** is a type.''

For **T** a type expression and **t** an object expression,
will be called
a * typing * . To separate the context from the typing we use ` >>`.
To continue the example above,
the full expression of our goal is
.

In general we use the following terminology.
* Declarations* are either * type declarations*, in which
case they have the form , or * object declarations*, in
which case they have the form for **T** a type expression.
A * hypothesis list* has the form of a sequence of declarations; thus,
for instance,
is a hypothesis list.
In a * proper* hypothesis list the types referenced in object declarations
are declared first (i.e., to the left of the object declaration).
A * typing*
has the form , where **t** is an object expression and
**T** is a type expression.
A * goal* has the form ,
where **H** is a hypothesis list and
is a typing.

We will now give rules for proving goals.
The rules specify a finite number of subgoals
needed to achieve the goal. The rules are stated in a ``top--down''
form or, following Bates [Bates 79], * refinement*
rules. The general shape of a refinement rule is:

goal by

- 1.
- subgoal 1
- .
- .
- .
- n.
- subgoal n.

Here is a sample rule.

It reads as follows: to prove that is a function in in the
context **H** (or from hypothesis list **H**) we must achieve the subgoals
and . That is, we must
show that the body
of the function has the type **T** under the assumption that the free variable
in the body has type **S** (a proof of this will demonstrate that **T** is a
type expression), and that **S** is a type expression.

A * proof * is a finite tree whose nodes are pairs consisting of a subgoal
and a rule name or a placeholder for a rule name.
The subgoal part of a child is determined by the rule name of the parent.
The leaves of a tree have rule parts that generate no subgoals or have
placeholders instead of rule names.
A tree in which there are no placeholders is * complete *.
We will use the term * proof* to refer to both complete and incomplete
proofs.

**Figure:** Rules for the Typed Lambda Calculus

Figure gives the rules for the small theory.
Note that in rule (3) the square brackets indicate an optional part of
the rule name; if the new y part is missing then the
variable ` x` is used, so that subgoal 1 is

The ``new variable'' part of a rule name allows the user to rename variables so as to prevent capture.

We say that an * initial * goal has the form

,where the are exactly the free type variables of

Figure describes a complete proof of a simple fact. This proof provides simultaneously a derivation of , showing that is a type expression; a derivation of , showing that this is an object expression; and type information about all of the subterms, e.g.,

is in ;There is a certain conceptual economy in providing all of this information in one format, but the price is that some of the information is repeated unnecessarily. For example, we show that three separate times. This is an inherent difficulty with the style of ``simultaneous proof'' adopted in Nuprl . In chapter 10 we discuss ways of minimizing its negative effects; for example, one could prove once as a lemma and cite it as necessary, thereby sparing some repetition.

is in given ;

is in ;

is in .

**Figure:** A Sample Proof in the Small Type Theory

It is noteworthy that from a complete proof from an initial
goal of the form we know that **t** is a closed object
expression (one with no free variables) and **T** is a type expression whose
free variables are declared in **H**.
Also, in all hypotheses lists in all subgoals any expression appearing
on the right side of a declaration is either or a type
expression whose variables are declared to the left.
Moreover, all
free variables of the conclusion in any subgoal are declared exactly
once in the corresponding hypothesis list.
In fact, no variable is declared at a subgoal unless it is free
in the conclusion.
Furthermore, every subterm receives a type in
a subproof , and in an application , , **f** will
receive a type and **a** will receive the type .
Properties of this variety can be proved by induction on
the construction of a complete proof.
For full Nuprl
many properties like these are proved in the
Ph.D. theses of R. W. Harper [Harper 85] and S. F. Allen [Allen 86].

Thu Sep 14 08:45:18 EDT 1995