Worlds in Twelf

Posted on March 7, 2015

Tags: twelf, types

In this post I wanted to focus on one particular thing in Twelf: %worlds declarations. They seems to be the most mysterious. I’ve had a couple people tell me that they just blindly stick %worlds () (x _ _ _) before every total and pray which is a little concerning..

In this post hopefully we’ll remove some of the “compile-n-pray” from using Twelf code.

What is %worlds

In Twelf we’re interested in proving theorems. These theorems are basically proven by some chunk of code that looks like this.

    my-cool-tyfam : with -> some -> cool -> args -> type.
    %mode my-cool-tyfam +A +B +C -D.

    some         : ... -> my-cool-tyfam A B C D.
    constructors : ... -> my-cool-tyfam A B C D.

    %worlds (...) (my-cool-tyfam _ _ _ _).
    %total (T) (my-cool-tyfam T _ _ _).

What’s interesting here is the 3 directives we needed

%mode to specify which arguments of the type family are universally quantified and which are existentially qualified in our theorem. This specifies the “direction” of the type family, + arguments are inputs and - arguments are outputs.
%total which actually goes and proves the theorem by induction on the canonical forms of the term in the parens.
%worlds which specifies the set of contexts to check the totality in. Note that a world is simply a set of contexts.

The one we’re interested in talking about here is %worlds. Everything we want to call %total has to have on of these and as mentioned above it specifies the contexts to check the theorem in. Remember that total is proven by induction over the canonical forms. One of the canonical forms for every type is off the form

For some x : ty ∈ Γ, then x is a canonical form of ty.

This is a little different than in other languages. We could usually just invert upon something in the context. That’s not the case in Twelf, we have to handle variables parametrically (this is critical to admitting HOAS and similar). This means that means we have to extremely careful about what’s in Γ lest we accidentally introduce something canonical form of ty without any additional information about it. The worlds specification tells us about the forms Γ can take. Twelf allows us to specify sets of contexts that are “regular”.

So for example remember how plus might be defined.

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

    plus/z : plus z N N.
    plus/s : plus N M P -> plus (s N) M (s P).

This is total in the empty context. If we added some b : nat to our context then we have no way of showing it is either a s or a z! This means that there’s a missing case for variables of type nat in our code. In order to exclude this impossible case we just assert that we only care about plus’s totality in the empty context. This is what the %worlds specification for plus stipulates

    %worlds () (plus _ _ _).

should be read as “plus should only be considered in the empty context” so the only canonical forms of plus are those specified as constants in our signature. This sort of specification is what we want for most vanilla uses of Twelf.

For most cases we want to be proving theorems in the empty context because we do nothing to extend the context in our constructors. That’s not to say that we can’t specify some nonempty world. We can specify a world where there is a b : nat, but if such a b must appear we have a derivation {a} plus b a z. This way when Twelf goes to check the canonical forms case for something in our context, b : nat, it knows that there’s a derivation that precisely matches what we need. I’ll circle back to this in a second, but first we have to talk about how to specify fancier worlds.

%block and Fancier Worlds

In Twelf there’s some special syntax for specifying worlds. Basically we can specify a template for some part of the world, called a block. A world declaration is just a conglomeration of blocks and Twelf will interpret this as a world of contexts in which each block may appear zero or more times.

