1#lang racket 2 3;"one point basis" 4;"formal aspects of computing" 5 6(require redex) 7 8(initial-font-size 12) 9(reduction-steps-cutoff 100) 10(initial-char-width 80) 11 12(define-language lang 13 (e (e e) 14 comb 15 abs1 16 abs2 17 abs3) 18 (e-ctxt (e e-ctxt) 19 (e-ctxt e) 20 hole) 21 (comb i 22 j 23 b 24 c 25 c* 26 w)) 27 28(define ij-relation 29 (reduction-relation 30 lang 31 (--> (in-hole e-ctxt_1 (i e_1)) 32 (in-hole e-ctxt_1 e_1)) 33 (--> (in-hole e-ctxt_1 ((((j e_a) e_b) e_c) e_d)) 34 (in-hole e-ctxt_1 ((e_a e_b) ((e_a e_d) e_c)))))) 35 36(define relation 37 (union-reduction-relations 38 ij-relation 39 (reduction-relation 40 lang 41 (--> (in-hole e-ctxt_1 (((b e_m) e_n) e_l)) 42 (in-hole e-ctxt_1 (e_m (e_n e_l)))) 43 (--> (in-hole e-ctxt_1 (((c e_m) e_n) e_l)) 44 (in-hole e-ctxt_1 ((e_m e_l) e_n))) 45 (--> (in-hole e-ctxt_1 ((c* e_a) e_b)) 46 (in-hole e-ctxt_1 (e_b e_a))) 47 (--> (in-hole e-ctxt_1 ((w e_a) e_b)) 48 (in-hole e-ctxt_1 ((e_a e_b) e_b)))))) 49 50 51(define c* `((j i) i)) 52(define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*))) 53(define (make-b c) `((,c ((j i) ,c)) (j i))) 54(define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*))) 55(define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b))) 56 57(traces relation 58 (list 59 `((,c* abs1) abs2) 60 `(((,(make-c 'c*) abs1) abs2) abs3) 61 `(((,(make-b 'c) abs1) abs2) abs3) 62 `((,(make-w 'b 'c 'c*) abs1) abs2) 63 `(((,(make-s 'b 'c 'w) abs1) abs2) abs3)) 64 #:multiple? #t) 65