next up previous contents
Next: Predicativity and Opacity Up: Declarations Previous: Declarations

Relative Type and Stratification

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.


next up previous contents
Next: Predicativity and Opacity Up: Declarations Previous: Declarations

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997