[POPLmark] [Provers] Re: Adequacy for LF

[James Cheney]

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