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:
- subgoal 1
- 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 T. The Nuprl system allows only initial goals with empty hypothesis lists. Also, in full Nuprl we do not distinguish type variables from any other kind of variable. We have introduced these special notions here as pedagogical devices.
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].