POPL Tutorial/Basic error messages

How STELF checks assertions

STELF proves a totality assertion for a type family such as mult by checking several properties. These properties, taken together, constitute a proof by induction on canonical forms that the type family defines a total relation.

Running Example

We’ll start from the following code:

%sort nat %.
%term zero nat %.
%term succ %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add zero N N %.
%term add/s %pi (add (succ M) N (succ P)) %<- (add M N P) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.
%sort mult {_ nat} {_ nat} {_ nat} %.
%mode mult %in %in %out %.
%term mult/z mult zero N zero %.
%term mult/s %pi (mult (succ M) N P') %<- (mult M N P) %<- (add N P P') %.

Mode

STELF checks that each constant inhabiting the type family is well-moded. Roughly, this means that the inputs to the conclusion of a constant determine the inputs of the first premise, and that these together with the outputs of the first premise determine the inputs of the second premise, and so on, until the outputs of all the premises determine the outputs of the conclusion. For example, the constant

mult/s : mult (succ M) N P'
    <- mult M N P
    <- add N P P'.

has mode +M +N -P because the input M and N in the conclusion determine the inputs of the premise, and the P output by the premise determines the first input to the second premise (add), and the output of that determines the conclusion. On the other hand, a constant

mult/bad-mode-output : mult zero N P.

is not well-moded---the output P is not determined by the inputs. Similarly,

mult/bad-mode-input : mult (succ M) N zero
            <- mult M Q P.

is not well-moded---the second input to the premise is not determined by the inputs of the conclusion.

Note that subgoal order matters:

mult/s : mult (succ M) N Q
    <- add P N Q
    <- mult M N P.

The premises are mode-checked in order; the outputs from one subgoal are consider ground in subsequent premises.

Worlds

STELF checks that each constant inhabiting the type family obeys the worlds declaration. Because we are only proving theorems about closed terms right now, we will not run across any problems with world checks.

Termination

STELF checks that each constant inhabiting the type family obeys the induction order specified in the %total declaration. In each inductive premise of a constant, the specified induction position must be a strict subterm of the corresponding argument in the conclusion. For example, the constant

mult/s : mult (s M) N Q
    <- mult M N P
    <- add P N Q.

obeys the induction order M specified in the above totality assertion because the term M is a strict subterm of the term (s M).

Recuring on exactly the same term is obviously a termination error:

mult/bad-termination-1 : mult M N P
        <- mult M N P.
%total M (mult M _ _).

As is recuring on an entirely unrelated argumenet:

mult/bad-termination-2 : mult M N P
        <- mult N N P.
%total M (mult M _ _).

For example STELF would not accept the totality of mult if N were used as the induction order—the same term N in the conclusion of this constant appears in the premise:

%total N (mult _ N _).

%In addition to the subterm ordering on a single argument, STELF supports mutual induction and TODO.

Output coverage

In the definition of a type family, you may pattern-match the outputs of a premise. For example, we might write

mult/bad-output-cov : mult (succ M) N zero
           <- mult M N (succ P).
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).

Here we have insisted that the output of the premise has the form succ P for some P. STELF correctly reports an output coverage error because this condition can fail.

Pattern-matching the output of a premise is like an TODO step in a proof: you’re insisting that the premise derivation must conclude a particular fact that is more specific than the judgement form itself. For STELF to accept a relation as total, STELF must notice that all of these inversions are permissible. STELF permits such inversions when it is readily apparent that they are justified, and those inversions that STELF does not accept can be proved explicitly.

In this example, we got an output coverage error because we constrained the output of the premise by insisting it be formed by a particular constant. The other way to get output coverage errors is to insist that the output of a premise be a variable that occurs elsewhere in the type. For example:

mult/bad-output-free : mult (succ M) N zero
      <- mult M N N.
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).

Here, we insisted that the output of the premise be the number N that we put in. STELF is very conservative in checking output freeness: a type family will not be judged total if you constrain the outputs of any premise at all in this manner.

Input coverage

Mode, worlds, termination, and output coverage ensure that each constant really does cover the part of the relation indicated by its conclusion. For example, if mult passes these four checks, we know that mult/z and mult/s cover (zero, N, _) and (succ M, N, _), respectively. What else is necessary to know that mult defines a total relation? We need to know that all the constants inhabiting mult, taken together, cover all of the inputs. Input coverage checks exactly this.

For example, if we forgot mult/z, input coverage for mult would fail. For example:

mult' : nat -> nat -> nat -> type.
%mode mult' +N1 +N2 -X3.

mult'/s : mult' (succ M) N Q
    <- mult' M N P
    <- add P N Q.

%worlds () (mult' _ _ _).
%total M (mult' M _ _).

Here’s an analogy that might be helpful: You can think of each constant of a type as being a clause in an ML pattern matching declaration. Then input coverage is like the exhaustiveness checker for pattern matching.

STELF checks input coverage by TODO the input types to case-analyze the various constants that could have been used to inhabit them. For add, STELF splits the first nat argument M, and then checks that the cases plus z N N and add (succ M) N P are covered. Fortunately, these are exactly the cases we wrote down. If we had case-analyzed further in the definition of the judgement (e.g., if the definition of plus case-analyzed the second argument as well), STELF would continue splitting the input space. Because STELF separates termination checking and coverage checking, the constants defining a type family do not need to follow any particular primitive recursion schema-the constants may pattern-match the inputs in a general manner.

When STELF checks what

To a first approximation, you can think of the %mode and %worlds declarations as specifying a totality assertion and the %total declaration as checking it. This isn’t exactly how STELF works, though:

• When a %mode declaration is entered, STELF checks that all previous constants inhabiting the specified type family are well-moded; further, it then mode-checks any subsequent constants inhabiting that family.
• When a %worlds declaration is entered, STELF world-checks the type family; further, it then reports an error if any new constants contributing to the family at all are added.
• When a %total declaration is entered, STELF checks termination, then input coverage, then output coverage. When checking output coverage, STELF checks for unjustified constant pattern-matching in a first pass and then output freeness problems in a second pass.

This separation allows you to, for example, check that each constant in a family is well-moded (i.e., takes specified inputs to specified outputs) without checking that the entire type family is total. You can also use the declarations %terminates and %covers to check termination and input coverage independently.

If any constant in a type family fails mode, worlds, or output coverage, then mode, worlds, or totality checking fails for the whole type family. One could imagine that STELF instead would just disregard the offending constant: it is possible that the type family as a whole satisfies a totality assertion without that constant, and, in a mathematical sense, adding additional constants never invalidates the fact a totality assertion is true of a family. The reason STELF does not work this way is that %total actually has a more specific meaning, as we discuss in the next section.