1#lang racket 2(require redex) 3 4(reduction-steps-cutoff 100) 5 6(define-language lang 7 (e (lambda (x) e) 8 (let (x e) e) 9 (app e e) 10 (+ e e) 11 number 12 x) 13 (e-ctxt (lambda (x) e-ctxt) 14 a-ctxt) 15 (a-ctxt (let (x a-ctxt) e) 16 (app a-ctxt e) 17 (app x a-ctxt) 18 hole) 19 (v (lambda (x) e) 20 x) 21 (x variable)) 22 23(define reductions 24 (reduction-relation 25 lang 26 (--> (in-hole e-ctxt_1 (app (lambda (x_1) e_body) e_arg)) 27 (in-hole e-ctxt_1 (subst (x_1 e_arg e_body)))) 28 (--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1)) 29 (in-hole e-ctxt_1 (subst (x_1 v_1 e_1)))))) 30 31(define-metafunction lang 32 [(subst (x_1 e_1 (lambda (x_1) e_2))) (lambda (x_1) e_2)] 33 [(subst (x_1 e_1 (lambda (x_2) e_2))) 34 ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) 35 (term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))] 36 [(subst (x_1 e_1 (let (x_1 e_2) e_3))) (let (x_1 (subst (x_1 e_1 e_2))) e_3)] 37 [(subst (x_1 e_1 (let (x_2 e_2) e_3))) 38 ,(term-let ((x_new (variable-not-in (term e_1) (term x_2)))) 39 (term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))] 40 [(subst (x_1 e_1 x_1)) e_1] 41 [(subst (x_1 e_1 x_2)) x_2] 42 [(subst (x_1 e_1 (app e_2 e_3))) 43 (app (subst (x_1 e_1 e_2)) 44 (subst (x_1 e_1 e_3)))] 45 [(subst (x_1 e_1 (+ e_2 e_3))) 46 (+ (subst (x_1 e_1 e_2)) 47 (subst (x_1 e_1 e_3)))] 48 [(subst (x_1 e_1 number_1)) number_1]) 49 50(traces reductions 51 '(let (plus (lambda (m) 52 (lambda (n) 53 (lambda (s) 54 (lambda (z) 55 (app (app m s) (app (app n s) z))))))) 56 (let (two (lambda (s) (lambda (z) (app s (app s z))))) 57 (app (app plus two) two)))) 58