Parallel beta-reduction for the lambda-calculus

par.rkt

#lang racket
(require redex/reduction-semantics)
;; http://lists.racket-lang.org/users/archive/2012-July/053007.html

(define-language Λ
  [X variable]
  [E (λ X E) (E E) X]
  [F (% (λ X F) F) (λ X F) (F F) X])

;; Mark all redexes
(define-metafunction Λ
  mark : E -> F
  [(mark X) X]
  [(mark ((λ X E_0) E_1))
   (% (λ X (mark E_0)) (mark E_1))]
  [(mark (E_1 E_2))
   ((mark E_1) (mark E_2))]
  [(mark (λ X E))
   (λ X (mark E))])

;; Reduce all marked redexes
(define-metafunction Λ
  rinse&repeat : F -> E
  [(rinse&repeat E) E]
  [(rinse&repeat X) X]
  [(rinse&repeat (% (λ X F_0) F_1))
   (rinse&repeat (subst X F_1 F_0))]
  [(rinse&repeat (F_1 F_2))
   ((rinse&repeat F_1)
    (rinse&repeat F_2))]
  [(rinse&repeat (λ X F))
   (λ X (rinse&repeat F))])

(define step
  (reduction-relation 
   Λ #:domain E
   (--> E (rinse&repeat (mark E)))))

(define-metafunction Λ
  subst : X any any -> any 
  ;; 1. x_1 bound, so don't continue in λ body 
  [(subst X_1 any_1 (λ X_1 any_2))
   (λ X_1 any_2)] 
  ;; 2. general purpose capture avoiding case 
  [(subst X_1 any_1 (λ X_2 any_2))
   (λ X_new (subst X_1 any_1 (subst-var X_2 X_new any_2))) 
   (where X_new ,(variable-not-in (term (X_1 any_1 any_2)) 
                                  (term X_2)))] 
  ;; 3. replace x_1 with e_1 
  [(subst X_1 any_1 X_1) any_1]
  ;; 4. x_1 and x_2 are different, so don't replace 
  [(subst X_1 any_1 X_2) X_2] 
  ;; the last cases cover all other expressions 
  [(subst X_1 any_1 (any_2 ...)) ((subst X_1 any_1 any_2) ...)]
  [(subst X_1 any_1 any_2) any_2])

(define-metafunction Λ
  subst-var : X any any -> any 
  [(subst-var X_1 any_1 X_1) any_1]
  [(subst-var X_1 any_1 (any_2 ...))
   ((subst-var X_1 any_1 any_2) ...)] 
  [(subst-var X_1 any_1 any_2) any_2])


(require redex)
(traces step (term (((λ S (λ Z (S (S (S Z)))))
                     (λ X X))
                    (λ Y Y))))