1#lang racket
2(require redex)
3
4(reduction-steps-cutoff 10)
5
6(define-language lang
7  (e (e e)
8     (abort e)
9     x
10     v)
11  (x (variable-except lambda call/cc abort))
12  (c (v c)
13     (c e)
14     hole)
15  (v call/cc
16     number
17     (lambda (x t) e))
18  (t num
19     (t -> t)))
20
21(define reductions
22  (reduction-relation
23   lang
24   (--> (in-hole c_1 (call/cc v_arg))
25        ,(term-let ([v (variable-not-in (term c_1) 'x)])
26           (term
27            (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))
28        call/cc)
29   (--> (in-hole c (abort e_1))
30        e_1
31        abort)
32
33   ;; this rules calls subst with the wrong arguments, which is caught by the example below.
34   (--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual))
35        (in-hole c_1 (subst (x_format e_body v_actual)))
36        βv)))
37
38(define (type-check term)
39  (let/ec k
40    (let loop ([term term]
41               [env '()])
42      (match term
43        [(? symbol?)
44         (let ([l (assoc term env)])
45           (if l
46               (cdr l)
47               (k #f)))]
48        [(? number?) 'num]
49        [`(lambda (,x ,t) ,b)
50         (let ([body (loop b (cons (cons x t) env))])
51           `(,t -> ,body))]
52        [`(,e1 ,e2)
53         (let ([t1 (loop e1 env)]
54               [t2 (loop e2 env)])
55           (match t1
56             [`(,td -> ,tr)
57              (if (equal? td t2)
58                  tr
59                  (k #f))]
60             [else (k #f)]))]))))
61
62(define (pred term1)
63  (let ([t1 (type-check term1)])
64    (lambda (term2)
65      (and t1
66           (equal? (type-check term2) t1)))))
67
68(define-language subst-lang
69  (x variable))
70
71(define-metafunction subst-lang
72  [(subst-n ((x_1 any_1) (x_2 any_2) ... any_3))
73   (subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
74  [(subst-n (any_3)) any_3])
75
76(define-metafunction subst-lang
77  ;; 1. x_1 bound, so don't continue in λ body
78  [(subst (x_1 any_1 (λ (x_1 t) any_2)))
79   (λ (x_1 t) any_2)]
80  ;; 2. general purpose capture avoiding case
81  [(subst (x_1 any_1 (λ (x_2 t) any_2)))
82   ,(term-let ([x_new
83                (variable-not-in (term (x_1 any_1 any_2))
84                                 (term x_2))])
85              (term
86               (λ (x_new t)
87                 (subst (x_1 any_1 (subst-vars ((x_2 x_new) any_2)))))))]
88  ;; 3. replace x_1 with e_1
89  [(subst (x_1 any_1 x_1)) any_1]
90  ;; 4. x_1 and x_2 are different, so don't replace
91  [(subst (x_1 any_1 x_2)) x_2]
92  ;; the last two cases cover all other expression forms
93  [(subst (x_1 any_1 (any_2 ...)))
94   ((subst (x_1 any_1 any_2)) ...)]
95  [(subst (x_1 any_1 any_2)) any_2])
96
97(define-metafunction subst-lang
98  [(subst-vars ((x_1 any_1) x_1)) any_1]
99  [(subst-vars ((x_1 any_1) (any_2 ...))) ((subst-vars ((x_1 any_1) any_2)) ...)]
100  [(subst-vars ((x_1 any_1) any_2)) any_2]
101  [(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3))
102   (subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
103  [(subst-vars (any)) any])
104
105(define (show term)
106  (traces reductions term #:pred (pred term)))
107
108(show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x))))
109