[POPLmark] [Provers] Re: Adequacy for LF

[Karl Crary]

There's no problem at all computing the free variables of a term.  
Here's a particularly slick implementation, but there's many other ways 
to do it:

appearsfree : (term -> term) -> type.

appearsfree_var : appearsfree ([x] x).
appearsfree_app : appearsfree ([x] app (E1 x) (E2 x))
       <- appearsfree E1
       <- appearsfree E2.
appearsfree_lam : appearsfree ([x] lam ([y] E x y))
       <- ({y:term} appearsfree ([x] E x y)).

The judgement "appearsfree ([x] E x)" will be derivable iff x appears 
free in E.  (I typed this directly into this message, so it's possible 
I've made a typo.)

Closure conversion is a little more interesting.  I suspect it's 
possible, but a certain amount ingenuity would be required.  The problem 
is getting your hands on the context, which is not usually a 
manipulatible object in LF.  (That is, the LF context is never 
manipulatible and ordinarily one identifies the object language context 
with LF's.)  To resolve this, I suspect one would have to reify the context.


Let me make a more general comment.  Many of the criticisms levelled at 
LF here have been of the form "you can't do X in LF/HOAS," and so far, 
all of those have been wrong, or at least unsubstantiated.  So why don't 
we declare a moratorium on that sort of thing.  Instead we can say that 
some things require some ingenuity to represent in HOAS, a statement on 
which we should all be able to agree.

    -- Karl


Geoffrey A. Washburn wrote:

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