[POPLmark] [Provers] Re: Adequacy for LF

[James Cheney]

>   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. ]
> 
>   }%
> 


Hi Geoff,

I'm glad that you raised this question.  Closure conversion is my
current favorite example of something that (I think) can be implemented
more easily using nominal logic/alpha Prolog than using any other
techniques of which I am aware.  

Before various people get on my case, I am happy to concede that at
present, alpha Prolog does not constitute a logical framework, just a
logic programming language (and a very immature one at that), so one
cannot prove any but the simplest kinds of theorems with it.  Whether it
is possible to develop a logical framework that combines the advantages
of nominal logic (first-class treatment of names, induction principles
expressible within the logic, theoretical simplicity) and those of LF-
like logical frameworks (propositions/judgments as types,
proofs/derivations as terms, slick handling of many kinds of
contexts/judgments, dependent types) is still to be seen.

In any case, here is the encoding of closure conversion in alpha Prolog.

I assume the syntax is as follows:

G ::= * | x,G 
t ::= x | \x.t | t u | fst t | snd t | (t,u) | ()

The following type declarations in alpha Prolog implement this syntax:

id : name_type.
type ctx = [id].
exp : type.
var : id -> exp.
app : (exp,exp) -> exp.
abs : id\exp -> exp.
fst : exp -> exp.
snd : exp -> exp.
pair : (exp,exp) -> exp.
unit : exp.
let : (exp,id\exp) -> exp.  (* let x = e1 in e2 --> let(e1,x\e2) *)

Except for the var and let cases these are essentially as you proposed
for Twelf.
I write env for a term of the form () | (v,env).
I will take the following as an informal definition of closure
conversion:

CC[[x,G |- x]]env   = fst(env)
CC[[y,G |- y]]env   = snd(env)  (* x != y *)
CC[[G |- t u]]env   = let c = CC[[G |- t]]env in 
                      (fst c)(CC[G|-u]env, snd(c))
CC[[G |- \x.t]]env  = (\y.CC[[x,G |- t]](y,env))  (* x,y not in G *)
CC[[G |- fst t]]env = fst(CC[[G|-t]]env)
CC[[G |- snd t]]env = snd(CC[[G|-t]]env)
CC[[G |- (t,u)]]env = (CC[[G|-t]]env,CC[[G|-u]]env)

The closure conversion translation is written in alpha Prolog as
follows.  Note that alpha Prolog allows the use of a function-like
notation but internally, this is just unwound to a (considerably less
readable) relational definition.  This is just a notational convenience.

func cconv(ctx,tm,tm) = tm.
cconv([X|G],var(X),E) = fst(E).
cconv([X|G],var(Y),E) = cconv(G,var(Y),snd(E)) 
        :- X # Y.  (* means X not equal to Y *)
cconv(G,app(T1,T2),E) 
        = let(cconv(G,T1,E),c\
              app(fst(var(c)),
                  pair(cconv(G,T2,E),snd(var(c))))).
cconv(G,abs(x\T),E) 
        = pair(abs(y\cconv([x|G],T,var(y))),E)
        :- x#G,y#G. (* means x,y not free in G *)
cconv(G,fst(T),E) = fst(cconv(G,T,E)).
cconv(G,snd(T),E) = snd(cconv(G,T,E)).
cconv(G,pair(T,U),E) = pair(cconv(G,T,E),cconv(G,U,E)).


If you do:

?- cconv ([],abs(x\abs(y\app(var(x),var(y)))),unit) = E.

you get

Yes.
E = pair(abs(y46\pair(abs(y101\
           let(fst(snd(var(y101))),c133\
               app(fst(var(c133)),
                   pair(fst(var(y101)),snd(var(c133)))))),
         var(y46))),
       unit)

 E.
Moreover, this is the only answer that alpha Prolog produces.es.
I believe that this is morally equivalent to what you wrote.  The only
differences are the use of "let" and the fact that the inner lambda's
environment is just var y46, not pair(fst var(y46),unit).  This may be a
bug in my understanding of closure conversion or may just mean that you
had something different in mind; if so, let me know and I'll see if I
can implement it.


Note that it is the second clause of cconv where something interesting
(i.e., not obviously equivalent to something in Twelf) happens. The
clause for abstraction could be written in Twelf as something like

cconv : tmlist -> tm -> tm -> tm.
cconv G (abs([x] T x)) E (pair (abs([x] U x)) E)
    <- {x:tm} cconv (cons x G) T (var(x)) (U x).

That is, the only real difference is that we are able to test explicitly
whether two names are equal or not.  It is possible, however, that this
is an artifact of the particular form of closure conversion I
implemented, and I think other approaches might require grabbing hold of
the context in a more explicit way.  However, there is nothing
preventing you from doing this in alpha Prolog.

I'm aware (from conversations with Frank Pfenning) that there are ways
to get the desired behavior in Twelf, for example using a linear counter
to generate "fresh" integer tags for the variable names as they go into
the explicit environment, and doing the inequality test on the tags. But
it is not clear to me how this is better than the above, since then you
need to reason explicitly about uniqueness/freshness/integers/sets of
"free" tags in the same way you would have to in a non-HOAS setting, but
without the kind of assistance that HOAS provides for ordinary binding
situations.  In contrast, nominal logic/alpha Prolog provides a uniform
framework for reasoning about freshness, fresh name generation and
alpha-equivalence.

On the other hand, you can "fool" my implementation by giving it a
context with repeated names, a term mentioning names not in the context,
or a context and environment that don't match up.  In a full
formalization that I wanted to prove something about, I would have to
add some additional checks to rule out these cases.  In contrast, one of
the great things about Twelf and other logical frameworks is that
dependent types usually make explicit checking of this form unnecessary.
I don't have a good answer for this yet, but have some ideas.

--James