Twelf User’s Guide: 9 Coverage

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 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.

9.1 Regular Worlds

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 Termination Declaration.

Consider the typing judgment from 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 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).

%worlds () callpats.

declares that the type families in callpats do not introduce any new parameters or hypotheses.

9.2 Input Coverage

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 Modes which comes in a short form (see section Short Mode Declaration) and long form (see section 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 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.

9.3 Totality

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 Termination Declaration. A totality declaration is processed in the following steps.

As an example, we use type preservation, a continuation of the sample programs for type inference and evaluation in Mini-ML (see see section Sample Program and file ‘examples/guide/lam.elf’). This can be proven automatically (see see section 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 _).

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 _).

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 _).

9.4 Subordination

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 ();

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.

9.1 Regular Worlds		Characterizing parameters and hypotheses
9.2 Input Coverage		Checking if all cases have been covered
9.3 Totality		Verifying if a family is total in its input
9.4 Subordination		How constants depend on each other