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