Output freeness

When STELF proves that an LF type family defines a total relation, it checks that the output of each premise of each constant can never fail to unify with an output that is actually produced. This is called output coverage checking. One way in which a premise can fail output coverage checking is if its output is a metavariable that is constrained by appearing elsewhere in the constant.

Output freeness checking ensures that no outputs are constrained in such a manner. More precisely, the output freeness check ensures that a metavariable in an output position does not occur in any previous input or output (where “previous” is the same order used in %mode checking—i.e., the search order of the logic programming operational semantics).

Prior to STELF 1.5, output freeness checking was not implemented, allowing some false metatheorems to check.

Simple example

As a first output freeness violation, consider the natural numbers

%sort nat %.
%term s %pi nat %-> nat %.
%term z nat %.

and following buggy definition of the addition relation:

add : nat -> nat -> nat -> type.
%mode add +M +N -O.

add/z : add M z M.

add/s-incorrect : add M (s N) (s N)
                   <- add M N N.

%worlds () (add _ _ _).
%total N (add _ N _).

This type family add clearly does not define a total relation: the constant add/s-incorrect only applies when add M N N, but in general it is possible to derive add M N O for O not equal to N (and the constant add-s-incorrect is the only constant that covers the case when the second number is a successor, so the relation is clearly not total without this constant).

Thus, STELF reports an output coverage error on this constant when we attempt to check totality. Specifically, an output freeness error: the output metavariable N occurs previously because N is an input to the relation.

Uniqueness example

It is common to encounter output freeness errors when working with relations that have unique outputs. For example, consider a correct definition of add:

%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add M z M %.
%term add/s-incorrect %pi (add M (s N) (s O)) %<- (add M N O) %.
%worlds () (add _ _ _) %.
%total N (add _ N _) %.