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