# Effectiveness lemma

We use the term **effectiveness lemma** for a lemma that explicitly proves a totality assertion for an LF type family using another LF type family.

There are two reasons to prove an effectiveness lemma:

- A type family may satisfy a totality assertion but not be written in such a way that Twelf can verify its totality automatically with a %total declaration. For example, justifying the induction might require an explicit termination metric, or knowing that the type family covers all possible inputs might require some sophisticated reasoning (such as reasoning from false).
- As an artifact of the way totality checking works, it is sometimes necessary to prove an effectiveness lemma even when Twelf has already verified the corresponding %total declaration.

We discuss these motivations in more detail after presenting an example effectiveness lemma.

## Example effectiveness lemma

Consider the relation that negates a bit:

bit : type. bit/0 : bit. bit/1 : bit. bit-flip : bit -> bit -> type. bit-flip/01 : bit-flip bit/0 bit/1. bit-flip/10 : bit-flip bit/1 bit/0.

We can ask Twelf to prove the following totality assertion:

- For all
`B : bit`, there exists a`B' : bit`and`D : bit-flip B B'`.

as follows:

%mode bit-flip +B -B'. %worlds () (bit-flip _ _). %total {} (bit-flip _ _).See Twelf's output

However, we can also prove the totality relation explicitly as an effectiveness lemma `can-bit-flip`:

can-bit-flip : {B:bit} bit-flip B B' -> type. %mode can-bit-flip +D1 -D2. - : can-bit-flip bit/0 bit-flip/01. - : can-bit-flip bit/1 bit-flip/10. %worlds () (can-bit-flip _ _). %total {} (can-bit-flip _ _).See Twelf's output

When processing the `%total`, Twelf verifies the following totality assertion:

- For all
`B : bit`, there exists a`B' : bit`and`D : bit-flip B B'`and a`D' : can-bit-flip B D`.

## Motivating scenario

This particular example is clearly not motivated by the first consideration mentioned above, as Twelf was able to prove the totality assertion directly. For such an example, see the tutorial on explicit termination metrics.

However, this effectiveness lemma is motivated by the second consideration, as the following example demonstrates. Consider a programming language that includes primitive bits and a negation operation on them:

tp : type. tp/bit : tp. tm : type. bt : bit -> tm. neg : tm -> tm. of : tm -> tp -> type. of-bt : of (bt _) tp/bit. of-neg : of (neg E) tp/bit <- of E tp/bit. eval : tm -> tm -> type. eval-bt : eval (bt B) (bt B). eval-neg : eval (neg E) (bt B') <- eval E (bt B) <- bit-flip B B'.

We elide the parts of the language that are not relevant to this example.

For simplicity, assume the language is manifestly terminating, so the progress theorem can be proved by a simple inductive argument that shows that all terms evaluate to a value:

progress : of E T -> eval E V -> type. %mode progress +D1 -D2. %worlds () (progress _ _).

Now, consider the case of progress for `of-neg`:

- : {Dflip : bit-flip B B'} progress (of-neg (Dof : of E tp/bit)) (eval-neg Dflip DevalE) <- progress Dof (DevalE : eval E (bt B)).

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)- : {B:bit} {B':bit} {E:tm} {Dof:of E tp/bit} {DevalE:eval E (bt B)} {Dflip:bit-flip B B'} progress Dof DevalE -> progress (of-neg Dof) (eval-neg Dflip DevalE). Error: Occurrence of variable B' in output (-) argument not necessarily ground

%% ABORT %%

By induction, we come up with a derivation `DevalE`, which, by the value inversion lemma, must result in a value of the form `(bt B)`. To finish the case, we need a derivation `Dflip : bit-flip B X1` for some `B':bit`.

You might think that this case should be accepted as is. After all, the totality assertion proved by the above `%total` shows that such a `Dflip` must exist.

Unfortunately, the current Twelf implementation rejects this case as ill-moded. In logic programming terms, variables bound in braces like `{Dflip}` are treated as unification variables, so they must be filled in by unification if they are not already part of an input term. On the other hand, subgoals, which are the premises that are searched for using logic programming, must be written with an `->`. This means that there is no way to **name** the derivation resulting from the appeal to the totality assertion for `plus`. In metatheorem terms, this means that we cannot appeal to the totality assertion for a type family to come up with a derivation of the type family itself, only the output indices of the family.

The work-around is to prove the effectiveness lemma. Using the above effectiveness lemma, we can finish this case as follows:

- : progress (of-neg (Dof : of E tp/bit)) (eval-neg Dflip DevalE) <- progress Dof (DevalE : eval E (bt B)) <- can-bit-flip B Dflip.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)- : {X1:bit} {B:bit} {Dflip:bit-flip B X1} {E:tm} {Dof:of E tp/bit} {DevalE:eval E (bt B)} can-bit-flip B Dflip -> progress Dof DevalE -> progress (of-neg Dof) (eval-neg Dflip DevalE).

%% OK %%

Because the derivation of ` bit-flip B B'` is an index to `can-flip-bit`, the case is mode-correct.

This limitation of Twelf could conceivably be addressed in a future release. For now, it is straightforward to work around it using effectiveness lemmas to prove totality assertions explicitly.

Read more Twelf tutorials and other Twelf documentation.