On Sun, Jun 20, 2010 at 7:10 PM, David Van Horn <dvanh...@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)
_________________________________________________
For list-related administrative tasks:
http://lists.racket-lang.org/listinfo/users
