[POPLmark] [Provers] Re: Adequacy for LF

[James Cheney]

On Tue, 2005-05-10 at 10:41 -0400, Karl Crary wrote: 
> James,
> 
> Here's how I would do what you ask in LF.  (Written by hand; hasn't 
> faced the typechecker.)
> 
> First, arrange the invariant that for every variable in the context, we 
> have a meta-assumption for fvs that returns the singleton set.  That is, 
> use the block:
> 
> %block varblock : block {v:var} {f:fvs (var v) (vcons v vnil)}.
> 
> Then:
> 
> fvs_app : fvs (app E1 E2) L
>        <- fvs E1 L1
>        <- fvs E2 L2
>        <- append L1 L2 L.
> fvs_lam : fvs (lam E) L
>        <- ({v:var}
>           fvs (var v) vnil
>           -> fvs (E v) L).
> 
> That being said, it's probably not such a good idea to distinguish 
> between variables and terms syntactically; I think it would generally be 
> better to distinguish them by an assumption.  That's more the general 
> practice.  The above solution would work in that setting as well.

OK, I think I see how this would work, but how can one ensure that
"enough" assumptions of the form 

f:fvs (var v) (vcons v vnil)

are in the context (without looking at the term yourself and adding
them)?  Doesn't that require figuring out what the free variables of the
term are (so we're back where we started)?  Would we have to make sure
that we add f:fvs (var v) (vcons v vnil) to the context whenever we
proceed inside a binder elsewhere in the program that might call fvs?
Or is this what your last comment about distinguishing variables and
terms by an assumption would address?

--James

PS.  I found the "How to believe a Twelf proof" draft very enlightening.