In this subsubsection, we discuss the implementation of the notion of stratification under Watson. Each operator in Watson must be declared with a ``left type'' and a ``right type'' which determine the displacement of the relative types of the left and right subterms of a term built with that operator from the relative type of the term. A strict prefix operator only needs a right type.
An alternative is to declare an operator as ``opaque'': abstraction into a term built with an opaque operator is not permitted, so such a term may not contain any locally free bound variable. Variable operators may be declared opaque if it is desired (as in structural tactics such as RIGHT above) that the variable operator match operators with arbitrary relative types. Variable operators can also be declared with specific relative types. Undeclared variable operators are treated as opaque. This is the main application of opaque operators in existing theories, though there are sensible applications of ``constant'' opaque operators in mathematics, and it turns out that defined operators used as type constructors (for types represented as retractions onto strongly Cantorian domains) need to be opaque.
The assignment of relative types to occurrences of subterms of a term then proceeds as follows: the relative types of the left and right subterms of a term built with an infix operator are obtained by adding the left and right types (respectively) to the type of the whole subterm; the right subterm of a term built with a strict prefix operator is handled in the same way. The immediate proper subterm of an abstraction term has relative type one lower than the abstraction term, and the immediate subterm must have the same relative type as all occurrences in the abstraction term of the bound variable bound in the abstraction term (this is the condition of stratification).