The stratification function has recently been refined in two ways.
Where embedded theorem names appear, they are checked for
stratification internally but their type relative to the term to which
they are attached is not checked. This is safe, since embedded
theorems have no effect on term value. In addition, a predeclared
infix `:` is provided which serves to generate type labels: the
term `t : x` is the result of applying a retraction to `x`,
determined by `t`, whose range is a ``strongly Cantorian set'' (a
technical notion in set theories related to New Foundations). This
has the effect of allowing the term to be freely raised and lowered in
type. The effect of this on stratification is that one may freely
raise and lower the types assigned to `x` and its subterms for
purposes of stratifying the term in which it occurs; the type label
should contain no type information (any variables in `t` must be
restricted to strongly Cantorian sets). The only way in which types
in `x` may influence stratification is that the difference between
the types of two variables occurring in `x` may be fixed, and this
will have to agree with the stratification of the context. This is
motivated by the theoretical claim which we have made (in our paper in
*Modern Logic*, vol. 4, no. 1) that ``strongly Cantorian set''
corresponds to ``data type'' in a model of computing based on this
kind of set theory.

A further refinement along the same lines is that functions and
operators whose input or output is restricted to a ``type'' (strongly
Cantorian set) (this must be witnessed by a theorem) can be declared
as ``scin'' (for strongly Cantorian input) or ``scout'' (for strongly
Cantorian output). Stratification restrictions are relaxed
accordingly, without any need for explicit type labels. For example,
the equality infix `=` or a universal quantifier function `
forall` can be declared ``scout'', since their output is boolean, and
so the stratification function of the prover can exploit the fact that
types of boolean-valued expressions can be freely raised and lowered
in order to permit more complex abstractions. This feature should
have the effect of minimizing the use of explicit type labels. Note
that any use of operators declared ``scin'' or ``scout'' in abstraction
terms has the effect of introducing dependencies on the witnessing
theorems for those operators.

Examples of permissible types are booleans (or any finite set) and natural numbers. Cartesian products and function spaces built from strongly Cantorian sets are strongly Cantorian. Recursive and polymorphic type constructions will also work. The system of absolute types which can be built under Mark2 is thus as strong as that usually used in computer science.

Fri Sep 5 16:28:58 MDT 1997