[plt-scheme] Re: Expressing closures in PLT Redex

Arjun Guha wrote:
> Say I have a language where closures are expressed as
> environment-abstraction pairs:

Hello Arjun,

This doesn't address your question directly, but may shed some light on 
the issues.

Below is a PLT Redex formulation of the applicative order reduction 
strategy for the "lambda rho hat" calculus, an extension of Curien's 
calculus of closures, lambda rho, that allows for one-step reduction to 
be expressed.

The reference for this work is Section 2.2 and 2.4 of A Concrete 
Framework for Environment Machines, Magorzata Biernacka and Olivier Danvy.

    http://www.brics.dk/RS/06/3/

(Note that this uses de Bruijn indices-- variables are represented by 
natural numbers and a substitution (an environment) is a list of values. 
  A variable's number gives the index into the list for value to which 
it is bound.  Environment extension is just cons.)

This is my first PLT Redex program, so caveat emptor, etc.

David

(define lang
   (language

    ;; Evaluation contexts
    (e hole
       (e c)
       (v e))

    ;; Substitutions
    (s (v ...))

    ;; Terms
    (t number
       (t t)
       (lambda t))

    ;; Closures
    (c (t s)
       (c c))

    ;; Values
    (v ((lambda t) s))))

(define reductions
   (list
    (reduction/context/name
     "Beta" lang e
     (((lambda t_0) s_0) v_0)
     (term (t_0 (v_0 . s_0))))

    (reduction/context/name
     "App" lang e
     ((t_0 t_1) s_0)
     (term ((t_0 s_0) (t_1 s_0))))

    (reduction/context/name
     "Var" lang e
     (number_0 s_0)
     (term-let ((c_0 (list-ref (term s_0) (term number_0))))
               (term c_0)))))