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