Parallel beta-reduction for the call-by-value lambda-calculus

parv.rkt

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

(define-language Λ
  [X variable]
  [V (λ X E)]
  [P E] ; side-condition: closed
  [E (λ X E) (E E) X]
  [F (% (λ X E) F) (λ X E) (F F)])

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

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

(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 (((λ X X) (λ Y Y))
                    ((λ P P) (λ Q Q)))))