POPL Tutorial/Basic error messages

From The Twelf Project
Jump to: navigation, search

How Twelf checks assertions

Twelf 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:

nat : type.  
zero : nat.
succ : nat -> nat.

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

add/z : add zero N N.
add/s : add (succ M) N (succ P) 
	 <- add M N P.

%worlds () (add _ _ _).
%total M (add M _ _).
mult : nat -> nat -> nat -> type.
%mode mult +M +N -P.

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

Mode

Twelf 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.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-mode-output : {N:nat} {P:nat} mult zero N P. Error: Occurrence of variable P in output (-) argument not necessarily ground

%% ABORT %%

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.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-mode-input : {M:nat} {Q:nat} {P:nat} {N:nat} mult M Q P -> mult (succ M) N zero. Error: Occurrence of variable Q in input (+) argument not necessarily ground

%% ABORT %%

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.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/s : {M:nat} {N:nat} {P:nat} {Q:nat} mult M N P -> add P N Q -> mult (succ M) N Q. Error: Occurrence of variable P in input (+) argument not necessarily ground

%% ABORT %%

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

Worlds

Twelf 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

Twelf 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 _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-termination-1 : {M:nat} {N:nat} {P:nat} mult M N P -> mult M N P. Error: Termination violation: ---> (M) < (M)

%% ABORT %%

As is recuring on an entirely unrelated argumenet:

mult/bad-termination-2 : mult M N P
			  <- mult N N P.
%total M (mult M _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-termination-2 : {N:nat} {P:nat} {M:nat} mult N N P -> mult M N P. Error: Termination violation: ---> (N) < (M)

%% ABORT %%

For example Twelf 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 _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Termination violation: ---> (N) < (N)

%% ABORT %%

In addition to the subterm ordering on a single argument, Twelf supports mutual induction and lexicographic induction.

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).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-output-cov : {M:nat} {N:nat} {P:nat} mult M N (succ P) -> mult (succ M) N zero. %worlds () (mult _ _ _). Error: Totality: Output of subgoal not covered Output coverage error --- missing cases: {X1:nat} {X2:nat} |- mult X1 X2 zero.

%% ABORT %%

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

Pattern-matching the output of a premise is like an inversion 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 Twelf to accept a relation as total, Twelf must notice that all of these inversions are permissible. Twelf permits such inversions when it is readily apparent that they are justified, and those inversions that Twelf 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).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult/bad-output-free : {M:nat} {N:nat} mult M N N -> mult (succ M) N zero. %worlds () (mult _ _ _). Error: Constant mult/bad-output-free Occurrence of variable N in output (-) argument not free

%% ABORT %%

Here, we insisted that the output of the premise be the number N that we put in. Twelf 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 _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult' : nat -> nat -> nat -> type. %mode +{N1:nat} +{N2:nat} -{X3:nat} (mult' N1 N2 X3). mult'/s : {P:nat} {N:nat} {Q:nat} {M:nat} add P N Q -> mult' M N P -> mult' (succ M) N Q. %worlds () (mult' _ _ _). Error: Coverage error --- missing cases: {X1:nat} {X2:nat} |- mult' zero X1 X2.

%% ABORT %%

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.

Twelf checks input coverage by splitting the input types to case-analyze the various constants that could have been used to inhabit them. For add, Twelf 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), Twelf would continue splitting the input space. Because Twelf 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 Twelf 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 Twelf works, though:

  1. When a %mode declaration is entered, Twelf checks that all previous constants inhabiting the specified type family are well-moded; further, it then mode-checks any subsequent constants inhabiting that family.
  2. When a %worlds declaration is entered, Twelf world-checks the type family; further, it then reports an error if any new constants contributing to the family at all are added.
  3. When a %total declaration is entered, Twelf checks termination, then input coverage, then output coverage. When checking output coverage, Twelf 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 Twelf 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 Twelf does not work this way is that %total actually has a more specific meaning, as we discuss in the next section.