In any term, each subterm can be assigned a *relative type* in
accordance with the following procedure: the relative type of the
entire term is 0; the relative type of the left/right subterm of a
variable binding context is one less than the relative type of the
variable-binding context; the relative type of the left (right)
subterm of an operator term is obtained by adding the left (right)
type of the operator to the relative type of the operator term.

A variable binding context entered by the user must have the property
that the relative type of each occurrence of the variable bound in it
is the same as the relative type of its left/right subterm. Terms
violating this condition can be created during proofs but cannot be
stored in theorems. Terms satisfying this condition for all subterms
which are variable binding contexts are said to be *weakly
stratified*.

A term is said to be *stratified* if it is weakly stratified
and, in addition, each free variable appears with no more than one
relative type. This notion is used in the definition facility.

These notions are best understood if one imagines (as is not the case)
that each term has an integer type associated with it. Type *n* will
be identified with the Cartesian product of type *n* and type *n*
(relative types of the infix `,` of ordered pairing are both 0)
while type *n*+1 is the type of functions from type *n* to type *n*.
This explains the typing of variable binding contexts (lambda-terms)
and is also illustrated by the fact that the left type of the infix
`@` of function application is 1 and its right type is 0. The
type theory being implemented can be thought of as a polymorphic
version of simple type theory with a linear hierarchy of function
types rather than set types; in fact, the types are all identified as
in Quine's New Foundations. Any difficulty with the open problem of
the consistency of New Foundations is avoided by not requiring that
function application be extensional; New Foundations with urelements
is known to be consistent.

Fri Sep 5 16:28:58 MDT 1997