[racket] Redex model of parallel one-step reduction

On Sun, Jun 20, 2010 at 7:10 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> I've tried a few times to model the parallel one-step relation on page 55 in
> the Redex book as a reduction-relation, but I just can't seem to make it
> work.  Has anyone else been able to do it?

I don't think that there is a good way to do this in redex. I guess
the simplest, clearest thing would be to use continuations (ala amb)
somehow.

I did the below and it seems to work (altho you may find bugs in it!),
but I will readily admit it is a hack (especially since it does not
generalize to nary functions....).

(I didn't include the usual iswim test suite, but if you want that,
let me know.)

Robby


#lang racket
(require redex)

(define-language iswim
  ((M N L K) X (λ X M) (M M) b (o2 M M) (o1 M))
  (o o1 o2)
  (o1 add1 sub1 iszero)
  (o2 + - * ↑)
  (b number)
  ((V U W) b X (λ X M))
  (E hole (V E) (E M) (o V ... E M ...))
  ((X Y Z) variable-not-otherwise-mentioned))

(define-metafunction iswim
  [(δ (iszero 0)) (λ x (λ y x))]
  [(δ (iszero b)) (λ x (λ y y))]
  [(δ (add1 b)) ,(add1 (term b))]
  [(δ (sub1 b)) ,(sub1 (term b))]
  [(δ (+ b_1 b_2)) ,(+ (term b_1) (term b_2))]
  [(δ (- b_1 b_2)) ,(- (term b_1) (term b_2))]
  [(δ (* b_1 b_2)) ,(* (term b_1) (term b_2))]
  [(δ (↑ b_1 b_2)) ,(expt (term b_1) (term b_2))])


(define-metafunction iswim

  ;; 1. X_1 bound, so don't continue in λ body
  [(subst (λ X_1 any_1) X_1 any_2)
   (λ X_1 any_1)]

  ;; 2. do capture avoiding substitution
  ;;    by generating a fresh name
  [(subst (λ X_1 any_1) X_2 any_2)
   (λ X_3
     (subst (subst-var any_1 X_1 X_3) X_2 any_2))
   (where X_3 ,(variable-not-in (term (X_2 any_1 any_2))
                                (term X_1)))]
  ;; 3. replace X_1 with any_1
  [(subst X_1 X_1 any_1) any_1]

  ;; the last two cases just recur on
  ;; the tree structure of the term
  [(subst (any_2 ...) X_1 any_1)
   ((subst any_2 X_1 any_1) ...)]
  [(subst any_2 X_1 any_1) any_2])

(define-metafunction iswim
  [(subst-var (any_1 ...) variable_1 variable_2)
   ((subst-var any_1 variable_1 variable_2) ...)]
  [(subst-var variable_1 variable_1 variable_2) variable_2]
  [(subst-var any_1 variable_1 variable_2) any_1])

(define red
  (reduction-relation
   iswim
   (--> M M)
   (--> (o b ...) (δ (o b ...)))
   (--> ((λ X M) U)
        (subst M_2 X U_2)
        (where (M_1 ... M_2 M_3 ...) ,(apply-reduction-relation red (term M)))
        (where (U_1 ... U_2 U_3 ...) ,(apply-reduction-relation red (term U))))
   (--> (M N)
        (M_2 N_2)
        (where (N_1 ... N_2 N_3 ...) ,(apply-reduction-relation red (term N)))
        (where (M_1 ... M_2 M_3 ...) ,(apply-reduction-relation red (term M))))
   (--> (λ X M)
        (λ X M_2)
        (where (M_1 ... M_2 M_3 ...) ,(apply-reduction-relation red (term M))))
   (--> (o1 M)
        (o1 M_2)
        (where (M_1 ... M_2 M_3 ...)
               ,(apply-reduction-relation red (term M))))
   (--> (o2 N M)
        (o2 N_2 M_2)
        (where (N_1 ... N_2 N_3 ...) ,(apply-reduction-relation red (term N)))
        (where (M_1 ... M_2 M_3 ...) ,(apply-reduction-relation red
(term M))))))

(test--> red
         (term (+ (+ 1 2) (+ 3 4)))
         (term (+ (+ 1 2) (+ 3 4)))
         (term (+ 3 (+ 3 4)))
         (term (+ (+ 1 2) 7))
         (term (+ 3 7)))
(test--> red
         (term (+ 1 2))
         (term (+ 1 2))
         (term 3))
(test--> red
         (term (λ x (+ x (+ 1 2))))
         (term (λ x (+ x (+ 1 2))))
         (term (λ x (+ x 3))))
(test--> red
         (term ((λ x (+ x (+ 2 3))) 1))
         (term ((λ x (+ x (+ 2 3))) 1))
         (term ((λ x (+ x 5)) 1))
         (term (+ 1 (+ 2 3)))
         (term (+ 1 5)))
(test--> red
         (term ((λ x (+ x (+ 3 4))) (+ 1 2)))
         (term ((λ x (+ x (+ 3 4))) (+ 1 2)))
         (term ((λ x (+ x 7)) (+ 1 2)))
         (term ((λ x (+ x (+ 3 4))) 3))
         (term ((λ x (+ x 7)) 3)))

(test-results)