[POPLmark] Regarding closure conversion

[James Cheney]

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