[POPLmark] Experience report with Twelf

[Dan Licata]

> A side note: I don't think that this is exactly the law of the
> excluded middle. I think it says something like "at least one of the
> 'subtyping' and 'notsubtyping' judgments are derivable." 

The law of the excluded middle is usually phrased as (A or not(A)),
which corresponds in this instance to the phrase in quotes above.

> For true classical reasoning, I found that I also needed the related
> lemma, that asserts that "at most one of the judgements is derivable".
> 
> subtyping-exclusive: subtyping A B -> not-subtyping A B -> false ->  
> type.

subtyping-exclusive is a different lemma, which asserts that (for this
particular A) (A and not(A) implies false).  This statement is true
for all A in intuitionistic logic, where not(A) is usually taken as
sugar for (A implies false).  So, if not-subtyping is really
not(subtyping), then this lemma should be provable easily using the
standard proof (apply the second premise to the first).

I don't know FJ, so I don't know what you're trying to encode.  If
not-subtyping is really not(subtyping), then you could encode it with
with the single rule

not-subtyping-contra : not-subtyping A B
		       <- (subtyping A B -> false)

and the metatheorem in this instance is easy to prove.  If your object
language definition of not-subtyping isn't really not(subtyping), then
you'd have to prove this metatheorem on paper as well.  Otherwise,
what tells you that the two are actually exclusive?  If you made a
mistake in one of the definitions they wouldn't be.
 
> Things like this get me too. As I understand it, a Twelf proof of the
> decidability of subtyping is not an LF element of type ({a : tp} {b:
> tp} sub-or-not a b) it is some meta reasoning that the Twelf logic
> program is a total function.

Right, a Twelf meta-proof isn't just a single LF term.  The
metatheorem apparatus lets you state Pi_2 sentences as type families
with modes.  The type family

A : B -> C -> D -> type.
%mode A +B +C -D.

represents the sentence "for all b:B, for all c:C, there exists a d:D"

A total relation from the universally quantified things to the
existentially quantified things is a proof of a Pi_2 sentence (for all
inputs, it constructs the witnesses to the existentials).  So, the
meta-theorem language needs to give us a way to write down a relation
and check that it is total.

The traditional way of thinking about Twelf is that the relation is
given by a logic program from the universally-quantified things to the
existentially-quantified things.  That is, you inhabit the type family
representing the metatheorem with cases that, in Elf, constitute a
logic program.  Then the meta-theorem checker proves that the cases
you've written down actually implement a total program.

To some degree, you can also understand what you're doing without
mentioning logic programming at all (though this is of course just
another way of looking at the same thing).  I sometimes find this
abstraction helpful.

You think of the type family  

A : B -> C -> D -> type.
%mode A +B +C -D.

as directly representing a relation where b,c,d are related iff 
(A b c d) is inhabited.  Then, your job in writing cases is to provide
enough constants in the signature such that for all canonical LF terms
of type B and all canonical LF terms of type C, there exists a
canonical LF term of type (A b c d) for some canonical d:D.  The
meta-theorem checker proves by induction over canonical forms that
this is actually the case.

In particular, let's verify something like

case1 : A (b-constructor Subderiv) DerivationOfC InductiveResult
         <- A Subderiv DerivationOfC InductiveResult

(note that this case is a tail call, in the sense that we just return
the inductive result).  

If you look at the canonical forms judgements for LF, you'll see that
when the application of a constant ('b-constructor' in this case) to
something is canonical, the something must itself be canonical.  Since
the meta-theorem checker works by induction on canonical forms, it can
*assume* that for Subderiv and DerivationOfC there exists a canonical
LF term InductiveResult:D for which there exists a canonical LF term
of type (A Subderiv DerivationOfC InductiveResult).  Then applying the
constant case1 to this assumed term yields a canonical term of type 
A (b-constructor Subderiv) DerivationOfC InductiveResult.  
This means that this case can be used to produce inhabitants of some
of the (A b c d) space.

I find this way of thinking helpful for understanding why a "by
induction" in the paper proof turns into a "<-" in the type of a
constant in the Twelf proof.  The induction in the paper proof turns
into an induction over canonical forms in the meta-theorem checker
that proves that the premises of the case are actually inhabited (if
the premises aren't inhabited, the constant doesn't help show that the
type family is inhabited).
    
Disclaimer: I came up with this second way of thinking about what's
going on myself, but I haven't checked to see if it's in any of the
existing work (e.g., Carsten's thesis).  Also, I haven't really
thought it through, so it might not actually work.

> >Or, you could state progress with an extra premise of type ({a : tp}
> >{b : tp} sub-or-not a b), though I don't immediately see that it
> >would be easy to satisfy this premise once you've proven decidability
> >as a meta-theorem.
> >
> 
> I agree, I don't think you can manipulate proofs like that in Twelf.

You sometimes can.  In this particular example, say we prove

progress' : ({a : tp} {b : tp} sub-or-not a b)
	    -> <usual statement>
	    -> type.
%mode progress' +X1 ... .

and then prove 

decide-sub : {a : tp} {b : tp} sub-or-not a b -> type.
%mode decide-sub +X1 +X2 -X3.

Can we use this to prove 

progress : <usual statement> -> type.

in terms of progress'?  Maybe.  

We can write a case like

- : progress ...
    <- ({a : tp} {b : tp} decide-sub a b (D a b))
       %% D : {a : tp} {b : tp} (sub-or-not a b)
    <- progress' D ...

That is, we call decide-sub in an extended context, so that the result
it returns has the abstracted type.  

The catch is that decide-sub has to be true in the context dictated by
the hypothetical (the {a} {b} in the context for the call comes from
the premise to progress'!).  If it is, then you can do this.  If it's
not, you could reprove decide-sub in the context you need to call it
in.  However, this could be tricky.  In this example, if you didn't
already have variables of LF type tp in the worlds for decide-sub,
then to prove decide-sub in a context containing them, you'd have to
figure out how to decide subtyping for the variables.

> >Sometimes strengthening does come up.  More than once, though, I've
> >thought I needed strengthening when really I had corrupted my
> >subordination relation (i.e., Twelf thought types were subordinate
> >when they shouldn't have been).  The subordination relation tells you
> >when objects of one type can appear in another.  You can use the
> >command (in the Twelf server directly) Print.subord to print the
> >subordination relation and inspect it.  I'm not sure that it shows
> >the transitive closure, so you may have to compute that yourself.
> 
> Thanks for the hint about Print.subord.
> 
> lookupClass_strengthen :
>    ({x:exp} lookupClass CT C (class C D FS (MT x)))
>      -> lookupClass CT C (class C D FS (MT unit)) -> type.
> 
> However, I think this is a case where strengthening is unavoidable.
> The type exp is subordinate to the type methodTable, but since the
> methodTable MT comes from the classTable CT (which does not depend on
> x) in this case, it can't depend on x.

This could be a property of the system you're formalizing, not just
the LF encoding.  That is, on paper, how do you *know* that the class
you get back doesn't mention some variable in the context?  Sometimes
I've glossed over things like this on paper only to have Twelf point
them out to me.

> Thanks for writing a careful description of how to go about addressing
> coverage errors---this is something that should appear in the Twelf
> wiki.

Agreed--I'll make a post.

-Dan