[POPLmark] [Provers] Re: Adequacy for LF

[Robert Harper]

Karl intends to answer this more fully, but, briefly, the difficulty 
with formulating closure conversion in Twelf is not to do with HOAS, 
it's to do with having to get access to the context.  Yes, it is 
difficult to formalize closure conversion in Twelf, but the reason is 
not to do with HOAS.

Bob

On May 9, 2005, at 3:18 PM, Geoffrey A. Washburn wrote:

>
>> However, I would like to correct a misconception that is unfortunately
>> being reinforced by the POPLmark challenge statement: the discussion
>> of HOAS suggests that it is somehow difficult to calculate
>> intensionally with variables.  Actually, it's quite easy.  One good
>> example of the intensional treatment of variable occurrences is the
>> formal Elf development of the proofs in the report "On the occurrence
>> of continuation parameters in CPS programs", by Danvy and Pfenning.
>> The report is actually also a great illustration of how doing the
>> machine-checkable representation can lead to better paper proofs, too.
>> The formal proofs have been updated for Twelf, and are included in
>> the standard Twelf distribution, in the examples/cpsocc directory.
>>
>> Another good set of examples that comes with Twelf is the correctness
>> of compilation from  Mini-ML to various low-level abstract machines,
>> in the examples/compile directory.  These analyze HOAS variables
>> intensionally in order to convert the HOAS into de Bruijn form (which
>> the low-level machines use).
>
> 	In the current draft we said "However, our experience also
>   suggests that it is often difficult to use HOAS to represent manty
>   problems.  For example, there are many languages with constructs that
>   require lists of binders that do not have obvious encodings into 
> HOAS.
>   Another example is proving properties about closure conversion.
>   Representing the closure conversion algorithm requires an intensional
>   mechanism for calculating free variables of a term, something that 
> does
>   not seem to be possible with HOAS."
>
> 	The first comment "For example, there are many languages with
>   constructs that require lists of binders that do not have obvious
>   encodings into HOAS" I think is worth ignoring for the moment, as 
> Karl
>   has already started a thread about it.
>
> 	However, your above comments do not seem to address the closure
>   conversion example.  At least as I understand closure conversion, it
>   is a very different process than CPS conversion or conversion to
>   de Bruijn form.  Maybe what you meant is that there is something in 
> the
>   way these examples were implemented that show how one might implement
>   closure conversion cleanly, but in a brief inspection I did not take
>   away any techniques that I could apply.  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. ]
>
>   }%
>
>   Maybe this is an easy problem, I'd love to see how it should be done,
>   but as far as I can tell, there is no straightforward methodology for
>   how to take the definition of closure conversion I would write on 
> paper
>   convert it into a Twelf logic program.  In particular a standard 
> closure
>   conversion algorithm would do some rather tricky rebinding that does 
> not
>   seem possible with HOAS.
>
>   	Note, I am not precluding that cconvert could use a different
>   representation of terms internally.  I'm certain it could be done by
>   first converting to deBruijn or some first-order representation, but
>   that would seem to defeat the purpose of using HOAS in the first 
> place.
>
> 	We would appreciate any feedback you have on this particular
>   problem, as well as any other comments that would improve our
>   characterization of HOAS approaches.
>
>
> -- 
> -- Geoff Washburn | geoffw at cis.upenn.edu | 
> http://www.cis.upenn.edu/~geoffw/ --
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark