[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

Hi Greg,

Good questions all.

> Just to clarify -- it's possible to code up deBruijn representations
> in LF/Twelf as well.  I think the real question is if you commit to
> using HOAS, where does it really bite?  Possible answers so far:
>
> * if your notion of substitution is non-standard
> * if you need to get your hands on the context
>

These are both true, particularly the former.  Substitution is so 
integral to LF that it wouldn't be good if substitution were 
non-standard.  (However, keep in mind that some things called 
substitution aren't really substitution, at least in so far as they 
would tickle this problem.)  I have an upcoming paper describing a trick 
that lets you get ahold of the context; I don't know if you would 
consider it nice, though.  Carsten's new meta-logic, Delphin, should 
provide a better solution to the problem.

> Perhaps there are others?
>
> I'm also curious about the evolutionary path.  It's clear that we're
> going to want to mod out by more than alpha-equivalence for many
> things, and I don't yet see how this will be handled nicely in
> *any* system.
>

I agree, this is a very important problem.  Roberto Virga's dissertation 
laid out a general framework for using LF modulo rewriting relations.  
But as things stand, not very many rewriting relations are 
well-understood, and none of it is supported by the proof checker.

> For instance, I still find modeling an abstract machine with a heap,
> which I want to consider as a partial map from (alpha-varying) labels
> to values (which may have free occurrences of those labels), to be
> very awkward to encode.  deBruijn representation blows here, because
> I don't want the order of the bindings to matter.  But I haven't
> found a nice way to do this in Twelf either...  [Karl, Bob,
> attack mode off.  I didn't say "It can't be done."  I very
> politely said that "I haven't found a nice way to do this."]
>

I don't have a good solution for this.  If you don't need labels to 
alpha-vary, then the problem isn't hard.  Naturally, I did a lot of that 
in TALT.  But if you really need them to alpha-vary, here's my bes 
idea:  The basic idea is that you introduce all the binders first, then 
lay out the heap, using a dependent type to make sure that the number of 
binders equals the number of entries in the heap.  The representation is 
adequate, and I have done some proofs based on it, but in the end I 
found it too annoying and re-did it without alpha-varying labels.

> I've been disappointed by the apparent lack of "polymorphism"
> in Twelf -- I seem to have to define various kinds of lists at
> every level.  For someone used to coding instead of proving,
> that's painful.  Is there a way around this?
>

All I can say is you get used to it.  I'm told that the upcoming module 
system will help with this, but I don't know much more about it.  
Perhaps if Frank or Kevin is lurking, they could add something?

> And finally, I find it somewhat annoying that when
> I write a simple, total function, I have to step out to the
> meta-level to establish that it is indeed a function.
> Maybe there's a good way around this too?
>

Penny Anderson and Frank Pfenning have an experimental system that's 
supposed to help with this.  I haven't gotten a chance to try it yet, 
though.

    -- Karl