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