[plt-scheme] Expressing closures in PLT Redex

From: Arjun Guha (arjun at cs.brown.edu)
Date: Wed Jul 19 11:47:59 EDT 2006

Say I have a language where closures are expressed as
environment-abstraction pairs:

(define lang
    (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
     (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.



Posted on the users mailing list.