1#lang racket
2(require redex/reduction-semantics)
3(provide subst subst-n)
4
5(define-language subst-lang
6  (x variable))
7
8(define-metafunction subst-lang
9  [(subst-n ((x_1 any_1) (x_2 any_2) ... any_3))
10   (subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
11  [(subst-n (any_3)) any_3])
12
13(define-metafunction subst-lang
14  ;; 1. x_1 bound, so don't continue in λ body
15  [(subst (x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2)))
16   (λ (x_2 ... x_1 x_3 ...) any_2)
17   (side-condition (not (member (term x_1) (term (x_2 ...)))))]
18  ;; 2. general purpose capture avoiding case
19  [(subst (x_1 any_1 (λ (x_2 ...) any_2)))
20   ,(term-let ([(x_new ...)
21                (variables-not-in (term (x_1 any_1 any_2))
22                                  (term (x_2 ...)))])
23              (term
24               (λ (x_new ...)
25                 (subst (x_1 any_1 (subst-vars ((x_2 x_new) ... any_2)))))))]
26  ;; 3. replace x_1 with e_1
27  [(subst (x_1 any_1 x_1)) any_1]
28  ;; 4. x_1 and x_2 are different, so don't replace
29  [(subst (x_1 any_1 x_2)) x_2]
30  ;; the last two cases cover all other expression forms
31  [(subst (x_1 any_1 (any_2 ...)))
32   ((subst (x_1 any_1 any_2)) ...)]
33  [(subst (x_1 any_1 any_2)) any_2])
34
35(define-metafunction subst-lang
36  [(subst-vars ((x_1 any_1) x_1)) any_1]
37  [(subst-vars ((x_1 any_1) (any_2 ...))) ((subst-vars ((x_1 any_1) any_2)) ...)]
38  [(subst-vars ((x_1 any_1) any_2)) any_2]
39  [(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3))
40   (subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
41  [(subst-vars (any)) any])
42
43(begin
44  (test-equal (term (subst (x y x))) (term y))
45  (test-equal (term (subst (x y z))) (term z))
46  (test-equal (term (subst (x y (x (y z))))) (term (y (y z))))
47  (test-equal (term (subst (x y ((λ (x) x) ((λ (y1) y1) (λ (x) z))))))
48        (term ((λ (x) x) ((λ (y2) y2) (λ (x) z)))))
49  (test-equal (term (subst (x y (if0 (+ 1 x) x x))))
50        (term (if0 (+ 1 y) y y)))
51  (test-equal (term (subst (x (λ (z) y) (λ (y) x))))
52        (term (λ (y1) (λ (z) y))))
53  (test-equal (term (subst (x 1 (λ (y) x))))
54        (term (λ (y) 1)))
55  (test-equal (term (subst (x y (λ (y) x))))
56        (term (λ (y1) y)))
57  (test-equal (term (subst (x (λ (y) y) (λ (z) (z2 z)))))
58        (term (λ (z1) (z2 z1))))
59  (test-equal (term (subst (x (λ (z) z) (λ (z) (z1 z)))))
60        (term (λ (z2) (z1 z2))))
61  (test-equal (term (subst (x z (λ (z) (z1 z)))))
62        (term (λ (z2) (z1 z2))))
63  (test-equal (term (subst (x3 5 (λ (x2) x2))))
64        (term (λ (x1) x1)))
65  (test-equal (term (subst (z * (λ (z x) 1))))
66        (term (λ (z x) 1)))
67  (test-equal (term (subst (q (λ (x) z) (λ (z x) q))))
68        (term (λ (z1 x1) (λ (x) z))))
69  (test-equal (term (subst (x 1 (λ (x x) x))))
70        (term (λ (x x) x)))
71  (test-results))
72