next up previous contents index
Next: Relationship to Set Up: Introduction to Type Previous: Sets and Quotients


This section is included for technical completeness; the beginning reader may wish to skip this section on a first reading. Here we shall consider only briefly the semantics.  The complete introduction appears in section gif. The semantics of are given in terms of a system of computation and in terms of criteria for something being a type, for equality of types, for something being a member of a given type and for equality between members in a given type.

The basic objects of are called terms.  They are built using variables and operators, some of which bind variables in the usual sense. Each occurrence of a variable in a term is either free  or bound.  Examples of free and bound variables from other contexts are:

By a closed  term we mean a term in which no variables are free. Central to the definitions of computation in the system is a procedure for evaluating  closed terms. For some terms this procedure will not halt, and for some it will halt without specifying a result. When evaluation of a term does specify a result, this value will be a closed term called a canonical  term. Each closed term is either canonical or noncanonical,  and each canonical term has itself as value.

Certain closed terms are designated as types;  we may write ``T type'' to mean that T is a type. Types always evaluate to canonical types.  Each type may have associated with it closed terms which are called its members;  we may write ``'' to mean that t is a member of T. The members of a type are the (closed) terms that have as values the canonical members of the type, so it is enough when specifiying the membership of a type to specify its canonical members. Also associated with each type is an equivalence relation on its members called the equality  in (or on) that type; we write ``'' to mean that t and s are members of T which satisfy equality in T. Members of a type are equal (in that type) if and only if their values are equal (in that type).

There is also an equivalence relation T = S on types called type  equality.  Two types are equal if and only if they evaluate to equal types. Although equal types have the same membership and equality, in some unequal types also have the same membership and equality.

We shall want to have simultaneous  substitution of terms, perhaps containing free variables, for free variables. The result of such a substitution is indicated thus:

where , are variables, and are the terms substituted for them in t.

What follows describes inductively the type terms in Nuprl and their canonical members. We use typewriter font to signify actual Nuprl syntax. The integers are the canonical members of the type int. There are denumerably many atom constants (written as character strings enclosed in quotes) which are the canonical members of the type atom.  The type void  is empty.  The type A|B is a disjoint union   of types A and B. The terms inl(a) and inr(b) are canonical members of A|B so long as and . (The operator names inl and inr are mnemonic for ``inject   left'' and ``inject  right'' .) The canonical  members of the cartesian product type A#B  are the terms <a,b>  with and . If x:A#B is a type then A is closed  (all types are closed) and only x is free in B. The canonical members of a type x:A#B (``dependent product'')   are the terms <a,b> with and . Note that the type from which the second component is selected may depend on the first component. The occurrences of x in B become bound  in x:A#B. Any free  variables of A, however, remain free in x:A#B. The x in front of the colon is also bound, and indeed it is this position in the term which determines which variable in B becomes bound. The canonical members of the type A list  represent lists of members of A. The empty  list is represented by nil,  while a nonempty list with head  a and tail  b is represented by a.b, where b evaluates to a member of the type A list.

A term of the form t(a) is called an application  of t to a, and a is called its argument.  The members of type A->B are called functions,  and each canonical member is a lambda term,  \ x.b, whose application to any member of A is a member of B. The canonical members of a type x:A->B,  also called functions, are lambda terms whose applications to any member a of A are members of . In the term x:A->B the occurrences of x free in B become bound, as does the x in front of the colon. For these function types it is required that applications of a member to equal members of A be equal in the appropriate type.

The significance of some constructors derives from the representation of propositions  as types, where the proposition represented by a type is true if and only if the type is inhabited. The term a<b is a type if a and b are members of int , and it is inhabited  if and only if the value of a is less than the value of b. The term (a=b in A) is a type if a and b are members of A, and it is inhabited if and only if . The term (a=a in A) is also written (a in A); this term is a type and is inhabited if and only if .

Types of form {A|B} or {x:A|B} are called set types.  The set constructor provides a device for specifying subtypes;  for example, {x:int|0<x} has just the positive integers as canonical members. The type {A|B} is inhabited if and only if the types A and B are, and if it is inhabited it has the same membership as A. The members of a type {x:A|B} are the members a of A such that is inhabited. In {x:A|B}, the x before the colon and the free x's of B become bound.

Terms of the form A//B and (x,y):A//B are called quotient types.  A//B is a type only if B is inhabited, in which case exactly when a and are members of A. Now consider (x,y):A//B. This term denotes a type exactly when A is a type, is a type for a and in A, and the relation is an equivalence relation over A in a and . If (x,y):A//B is a type then its members are the members of A; the difference between this type and A only arises in the equality between elements. Briefly, if and only if a and are members of A and

is inhabited. In (x,y):A//B the x and y before the colon and the free occurrences of x and y in B become bound.

Now consider equality on the types already discussed.  Members of int are equal (in int) if and only if they have the same value. The same goes for type atom. Canonical members of A|B, A#B, x:A#B and A list are equal if and only if they have the same outermost operator and their corresponding immediate subterms are equal (in the corresponding types). Members of A->B or x:A->B are equal if and only if their applications to any member a of A are equal in . The types a<b and (a=b in A) have at most one canonical member, namely axiom, so equality is trivial. Equality in {x:A|B} is just the restriction of equality in A to {x:A|B}, as is the equality for {A|B}.

Now consider the so--called universes,  Uk (k positive). The members of Uk are types.  The universes are cumulative;  that is, if j is less than k then membership and equality in Uj are just restrictions of membership and equality in Uk. Uk is closed  under all the type--forming operations except formation of Ui for i greater than or equal to k. Equality in Uk is the restriction of type equality to members of Uk.

With the type theory in hand we now turn to the Nuprl proof theory. The assertions that one tries to prove in the system are called judgements.  They have the form

where are distinct variables and and s are terms (n may be 0), every free  variable of is one of , and every free variable of S or of s is one of . The list is called the hypothesis  list or assumption  list, each : is called a declaration  (of ), each is called a hypothesis  or assumption,  S is called the consequent or conclusion,  s the extract term (the reason will be seen later), and the whole thing is called a sequent. 

The criterion for a judgement being true  is to be found in the complete introduction to the semantics.gif Here we shall say a judgement
is almost true  if and only if
* if
That is, a sequent like the one above is almost true exactly when substituting terms of type (where and may depend on and for j<i) for the corrseponding free variables in s and S results in a true membership relation between s and S.

It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, the extract term or any hypothesis, then the variable (and the colon following it) may be omitted.

In it is not possible for the user to enter a complete sequent directly; the extract term must be omitted. In fact, a sequent is never displayed with its extract  term. The system has been designed so that upon completion of a proof, the system automatically provides, or extracts,  the extract term. This is because in the standard mode of use the user tries to prove that a certain type is inhabited without regard to the identity of any member. In this mode the user thinks of the type (that is to be shown inhabited) as a proposition and assumes that it is merely the truth of this proposition that the user wants to show. When one does wish to show explicitly that or that , one instead shows the type (a = b in A) or the type (a in A) to be inhabited.gif

The system can often extract a term from an incomplete  proof when the extraction is independent of the extract terms of any unproven claims within the proof body. Of course, such unproven claims may still contribute to the truth of the proof's main claim. For example, it is possible to provide an incomplete proof of the untrue sequent >> 1<1 [ext axiom], the extract term axiom being provided automatically.

Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. In the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.

next up previous contents index
Next: Relationship to Set Up: Introduction to Type Previous: Sets and Quotients

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995