next up previous contents
Next: Refinements: Embedded Theorems and Up: Declarations Previous: Relative Type and Stratification

Predicativity and Opacity

Certain special conditions complicate the definitions of weak stratification and stratification. Theories started with the clearpredicative command place the restriction on stratified or weakly stratified terms that no variables of appropriate types occur within any variable binding context or in the left (right) subterm of an operator term if the left (right) type of the operator happens to be negative. The impredicative command lifts this restriction for a theory. This used to be the default state of the prover, so theory files produced with old versions of the prover may be in this state.

The declareopaque command can be used to place additional restrictions on stratification notions. Operators may be declared ``opaque''; a term built with an opaque operator should not contain any variables of the kind under consideration to be stratified or a subterm of a stratified term. The declareopaque command has an additional application: it can be used to block the later declaration of an untyped operator variable as typed. Operator variables which are not declared with types are treated as opaque in any case, since relative types cannot be assigned to subterms of terms built with such operators. The declareopaque command can only be used to declare a new operator; existing operators cannot be made opaque.

In the case of weak stratification, the restrictions indicated in case of predicativity or opacity apply only to bound variables; in case of full stratification, they apply to all variables.

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