1#lang racket
2(require redex "subst.rkt")
3
4(reduction-steps-cutoff 10)
5
6(define-language lang
7  (e (e e)
8     (abort e)
9     x
10     v)
11  (c (v c)
12     (c e)
13     hole)
14  (v call/cc
15     number
16     (lambda (x) e))
17
18  (x (variable-except lambda call/cc abort)))
19
20(define reductions
21  (reduction-relation
22   lang
23   (--> (in-hole c (call/cc v))
24        (in-hole c (v (lambda (x) (abort (in-hole c x)))))
25        call/cc
26        (fresh x))
27   (--> (in-hole c (abort e))
28        e
29        abort)
30   (--> (in-hole c ((lambda (x) e) v))
31        (in-hole c (subst (x v e)))
32        βv)))
33
34(traces reductions '((lambda (x) (x x)) (lambda (x) (x x))))
35(traces reductions '((call/cc call/cc) (call/cc call/cc)))
36(traces reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
37