Coverage checking can verify that no cases in the definition of a type family have omitted. In combination with mode and termination checking, it is a powerful tool for analysing signatures. Its primary use in Twelf is for verifying totality of higher-level judgments, which can thereby be seen to represent proofs of meta-theorems.
There are several features of LF and its use as a logical framework which make coverage checking a complex problem.
The first is that higher-order representations often require us to
consider classes of contexts. For example, in the program for type
inference (see section 5.6 Sample Program) we introduce parameters x:exp
together with a typing assumption u:of x T for some T.
This means the type exp of expressions is dynamically extended
with new parameters, and coverage must take these into account.
The second are indexed types. While it easy to see if all cases for a simple data type such as the natural numbers (either zero or successor) are covered, it is more difficult to verify whether all cases for indexed types, such as possible deductions of A implies A, are covered.
The third is the higher-order nature of encodings. We may have to verify that all functions of a given type have been covered, not just values of atomic type. The fact that functions in LF must be parametric makes this possible, but it can be subtle.
Coverage addresses all three of these problems in different ways. The programmer can specify the kinds of parameters and hypotheses considered valid for an encoding. World checking verifies that this specification is respected. The programmer can also specify which arguments of a given type family should cover all possibilities exhaustively. Coverage checking verifies that this is indeed the case, or produces a list of missing cases. Coverage checking is always relative to a world declaration. Finally, totality checking verifies both coverage and termination, thereby ensuring that any mode-correct invocation of the type family considered as a logic program will succeed. Hence, a total type family represents a total, possibly non-deterministic, function and can thus be often seen to realize a meta-theoretic proof.
The adequacy of an encoding using higher-order abstract syntax usually relies on a characterization of the possible parameters and hypotheses that may be introduced. They often occur in blocks of assumptions that have to be made together in order for a representation to be correct. We refer to the total collection of assumptions as regular worlds consisting of blocks.
In Twelf, we first declare names for such blocks with %block,
then we check if a given type family respects this block structure
with %worlds.
decs ::= % Empty parameter declaration
| {id:term} decs % x:A for parameter x
| {id} decs % x:A with type A omitted
bdecl ::= some decs block decs % Blocks with indeterminate variables
| block decs % Closed blocks
worlds ::= % Empty world
| id % Block label b
| id | worlds % Block label b and alternatives
wdecl ::= (worlds) callpats. % Worlds declaration
decl ::= ...
| %block id : bdecl. % Block declaration with label b
| %worlds wdecl. % Regular world declaration
The syntactic category of call patterns (callpats) was in introduced in section 8.1 Termination Declaration.
Consider the typing judgment from section 5.6 Sample Program which can also be found in file `examples/guide/lam.elf'. We show only the last three declarations here.
of : exp -> tp -> type.
tp_lam : of (lam E) (arrow T1 T2)
<- ({x:exp} of x T1 -> of (E x) T2).
tp_app : of (app E1 E2) T1
<- of E1 (arrow T2 T1)
<- of E2 T2.
Note that every time the clause tp_lam is invoked, it introduces
a new parameter x:exp and also a new assumption of x T
for some T. In order for type inference to work correctly, it
is important that those two hypotheses always occur together. So, in
general, the context consisting of all hypotheses should have the form
x1:exp, u1:of x1 T1, ..., xn:exp, un:of xn Tn. We call this
a regular context. It consists of blocks of the
form x:exp, u:of x T for some T.
We declare this block, labeled tp_var, and then verify
that any hypotheses introduced by the type family of
will have this form.
%block tp_var : some {T:tp} block {x:exp} {u:of x T}.
%worlds (tp_var) (of E T).
Our encoding of natural deduction (see see section 3.6 Sample Signature and file
`examples/guide/nd.elf') shows that regular worlds also arise when
a signature does not have an immediate operational interpretation.
In this case, we may generate either a new parameter x:i
(in foralli and existse) or a new assumption
u:nd A for some proposition A (in impi,
ore, and existse). This can be verified with
%block nd_hyp : some {A:o} block {u:nd A}.
%block nd_parm : block {x:i}.
%worlds (nd_hyp | nd_parm) (nd A).
There are several subtleties in world checking.
... <- ({x:exp} of x T -> {y:exp} of y S -> ...)
instead of
... <- ({x:exp} {y:exp} of x T -> of y S -> ...).
As a special case of regular world declaration, the form
%worlds () callpats.
declares that the type families in callpats do not introduce any new parameters or hypotheses.
Once a set of regular worlds has been declared for a type family, Twelf can determine if all the possible cases for a given collection of input arguments are covered.
decl ::= ...
| %covers mdecl. %coverage declaration
This form reuses the mode declaration mdecl introduced in section 7 Modes which comes in a short form (see section 7.1 Short Mode Declaration) and long form (see section 7.2 Full Mode Declaration). The coverage checker selects the arguments declared as input (+) and verifies that the given family provides a clause for any combination of ground input arguments. The term input coverage emphasizes that we only verify the status of input arguments to a family, but not indefinite or output arguments.
For example, in order to check that there is a typing rule for every expression in the type inference code for Mini-ML (see section 5.6 Sample Program), we first declare the regular world and then check input coverage.
%block tp_var : some {T:tp} block {x:exp} {u:of x T}.
%worlds (tp_var) (of E T).
%covers of +E *T.
Coverage checking takes dependent types and subordination into account, but it is a decidable, syntactic test rather than a semantic criterion. This means that it can list the missing cases when it fails. For example, if we comment out the typing rule for application, we obtain the following error message:
Coverage error --- missing cases:
{E1:exp} {E2:exp} {T1:tp} |- of (app E1 E2) T1.
The format of the missing cases is G |- A, where A is a
form of goal for which does not unify with the head of any clause and
G is a context declaring the types for the free (existential)
variables in A.
A more subtle error occurs, if we forget the typing assumption for a new variable.
...
tp_lam : of (lam E) (arrow T1 T2)
<- ({x:exp} of (E x) T2).
%block tp_var : some {T:tp} block {x:exp}. % {u:of x T}.
%worlds (tp_var) (of E T).
%covers of +E *T.
Clearly, coverage has to fail since there is no typing assumption for bound variables. In this case we get the error message
Coverage error --- missing cases:
{T1:tp} {#tp_var:{x:exp}} {T2:tp} |- of #tp_var_x T2.
Here we see the notation for parameters in context blocks. The goal
of #tp_var_x T2 refers to a parameter called x in the
context block tp_var. The hypotheses available with this block
are listed in the declaration {#tp_var:{x:exp}}. This block
contains no typing assumption for x and coverage is violated.
Note that this notation can never be an input to Twelf; it is only
used for error messages.
One of the most difficult errors to analyse occurs when coverage is violated due to argument transposition and dependencies. In that situation the error is often reflected in implicit arguments which may not be easy to discern. An example of this form is given below in the next section.
The most advanced application of coverage checking is verifying the totality of a given type family. This is usually used to ascertain that a given higher-level type family implements a meta-theoretic proof. Checking that a type family is total requires, in this order, mode checking, world checking, termination checking, and coverage checking. Mode and world declarations have to be made separately, while termination and coverage checking are folded into a single declaration.
decl ::= ...
| %total tdecl. %totality declaration
Here tdecl is a termination declaration introduced in section 8.1 Termination Declaration. A totality declaration is processed in the following steps.
*) are not allowed.
As an example, we use type preservation, a continuation of the sample programs for type inference and evaluation in Mini-ML (see see section 5.6 Sample Program and file `examples/guide/lam.elf'). This can be proven automatically (see see section 10.2 Sample Theorems), but we can also give the proof by hand and have Twelf verify it via totality checking.
First, the correct program and verification. The type preservation
theorem states that for any closed evaluation D:eval E V and
typing derivation P:of E T there exists a typing derivation
Q:of V T.
tps : eval E V -> of E T -> of V T -> type.
tps_lam : tps (ev_lam) (tp_lam P) (tp_lam P).
tps_app : tps (ev_app D3 D2 D1) (tp_app P2 P1) Q
<- tps D1 P1 (tp_lam Q1')
<- tps D2 P2 Q2
<- tps D3 (Q1' V2 Q2) Q.
%mode tps +D +P -Q.
%worlds () (tps D P _).
%total D (tps D P _).
The mode declaration specifies that the evaluation and typing derivation
for E are input, while the typing derivation for V is
output. The worlds declaration expresses that expressions and types
must be closed, that is, not depend on any parameters. The final
totality declaration claims that the logic programming execution of
tps D P Q for ground D and P and free existential
variable Q terminates because tps is inductively defined
based on the structure of D. Note that this implies that the
meta-theorem of type preservation holds, because the type family
cps realizes the proof: it can always compute a typing derivation
Q:of V T when given arbitrary evaluation D:eval E V and
typing derivation P:of E T.
The signature above passes all three tests. The main subtlety in this example lies in the output coverage of the first subgoal
<- tps D1 P1 (tp_lam Q1')
How does Twelf know that any typing derivation Q1 returned by a
call tps D1 P1 Q1 must in fact have the form tp_lam Q1'
for some Q1'? Here, this follows by the structure of the
indexed types: Q1 : of (lam [x] E1' x) (arrow T2 T1) for some
E1', T1, and T2. Hence there remains only one
applicable top-level constructor for Q1, namely tp_lam,
which corresponds to the typing rule lambda-abstraction. In informal
proofs, we refer to this as inversion or genericity.
For the sake of illustration, we introduce two bugs into our proof
and analyse the error message. In the first, we reverse the arguments
D2 and D3 in rule tps_app.
tps_app : tps (ev_app D2 D3 D1) (tp_app P2 P1) Q
<- tps D1 P1 (tp_lam Q1')
<- tps D2 P2 Q2
<- tps D3 (Q1' V2 Q2) Q.
The resulting clause still passes all test up to input coverage, which fails with the message
Coverage error --- missing cases:
{E1:exp} {E2:exp} {E3:exp} {T1:tp} {E4:exp -> exp} {E5:exp}
{D1:eval (E4 E5) E3} {D2:eval E2 E5}
{D3:eval E1 (lam ([e:exp] E4 e))} {T2:tp} {P1:of E2 T2}
{P2:of E1 (arrow T2 T1)} {P3:of E3 T1}
|- tps (ev_app D1 D2 D3) (tp_app P1 P2) P3.
This clearly identifies the missing case, but it does not help much in
identifying which the rule tps_app fails to cover the given case.
If look back at the declaration for tps_app after reconstruction
tps_app :
{E1:exp -> exp} {V2:exp} {T1:tp} {D3:eval (E1 V2) V2} {T2:tp}
{Q1':{e:exp} of e T2 -> of (E1 e) T1} {Q2:of V2 T2} {Q:of V2 T1}
{D2:eval (E1 V2) V2} {P2:of (E1 V2) T2} {E2:exp}
{D1:eval E2 (lam ([e:exp] E1 e))} {P1:of E2 (arrow T2 T1)}
tps D3 (Q1' V2 Q2) Q -> tps D2 P2 Q2 -> tps D1 P1 (tp_lam Q1')
-> tps (ev_app D2 D3 D1) (tp_app P2 P1) Q.
we see that {D3:eval (E1 V2) V2} which is clearly non-sensical
and points to an argument ordering problem (V and V2
have been identified).
As the second example of an intentional problem, we use an apparently
correct implementation of a copy family implements the identity
relation on expressions recursively (see file
`example/guide/lam.elf').
cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
<- cp E1 F1
<- cp E2 F2.
cp_lam : cp (lam [x] E x) (lam [x] F x)
<- ({x:exp} {y:exp} cp x y -> cp (E x) (F y)).
%mode cp +E -F.
%block cp_var : block {x:exp} {y:exp} {u:cp x y}.
%worlds (cp_var) (cp E _).
%total E (cp E _).
This fails with the message
Coverage error --- missing cases:
{#cp_var:{x:exp} {y:exp} {u:cp x y}} {E1:exp} |- cp #cp_var_y E1.
because the parameter y:exp is not accompanied by an assumption
on how to copy y. Twelf does not perform the global analysis
that would be necessary to show that y actually can never occur
as a first argument to cp. If we introduce such an assumption,
for example, cp y y,
cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
<- cp E1 F1
<- cp E2 F2.
cp_lam : cp (lam [x] E x) (lam [x] F x)
<- ({x:exp} {y:exp} cp x y -> cp y y -> cp (E x) (F y)).
%mode cp +E -F.
%block cp_var : block {x:exp} {y:exp} {u:cp x y} {w:cp y y}.
%worlds (cp_var) (cp E _).
%total E (cp E _).
then totality checking still fails. The error message
Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp -> exp} {E2:exp -> exp -> exp}
|- {x:exp} {y:exp} cp x y -> cp y y -> cp (E1 x) (E2 x y).
shows that Twelf expected the output argument of the recursive call to
possibly depend on both x and y, while the corresponding
pattern F y allowed dependency only on y. Again, Twelf
does not perform the global analysis necessary to show that x can
never appear in the output argument of cp.
A correct and checkable implementation of cp introduces only one new
parameter, thereby avoiding the problems above.
cp : exp -> exp -> type.
cp_app : cp (app E1 E2) (app F1 F2)
<- cp E1 F1
<- cp E2 F2.
cp_lam : cp (lam [x] E x) (lam [x] F x)
<- ({x:exp} cp x x -> cp (E x) (F x)).
%mode cp +E -F.
%block cp_var : block {x:exp} {u:cp x x}.
%worlds (cp_var) (cp E _).
%total E (cp E _).
An important component for termination checking and coverage
checking is subordination Virga 99, Ph.D. Thesis.
We say that type family b subordinates type family
a (written b |> a) if a term of typ
b ...
might occur as a subterm of a term of type a ....
From the point of view of the application in Twelf, it is
the contrapositive that is important: if b does not
subordinate a, then no subterm of type a ...
can occur in a subterm of type b .... The notion
of occurrence here refers to terms in canonical form.
As Twelf performs type reconstruction, it incrementally keeps track of the subordination relation. It can be viewed at any time with the
Twelf.Print.subord ();
command. For each type family it shows the families that it subordinates.
Subordination information is used in section 8 Termination and section 9 Coverage.
Sometimes it is necessary to ensure that a given type family is not extended with additional constructors that might invalidate meta-theorems or add new (unwanted) axioms to a theory represented in LF. In order to prohibit further extensions to some type families, issue
%freeze a1 ... an.
to prevent further declarations of type a1 through an or any other type family subordinated by one of the a's.
Go to the first, previous, next, last section, table of contents.