A Formal System

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 a becomes bound when a is substituted for each free occurrence of x. For example, z is free for x in , but y is not. If a has a free variable which becomes bound as a result of a substitution then we say that the variable has been captured . Thus ``captures'' y if we try to substitute y for x in . If t is a term then denotes the term which results from replacing each free occurrence of x in t by a, provided that a is free for x in t. If a is not free for x then denotes t with a replacing each free x and the bound variables of t which would capture free variables of a being renamed to prevent capture.

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

,

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 ;
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].