[POPLmark] Lists of binders in HOAS

[Robert Harper]

The problem here is first of all to give a clean formulation of mutual 
recursion, even on paper.  My own practice is to recognize that 
"packets" of mutually recursive functions are best represented as 
objects --- a single "self" with one component (method) for each 
mutually recursive function.  This, then, formalizes in Twelf very 
cleanly.

Bob

On May 9, 2005, at 2:06 PM, David Walker wrote:

> Hi,
>
> I started lurking here after being told there was considerable 
> excitement on
> the poplmark list....
>
> Karl, I would love to see your solution for a collection of mutually
> recursive multi-argument functions.  ie, encode the syntax, typing 
> relation
> and operational semantics of something like:
>
>
> tp ::= unit | (tp,...,tp) -> tp
>
> f ::= fun x (x:tp,...,x:tp):tp = e   (* recursive function *)
>
> fs ::= f | f and fs                      (* mutually recursive *)
>
> e ::= x | () | let fs in e | e e
>
> I suppose you must already have something like this for your 
> formalization
> of the definition of standard ML.  If you could show me this little 
> piece,
> I'd be very interested.  The obvious difficulty here is that the 
> scopes of
> the function variables do not follow the syntactic structure of the
> pseudo-BNF definition given above.  Therefore, to do a HOAS 
> formalization,
> it seems you have to lift introduction of the function variables above 
> the
> group of mutually recursive function definitions.  In addition, you 
> may need
> some trick to use the framework's definition of substitution to 
> implement
> the substitutions necessary for implementing the operational semantics 
> of
> function application.
>
> I hope your encoding is just as elegant as the HOAS encodings of
> non-recursive functions.  Is the proof of adequacy also equally simple?
> That would be great!
>
> Thanks,
> Dave
>
>> -----Original Message-----
>> From: poplmark-bounces at lists.seas.upenn.edu [mailto:poplmark-
>> bounces at lists.seas.upenn.edu] On Behalf Of Karl Crary
>> Sent: Monday, May 09, 2005 1:01 PM
>> To: poplmark at lists.seas.upenn.edu
>> Subject: [POPLmark] Lists of binders in HOAS
>>
>> My attention has been drawn to the following statement on page 6 of 
>> the
>> Poplmark challenge: "However, our experience also suggests that it is
>> often difficult to use HOAS to represent many problems.  For example,
>> there are many languages with constructs that require lists of binders
>> that do not have any obvious encoding into HOAS."
>>
>> Of course, I can't refute this conclusively without knowing what you
>> have in mind, but lists of binders are no problem at all in HOAS.  For
>> example, to define a multi-argument lambda:
>>
>> term : type.
>> bterm : type.  %% bound term
>>
>> lam : bterm -> term.
>>
>> bterm_none : term -> bterm.
>> bterm_another : (term -> bterm) -> bterm.
>>
>> Then you encode \x,y.e as:
>>
>>     lam (bterm_another ([x] bterm_another ([y] bterm_none (E x y)))).
>>
>> As far as I know, this technique is quite robust.  So I'm curious, 
>> what
>> did the challenge authors have in mind?
>>
>>     -- Karl
>>
>> _______________________________________________
>> Poplmark mailing list
>> Poplmark at lists.seas.upenn.edu
>> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark