Proving metatheorems:Proving totality assertions about the natural numbers
Previous: Full LF |
Proving metatheorems with Twelf | Next: Proving metatheorems |
In this section, we will use Twelf to mechanize proofs of metatheorems, which are statements about an object language. First, we recap the signature we have defined to this point, using the conveniences afforded by Twelf:
nat : type. z : nat. s : nat -> nat. even : nat -> type. even-z : even z. even-s : even (s (s N)) <- even N. plus : nat -> nat -> nat -> type. plus-z : plus z N2 N2. plus-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.
Totality assertions
A type family such as plus defines a relation among its indices, where indices are related iff their instance of the family is inhabited by an LF term. For example, plus defines a relation between three terms of type nat. The terms (s (s z), s z, s (s (s z))) are related by this relation (because 2 + 1 = 3), but the terms (z, s z, s (s (s z))) are not.
Totality assertions are one class of statements about LF type families. A totality assertion for a type family is specified by designating some index positions as inputs and others positions as outputs. We call this specification the mode of the totality assertion. Given a mode specification, the totality assertion asserts that for all inputs, there exist outputs that stand in the relation. Using plus as an example, if we designate the first two positions as inputs and the third position as an output, this specifies the following totality assertion:
- For all N1:nat and N2:nat, there exist N3:nat and D:plus N1 N2 N3.
That is, the sum of any two natural numbers exists. Designating instead the first position as output and second and third positions as inputs defines the following totality assertion:
- For all N2:nat and N3:nat, there exist N1:nat and D:plus N1 N2 N3.
Of course, this totality assertion is false, as N3 - N2 might not be a natural number.
A totality assertion for an LF type family corresponds with the standard notion of totality for the relation defined by the family. Proving a relation total is different from showing that the relation defines a function, as the outputs of a total relation are not necessarily unique—the relation may relate particular inputs to more than one collection of outputs.
We may prove a totality assertion by induction on canonical forms. For example, we can prove the first above totality assertion by induction on N1:nat. The second totality assertion above is actually false—for example, there is no N1 such that plus N1 (s z) z is inhabited.
Totality assertions for LF type families are actually more general than we have discussed so far. The above examples consider only terms that are well-typed without mentioning LF variables. In general, it is useful to state totality assertions about all terms that are well-typed in any LF context in a particular world, which is a set of LF contexts. Thus, a totality assertion is specified by both a mode declaration and a world declaration. For the time being, we will consider totality assertions that are stated for the world containing only the empty LF context (i.e., totality assertions about closed terms), so we defer further discussion of worlds.
Totality assertions in Twelf
You can use Twelf to verify totality assertions about LF type families. For example, to verify the totality assertion
- For all N1:nat and N2:nat, there exist N3:nat and D:plus N1 N2 N3.
you enter the following Twelf declarations:
%% declare totality assertion %mode plus +N1 +N2 -N3. %worlds () (plus _ _ _). %% check totality assertion %total N1 (plus N1 _ _).
Let's break down what each of these declarations means:
- The %mode declaration specifies the mode of a type family—in this case, that N1 and N2 are universally quantified (+) and that N3 is existentially quantified (-). We will sometimes refer to the universally-quantified types as inputs and the existentially-quantified types as outputs.
- The %worlds declaration states the totality assertion for LF terms in the empty context, which adequately represent natural numbers and the addition judgement.
- The %total declaration asks Twelf to prove the totality assertion by induction on the canonical forms N1 of type nat. Note that it is the position of the variable named in the %total that determines the induction index.
In this case, Twelf succeeds in proving this assertion.
How Twelf checks assertions
Twelf proves a totality assertion for a type family such as plus by checking several properties. These properties, taken together, constitute a proof by induction on canonical forms that the type family defines a total relation.
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
plus-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.
has mode +N1 +N2 -N3 because the input N1 and N2 in the conclusion determine the inputs of the premise, and the N3 output by the premise determines the output of the conclusion. On the other hand, a constant
plus-bad-mode : plus N1 N2 N3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)plus-bad-mode : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3. Error: Occurrence of variable N3 in output (-) argument not necessarily ground
%% ABORT %%
is not well-moded—the output N3 is not determined by the inputs. Similarly,
plus-bad-mode2 : plus N1 N2 N3 <- plus N4 N2 N3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)plus-bad-mode2 : {N4:nat} {N2:nat} {N3:nat} {N1:nat} plus N4 N2 N3 -> plus N1 N2 N3. Error: Occurrence of variable N4 in input (+) argument not necessarily ground
%% ABORT %%
is not well-moded—the first input to the premise is not determined by the inputs of the conclusion.
Worlds
Twelf checks that each constant inhabiting the type family obeys the worlds declaration. Because we are only proving theorems about closed terms in this section, we will not run across any problems with world checks. Consequently, we defer discussion of world checking until later.
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
plus-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.
obeys the induction order N1 specified in the above totality assertion because the term N1 is a strict subterm of the term (s N1). On the other hand, Twelf would not accept the totality of plus if N2 were used as the induction order—the same term N2 in the conclusion of this constant appears in the premise:
%total N2 (plus _ N2 _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)Error: Termination violation: ---> (N2) < (N2)
%% ABORT %%
In addition to the subterm ordering on a single argument, Twelf supports mutual induction and lexicographic induction.
Output coverage
%mode plus +X1 +X2 -X3.
In the definition of a type family, you may pattern-match the outputs of a premise. For example, we might write
plus-bad-output : plus (s N1) N2 (s (s N3)) <- plus N1 N2 (s N3). %worlds () (plus _ _ _). %total N1 (plus N1 N2 N3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)plus-bad-output : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 (s N3) -> plus (s N1) N2 (s (s N3)). %worlds () (plus _ _ _). Error: Totality: Output of subgoal not covered Output coverage error --- missing cases: {X1:nat} {X2:nat} |- plus X1 X2 z.
%% ABORT %%
Here we have insisted that the output of the premise has the form s N3 for some N3. Twelf correctly reports an output coverage error because this condition can fail (for example, if the premise was plus-z : plus z z z).
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:
plus-bad-output-freeness : plus (s N1) N2 (s N2) <- plus N1 N2 N2. %worlds () (plus _ _ _). %total N1 (plus N1 N2 N3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)plus-bad-output-freeness : {N1:nat} {N2:nat} plus N1 N2 N2 -> plus (s N1) N2 (s N2). %worlds () (plus _ _ _). Error: Constant plus-bad-output-freeness Occurrence of variable N2 in output (-) argument not free
%% ABORT %%
Here, we insisted that the output of the premise be the number N2 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 plus passes these four checks, we know that plus-z and plus-s cover (z, N2, N2) and (s N1, N2, s N3), respectively. What else is necessary to know that plus defines a total relation? We need to know that all the constants inhabiting plus, taken together, cover all of the inputs. Input coverage checks exactly this.
For example, if we forgot plus-z, input coverage for plus would fail. For example:
plus' : nat -> nat -> nat -> type. %mode plus' +N1 +N2 -X3. plus-s' : plus' (s N1) N2 (s N3) <- plus' N1 N2 N3. %worlds () (plus' _ _ _). %total N1 (plus' N1 _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)plus' : nat -> nat -> nat -> type. %mode +{N1:nat} +{N2:nat} -{X3:nat} (plus' N1 N2 X3). plus-s' : {N1:nat} {N2:nat} {N3:nat} plus' N1 N2 N3 -> plus' (s N1) N2 (s N3). %worlds () (plus' _ _ _). Error: Coverage error --- missing cases: {X1:nat} {X2:nat} |- plus' z 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. The type family plus is exhaustive, but this plus' is not.
Twelf checks input coverage by splitting the input types to case-analyze the various constants that could have been used to inhabit them. For plus, Twelf splits the first nat argument N1, and then checks that the cases plus z N2 N2 and plus (s N1) N2 N3 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:
- 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.
- 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.
- 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.
Logic programming
An LF signature can be interpreted as a logic program, where the constants defining a type family are viewed as rules for searching for derivations of that type family. For example, we can use Twelf to add numbers as follows:
%solve D : plus (s z) (s z) N.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%solve plus (s z) (s z) N. OK D : plus (s z) (s z) (s (s z)) = plus-s plus-z.
%% OK %%
This %solve declaration asks Twelf to find an N and a derivation D that plus (s z) (s z) N. Of course, Twelf responds that 1 + 1 = 2.
This logic programming interpretation of an LF signature is very useful: you can directly run the judgements defining your programming language. However, because the focus of this introduction is proving metatheorems, an interested reader should refer to the tutorial on logic programming.
The reason for bringing up logic programming here is that, when Twelf proves a totality assertion via %total, it actually proves a stronger statement than the totality assertion itself: Twelf proves that the type family defines a total logic program. The above checks have an operational interpretation:
- Mode: when called on ground inputs (i.e., concrete terms without unification variables), the logic program returns ground outputs.
- Worlds: all premises of every constant are in a context in the world specified by the premise's world declaration.
- Termination: search for a derivation always terminates.
- Output coverage: the output of a recursive call never fails to unify.
- Input coverage: the logic program covers all possible inputs.
To start proving metatheorems, it is not necessary to have a thorough understanding of the logic programming interpretation of the LF signature. However, the logic programming view does explain some of the specifics of what Twelf will and will not deem total. For example, mode checking considers premises in the order that it does (rather than, say, the reverse order) because that is the order in which the logic programming engine searches for derivations.
Summary
In this section, we have seen how to ask Twelf to verify totality assertions for LF type families. To see why we have spent so much time on totality assertions, proceed to the next section.
Previous: Full LF |
Proving metatheorems with Twelf | Next: Proving metatheorems |