closure-calculus.ss
;; Reduction semantics for a Calculus of Closures

;; Copyright (c) 2006 David Van Horn
;; Licensed under the Academic Free License version 3.0

;; <dvanhorn@cs.brandeis.edu>

(module closure-calculus mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2 2)))
  (provide (all-defined))
  
  (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)))))

  ) ; end of closure-calculus module