I have been working on logic programming using nominal logic, a logic that incorporates some interesting features for reasoning about names, binding, and freshness. I have developed a prototype implementation of such a language called alpha Prolog. There is a lot of overlap (in terms of functionality) between higher-order and nominal logic programming, and figuring out just what the difference is has been of interest to me for a while (that is, for which, if any, problems does one approach offer a nicer way of doing things than the other?). Closure conversion has been my best example of something that one can "just implement" in alpha Prolog but apparently not in higher-order logic programming or LF. Until recently I haven't been able to figure out how to do closure conversion in LF.
As a result of discussions on the POPLMark mailing list (starting with Geoff Washburn's question about whether closure conversion is definable in LF), I realized one way to handle the variable-inequality testing that is needed in closure conversion. One can combine a "fvs" function with local hypotheses to add "enough" judgments about inequality to the context whenever you pass inside a binder. Perhaps this is a standard trick, but this is very interesting to me because it suggests a way to encode nominal logic in LF, which is something I've been chewing on for a while. (This may be of interest only to me.)
Based on this idea, I have attempted an encoding of Hannan's first closure conversion judgment (figure 1 of the paper) in LF. I also implemented it in alpha Prolog.
There is another minor subtlety in that we need to enforce that rules (1.5), (1.6), and (1.8) apply only when x is a variable (otherwise nondeterminism appears possible). To do this, I introduced an auxiliary judgment cconv_var that is used for local hypotheses cconv_var x y added in rules (1.2) and (1.4) and used in rules (1.5), (1.6), and (1.8).
%solve d2 : cconv (lam[x](lam [z] x)) (X).
I fixed this by implementing an explicit list-remove predicate remove_tlist. Fortuitously, inequality was not needed since we are only removing a locally bound variable.
%solve d4 : cconv (lam[x] (lam[z] (app x (lam[w] (app x x))))) X.
cconv.apl (183 LOC, 61 for substitution) is a version implemented in alpha Prolog. I can't help but point out that this is just the kind of situation in which nominal logic's treatment of names (in particular, the ability to talk about freshness/name inequality and names that escape what would be their scope in a HOAS representation) seems to be more expressive. However, I'm not making any formal claims about it. It just seems to me to be a reasonable way of interpreting Hannan's rules (replacing uses of higher-order features with nominal/first order features as necessary). And it appears to work properly on the trivial examples above.
In addition, I included definitions of capture-avoiding substitution which I think cover all the cases that would be needed in Hannan's operational semantics. As you'd expect, it is not pretty; however, I claim that the definition of capture-avoiding substitution in alpha Prolog/nominal logic/FreshML is regular enough that these clauses could be generated automatically using generic programming techniques. (In fact, alpha Prolog has a "hack" for doing just this, but it's not integrated with unification yet.)
To be fair, there are probably queries for which Twelf's higher-order unification implementation will find an answer whereas alpha Prolog will loop. However, when run in the (intended) forward direction, I believe that the two implementations provide essentially the same behavior.
Caveat: Both cconv3.elf and cconv.apl appear to not quite have the right behavior on
%solve d5 : cconv (lam[x] (lam[z] (lam[w] x)))) X.
(or the alpha Prolog equivalent): the result contains a reference to the outer argument within the inner lambdas' environments. This seems unlike what is wanted for closure conversion, but appears to be allowed by Hannan's rules. Possibly there is something subtle going on that I'm missing, but I think that additional converting is needed when we cross a scope boundary, and Hannan's rules do not appear to do this.
I think that cconv3.elf provides an answer to Geoff's original question: Yes, it is possible to encode closure conversion in LF. However, is this encoding elegant? Or, is a more elegant encoding possible? I think these are the real questions, and I don't know the answers. Comparing the amount and complexity of code in the cconv3.elf with that in cconv.apl, one finds that the LF version takes 187 lines of code whereas the alpha Prolog version takes 182 lines of code (of which roughly one third are "boilerplate" capture-avoiding substitution clauses). This is not a scientific comparison. I think that further simplification to the alpha Prolog version is possible, but have not done so in order to keep the correspondence between Hannan's rules, the LF version and the alpha Prolog version as clear as possible.
I haven't tried to verify that the LF version has the correctness properties asserted of it by Hannan, or to prove some kind of adequacy property. Similarly, no formal or informal correctness of the alpha Prolog version is being asserted.
Suggestions on how to improve these programs are welcome.