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