[plt-scheme] Expressing closures in PLT Redex

Is this a question about plt redex, or a question about what  
reduction system you want to write?

If the latter, why not just reduce to to the body of the lambda with  
the new environment installed? (note that you'll have to do more than  
just that. You might want to check out MF & MRF's monograph; I think  
you want the CEK machine or one possibly the one just before it).

If the former, I'm not getting the question.

Robby

On Jul 19, 2006, at 10:47 AM, Arjun Guha wrote:

> Say I have a language where closures are expressed as
> environment-abstraction pairs:
>
> (define lang
>    (language
>     (e-cxt hole (e-cxt E) (V e-cxt))
>
>     (env ((var V) ...))
>
>     (P (env E))
>
>     (E V var (E E) #| and so on |#)
>
>     (V ; values are numbers and closures
>      number
>      (lambda env (var) E))
>
>
> So, for example, I might have a closure:
>
> (lambda ((a 3) (b 4)) (x) (+ x a))
>
> that adds 3 to its argument, and this closure happens to have  
> captured b
> as well.
>
> Given that my programs, P are environment-expression pairs, what is  
> the
> best way to write the "AppLam" rule (in PLT Redex), that evaluates the
> body of the closure in the closure's environment (appropriately
> extended), and then resumes executing the context in its environment?
>
> (reduction/name "AppLam" lang
>     (env_1 (in-hole e-cxt_1 ((lambda env_2 (x) E_1) V_1)))
>     << what goes here >>)
>
> In << what goes here >>, I could have something along the lines of:
>
> (in-hole e-cxt_1 (reduce (extended-env_2 E_1)))
>
> However, that strikes me as a bit arbitrary.
>
> Thanks.
>
> Arjun
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>