[POPLmark] [Provers] Re: Adequacy for LF

[Geoffrey A. Washburn]

> 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/ --