[POPLmark] Regarding closure conversion

Tue May 10 11:18:56 EDT 2005

I believe John Hannan has implemented closure conversion in Twelf and
proved some properties of it.  I don't have the source, but it is referenced
in

Type Systems for Closure Conversions, John Hannan.  Participants'
Proceedings of the Workshop on Types for Program Analysis, May, 1995.
<http://www.cse.psu.edu/~hannan/papers/tpa.ps.gz>

There is also some subsequent work on lambda-lifting, but I don't
know how much of this has been implemented.

  - Frank

> >   To be concrete here I what I'd
> >   like to see demonstrated:
> > 
> >   % Object language
> >   tm : type.
> >   unit : tm.
> >   pair : tm -> tm -> tm.
> >   fst : tm -> tm.
> >   snd : tm -> tm.
> >   abs : (tm -> tm) -> tm.
> >   app : tm -> tm -> tm.
> > 
> >   % Closure conversion
> >   cconvert : tm -> tm -> type.
> >   %mode cconvert +T1 -T2.
> > 
> >   %{ cconvert transforms terms in the object language to terms
> >      in the same language, but lexical scope is not used,
> >      instead free variables have been packaged up with each function
> >      as tuple (closure).  That is
> > 
> > 	abs ([x] (abs ([y] (app x y))))
> > 
> > 
> >      would become
> > 
> > 	pair (abs ([x] pair (abs [y]
> >                                (app (fst (fst (snd y)))
> >                                     (pair (fst y) (snd (fst (snd y))))))
> >                             (pair (fst x) unit))
> >              (unit)
> > 
> >      [ The above was closure converted by hand, so it is entirely possible
> >        I made a subtle error. ]
> > 
> >   }%
> > 
> 
> 
> Hi Geoff,
> 
> I'm glad that you raised this question.  Closure conversion is my
> current favorite example of something that (I think) can be implemented
> more easily using nominal logic/alpha Prolog than using any other
> techniques of which I am aware.  
> 
> Before various people get on my case, I am happy to concede that at
> present, alpha Prolog does not constitute a logical framework, just a
> logic programming language (and a very immature one at that), so one
> cannot prove any but the simplest kinds of theorems with it.  Whether it
> is possible to develop a logical framework that combines the advantages
> of nominal logic (first-class treatment of names, induction principles
> expressible within the logic, theoretical simplicity) and those of LF-
> like logical frameworks (propositions/judgments as types,
> proofs/derivations as terms, slick handling of many kinds of
> contexts/judgments, dependent types) is still to be seen.
> 
> In any case, here is the encoding of closure conversion in alpha Prolog.
> 
> I assume the syntax is as follows:
> 
> G ::= * | x,G 
> t ::= x | \x.t | t u | fst t | snd t | (t,u) | ()
> 
> The following type declarations in alpha Prolog implement this syntax:
> 
> id : name_type.
> type ctx = [id].
> exp : type.
> var : id -> exp.
> app : (exp,exp) -> exp.
> abs : id\exp -> exp.
> fst : exp -> exp.
> snd : exp -> exp.
> pair : (exp,exp) -> exp.
> unit : exp.
> let : (exp,id\exp) -> exp.  (* let x = e1 in e2 --> let(e1,x\e2) *)
> 
> Except for the var and let cases these are essentially as you proposed
> for Twelf.
> I write env for a term of the form () | (v,env).
> I will take the following as an informal definition of closure
> conversion:
> 
> CC[[x,G |- x]]env   = fst(env)
> CC[[y,G |- y]]env   = snd(env)  (* x != y *)
> CC[[G |- t u]]env   = let c = CC[[G |- t]]env in 
>                       (fst c)(CC[G|-u]env, snd(c))
> CC[[G |- \x.t]]env  = (\y.CC[[x,G |- t]](y,env))  (* x,y not in G *)
> CC[[G |- fst t]]env = fst(CC[[G|-t]]env)
> CC[[G |- snd t]]env = snd(CC[[G|-t]]env)
> CC[[G |- (t,u)]]env = (CC[[G|-t]]env,CC[[G|-u]]env)
> 
> The closure conversion translation is written in alpha Prolog as
> follows.  Note that alpha Prolog allows the use of a function-like
> notation but internally, this is just unwound to a (considerably less
> readable) relational definition.  This is just a notational convenience.
> 
> func cconv(ctx,tm,tm) = tm.
> cconv([X|G],var(X),E) = fst(E).
> cconv([X|G],var(Y),E) = cconv(G,var(Y),snd(E)) 
>         :- X # Y.  (* means X not equal to Y *)
> cconv(G,app(T1,T2),E) 
>         = let(cconv(G,T1,E),c\
>               app(fst(var(c)),
>                   pair(cconv(G,T2,E),snd(var(c))))).
> cconv(G,abs(x\T),E) 
>         = pair(abs(y\cconv([x|G],T,var(y))),E)
>         :- x#G,y#G. (* means x,y not free in G *)
> cconv(G,fst(T),E) = fst(cconv(G,T,E)).
> cconv(G,snd(T),E) = snd(cconv(G,T,E)).
> cconv(G,pair(T,U),E) = pair(cconv(G,T,E),cconv(G,U,E)).
> 
> 
> If you do:
> 
> ?- cconv ([],abs(x\abs(y\app(var(x),var(y)))),unit) = E.
> 
> you get
> 
> Yes.
> E = pair(abs(y46\pair(abs(y101\
>            let(fst(snd(var(y101))),c133\
>                app(fst(var(c133)),
>                    pair(fst(var(y101)),snd(var(c133)))))),
>          var(y46))),
>        unit)
> 
>  E.
> Moreover, this is the only answer that alpha Prolog produces.es.
> I believe that this is morally equivalent to what you wrote.  The only
> differences are the use of "let" and the fact that the inner lambda's
> environment is just var y46, not pair(fst var(y46),unit).  This may be a
> bug in my understanding of closure conversion or may just mean that you
> had something different in mind; if so, let me know and I'll see if I
> can implement it.
> 
> 
> Note that it is the second clause of cconv where something interesting
> (i.e., not obviously equivalent to something in Twelf) happens. The
> clause for abstraction could be written in Twelf as something like
> 
> cconv : tmlist -> tm -> tm -> tm.
> cconv G (abs([x] T x)) E (pair (abs([x] U x)) E)
>     <- {x:tm} cconv (cons x G) T (var(x)) (U x).
> 
> That is, the only real difference is that we are able to test explicitly
> whether two names are equal or not.  It is possible, however, that this
> is an artifact of the particular form of closure conversion I
> implemented, and I think other approaches might require grabbing hold of
> the context in a more explicit way.  However, there is nothing
> preventing you from doing this in alpha Prolog.
> 
> I'm aware (from conversations with Frank Pfenning) that there are ways
> to get the desired behavior in Twelf, for example using a linear counter
> to generate "fresh" integer tags for the variable names as they go into
> the explicit environment, and doing the inequality test on the tags. But
> it is not clear to me how this is better than the above, since then you
> need to reason explicitly about uniqueness/freshness/integers/sets of
> "free" tags in the same way you would have to in a non-HOAS setting, but
> without the kind of assistance that HOAS provides for ordinary binding
> situations.  In contrast, nominal logic/alpha Prolog provides a uniform
> framework for reasoning about freshness, fresh name generation and
> alpha-equivalence.
> 
> On the other hand, you can "fool" my implementation by giving it a
> context with repeated names, a term mentioning names not in the context,
> or a context and environment that don't match up.  In a full
> formalization that I wanted to prove something about, I would have to
> add some additional checks to rule out these cases.  In contrast, one of
> the great things about Twelf and other logical frameworks is that
> dependent types usually make explicit checking of this form unnecessary.
> I don't have a good answer for this yet, but have some ideas.
> 
> --James
> 
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark