[POPLmark] Regarding closure conversion

[Karl Crary]

Hi James,

You can identify variables quite easily by adding a variable judgement 
and introducing a variable assumption whenever a variable enters scope.  
That much is standard.  The inequality condition is a bit harder, and 
although there are ways to do it, I don't know what Hannan has in mind.  
(Caveat: I first heard of the paper from Frank's post, and I have not 
read it yet.)

    -- Karl


James Cheney wrote:

>On Tue, 2005-05-10 at 10:18 -0400, Frank Pfenning wrote:
>  
>
>>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.
>>    
>>
>
>Hi Frank,
>
>I had a look.  Hannan's translation includes rules (1.6, 2.10, 3.6) like
>the following:
>
>L |> x |--> N,L'
>----------------------------- (x != z)
>(L,x,c) |> z ==> (N # c);L'
>
>Here L,L' are lists of target terms, x is a source term, c a target
>closure term, and z is a source term (x,c,z often variables), and N is
>an integer.  Closures are considered to be lists of terms, and N # c is
>field lookup.  In this setting, functions lambda x.t are translated to
>functions lambda x. lambda c. t', where c is the closure/environment
>argument.
>
>The intuitive reading of a rule like the above is "when translating a
>variable, if it is not the argument introduced by the current function,
>then look it up in the closure".
>
>However, I do not see how to translate such a rule directly into a Twelf
>rule in a natural way that captures the intended meaning.  In
>particular, the property "is a variable" and the inequality side
>condition seems to have no counterpart in Twelf (circa 1995).  Simply
>writing something like
>
>sterm : type.
>tterm : type.
>tclos : type.
>tlist : type.
>
>app : sterm -> sterm -> sterm.
>lam : (sterm -> sterm) -> sterm.
>
>tapp    : tterm -> tterm -> tterm.
>tlookup : nat -> tclos -> tterm.
>tclos   : tclos -> tterm.
>tapp    : tterm -> tterm -> tterm.
>clos    : (tterm -> tclos -> tterm) -> tlist -> tclos.
>tnil    : tlist.
>tcons   : tlist -> tterm -> tlist.
>
>cconv        : sterm -> tterm -> type.
>cconv_ctxt   : tlist -> sterm -> tclos -> sterm -> tterm -> tlist 
>                 -> type.
>cconv_lookup : tlist -> sterm -> nat -> tlist -> type.
>...
>
>{L,L':tlist}{X,Z:sterm}{C:tclos}{N:nat}
>cconv_ctxt L X C Z (lookup N C) L' 
>	   <- X neq Z,
>	   <- cconv_lookup L Z N L'.
>
>does not appear to be what is wanted for two reasons: 
>1.  Since no effort is made to restrict the above rule to apply when Z
>is a variable only, the above rule applies to translate *any* Z.  So, it
>overlaps with the other rules for cconv_ctxt.  I believe this is fixable
>using assumptions "this is a variable" and worlds, and maybe this is
>what Hannan's implementation did.  Presumably something like 
>
>{L,L':tlist}{X,Z:sterm}{C:tclos}{N:nat}
>cconv_ctxt L X C Z (lookup N C) L' 
>	   <- is_var X
>           <- is_var Z
>           <- X neq Z,
>	   <- cconv_lookup L Z N L'.
>
>where is_var is introduced whenever we pass inside a source lambda,
>would work.
>
>2.  I do not believe there is any way to give meaning to X neq Z that
>gives correct behavior (i.e., for which you could prove adequacy between
>Hannan's rules and an intuitively equivalent translation in terms of
>concrete syntax.)  Perhaps this is fixable by threading an integer
>counter through the computation that can be used to "tag" each variable
>so that we can tell later on whether two variable occurrences are
>distinct (i.e., were introduced by different binders).  This would still
>not be an immediate translation of Hannan's rules, whereas from reading
>the paper one gets the impression that the paper rules correspond
>directly to LF rules.
>
>Hannan presents only the higher-order encoded form of the translation,
>and does not consider adequacy.  He proves correctness properties of the
>form "if T steps to T' and T translates to U then for some U', U steps
>to U' and T' translates to U'" (soundness)  and "if T translates to U
>and U steps to U' then there exists T' such that T steps to T' and T'
>translates to U'" (completeness).  Such properties are certainly
>necessary for correctness, but it is not clear to me:
>
>1.  what constitutes a formalized proof here? Hannan claims that he has
>formalized proofs of these properties in Elf, but what constitutes a
>proof in Elf (circa 1995) for this formalization?  I think the answer
>must be that a proof is a collection of relation instances relating the
>input and output derivations, with totality checked by inspection or
>schema checking.  But not enough explanation is present for me to be
>sure.
>
>2.  what effort has been made to check that the translation encoding is
>sensible? that is, adequate, or at least total, deterministic (in an
>appropriate mode)?  In particular, I have no trouble believing that the
>correctness theorems above are true (in both informal and Elf forms) and
>that the latter is provable in (tw)Elf, but I don't believe that a proof
>of the latter implies the truth of the former, because I think there are
>derivable things in the formalized translation that (I think) are not in
>the informal translation.  If the formalization used is provably
>adequate, then I suspect that it is quite different from the clean
>version presented in the paper.
>
>I have written to Hannan about these questions.  Maybe it is just that
>there is something more subtle going on that I am missing.
>
>The lambda lifting paper ("Specification and Correctness of Lambda
>Lifting", Fischbach and Hannan, Workshop on Semantics, Applications and
>Implementation of Program Generation, 2000) does not employ higher-order
>abstract syntax or an LF encoding.  Maybe there is other work on this I
>am not aware of.
>
>--James
>
>PS.  All of the papers mentioned can be found on Hannan's web page
>http://www.cse.psu.edu/~hannan/papers.html
>
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>