[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

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.

    -- Karl


James Cheney wrote:

>On Mon, 2005-05-09 at 16:35 -0400, Karl Crary wrote:
>  
>
>>There's no problem at all computing the free variables of a term.  
>>Here's a particularly slick implementation, but there's many other ways 
>>to do it:
>>
>>appearsfree : (term -> term) -> type.
>>
>>appearsfree_var : appearsfree ([x] x).
>>appearsfree_app : appearsfree ([x] app (E1 x) (E2 x))
>>       <- appearsfree E1
>>       <- appearsfree E2.
>>appearsfree_lam : appearsfree ([x] lam ([y] E x y))
>>       <- ({y:term} appearsfree ([x] E x y)).
>>
>>The judgement "appearsfree ([x] E x)" will be derivable iff x appears 
>>free in E.  (I typed this directly into this message, so it's possible 
>>I've made a typo.)
>>    
>>
>
>Hi Karl,
>
>In my opinion, the above program does not "calculate the free variables
>of a term".  It only tests whether a single variable is free in the
>given term (or, looking at things a different way, whether the function
>term provided is strict), rather than computing a list/set/other data
>structure containing all the free variables of the term.  This is the
>kind of calculation that would be necessary to build an explicit
>environment data structure during some kinds of closure conversion.  For
>example, a common optimization is to limit the environment constructed
>for a given lambda abstraction to only mention the variables that are
>actually used inside the lambda.  
>
>Can you show how one would write a predicate that relates a term and a
>list containing all variables that occur in it (and no other variables)?
>Is this even a meaningful question to ask of the kind of encoding being
>used above?
>
>Since variables are not a separate type from terms:
>
>term : type.
>app : term -> term -> term.
>lam : (term -> term) -> term.
>
>something like
>
>fvs : term -> termlist -> type.
>
>does not seem to say what we want.
>
>Instead, I have in mind something like
>
>term : type.
>var : type.
>var : var -> term.
>app : term -> term -> term.
>lam : (var -> term) -> term.
>
>vlist : type.
>vnil : vlist.
>vcons : var -> vlist -> vlist.
>
>fvs : term -> vlist -> type.
>
>that relates a term with a vlist that includes all vars appearing free
>in it.  (Repetitions are OK.)
>
>This is expressible in alpha Prolog as follows:
>
>term : type.
>v : type.
>var : v -> term.
>app : term -> term -> term.
>lam : v\term -> term.
>
>
>pred fvs(term,[v]).
>fvs(var(X),[X]).
>fvs(app(T,U),N) :- fvs(T,L), fvs(U,M), append(L,M,N).
>fvs(lam(x\T),M) :- fvs(T,M), remove(M,x,N).
>
>where remove is defined as
>
>pred remove([v],v,[v]).
>remove([],X,[]).
>remove(X::L,X,M) :- remove(L,X,M).
>remove(Y::L,X,Y::M) :- X # Y, remove(L,X,M).
>
>--James
>
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>