In Twelf code we specify a block with the following syntax

    %block block_name : block {a : ty} ... {b : ty'}.

This specifies that if there is an a : ty in the context, it’s going to be accompanied by a bunch of other stuff including a b : ty'. Some blocks are pretty trivial. For example, if we wanted to allow plus to be defined in a context with some a : nat in the context we might say

    %block random_nat : block {b : nat}.
    %worlds (random_nat) (plus _ _ _).

This doesn’t work though. If we ask Twelf to check totality it’ll get angry and say

Coverage error --- missing cases:
{#random_nat:{b:nat}} {X1:nat} {X2:nat} |- plus #random_nat_b X1 X2.

In human,

You awful person Danny! You’re missing the case where you have to random integers and the random natural number b from the random_nat block and we want to compute plus b X X'.

Now there are a few things to do here. The saner person would probably just say “Oh, I clearly don’t want to try to prove this theorem in a nonempty context”. Or we can wildly add things to our context in order to patch this hole. In this case, we need some proof that about adding b to other stuff. Let’s supplement our block

    %block random_nat : block {b : nat}{_:{a} plus b a z}

Such a context is pretty idiotic though since there isn’t a natural number that can satisfy it. It is however enough to sate the totality checker.

    %total (T) (plus T _ _).

For a non contrived for example let’s discuss where interesting worlds come into play: with higher order abstract syntax. When we use HOAS we end up embedding the LF function space in our terms. This is important because it means as we go to prove theorems about it we end up recursing on a term under an honest to goodness LF lambda. This means we extend the context at some points in our proof and we can’t just prove theorems in the empty context!

To see this in action here’s an embedding of the untyped lambda calculus in LF

    term : type.
    lam  : (term -> term) -> term.
    app  : term -> term -> term.

Now let’s say we want to determine how many binders are in a lambda term. We start by defining our relation

    nbinds : term -> nat -> type.
    %mode nbinds +T -N.

We set this type family up so that it has one input (the term) and one output (a nat representing the number of binders). We have two cases to deal with here

    nbinds/lam : nbinds (lam F) (s N)
                  <- ({x : term} nbinds (F x) N).
    nbinds/app : nbinds (app F A) O
                  <- nbinds F N1
                  <- nbinds A N2
                  <- plus N1 N2 O.

In the lam case we recurse under the binder. This is the interesting thing here, we stick the recurse call under a pi binder. This gives us access to some term x which we apply the LF function two. This code in effect says "If for all terms F has N binders then lam F has N + 1 binders. The app case just sums the two binders.

We can try to world check this in only the empty context but this fails with

Error:
While checking constant nbinds/lam:
World violation for family nbinds: {x:term} </: 1

This says that even though we promised never to extend the LF context we did just that! To fix this we must have a fancier world. We create a block which just talks about adding a term to the context.

    %block nbinds_block : block {x : term}.
    %worlds (nbinds_block) (nbinds _ _).

This world checks but there’s another issue lurking about. Let’s try to ask Twelf to prove totality.

    %total (T) (nbinds T _).

This spits out the error message

Coverage error --- missing cases:
{#nbinds_block:{x:term}} {X1:nat} |- nbinds #nbinds_block_x X1.

This is the same error as before! Now that we’ve extended our context with a term we need to somehow be able to tell Twelf the height of that term. This smacks of the slightly fishy type of nbinds/lam: it’s meaning is that F x has the height N for any term x. This seems a little odd, why doesn’t the height of a functions body depend on its argument? We really ought to be specifying that whatever this x is, we know its height is z. This makes our new code

    nbinds/lam : nbinds (lam F) (s N)
                 <- ({x : term}{_ : nbinds x z} nbinds (F x) N).

Now we specify that the height of x is zero. This means we have to change our block to

    %block nbinds_block : block {x : term}{_ : nbinds x z}.

With this modification else everything goes through unmodified. For fun, we can ask Twelf to actually compute some toy examples.

    %solve deriv : nbinds (lam ([x] (lam [y] x))) N.

This gives back that deriv : nbinds (lam ([x] lam ([y] x))) (s (s z)) as we’d hope. It’s always fun to run our proofs.

Conclusion

Hopefully that clears up some of the mystery of worlds in Twelf. Happily this doesn’t come up for a lot of simple uses of Twelf. As far as I know the entire constructive logic course at CMU sidesteps the issue with a quick “Stick %worlds () (...) before each totality check”.

It is completely invaluable if you’re doing anything under binders which turns out to be necessary for most interesting proofs about languages with binders. If nothing else, the more you know..

Those who enjoyed this post might profit from Dan Licata and Bob Harper’s paper on mechanizing metatheory.

Cheers,