1#lang racket 2(require redex 3 "subst.rkt") 4 5(reduction-steps-cutoff 10) 6 7(define-language lang 8 (e (e e) 9 x 10 number 11 (lambda (x t) e) 12 (if e e e) 13 (= e e) 14 (-> e e) 15 num 16 bool) 17 (c (t c) 18 (c e) 19 (-> t c) 20 (-> c e) 21 (= t c) 22 (= c e) 23 (if c e e) 24 (if t c e) 25 (if t t c) 26 hole) 27 (x (variable-except lambda -> if =)) 28 (t num bool (-> t t))) 29 30(define reductions 31 (reduction-relation 32 lang 33 (r--> number num) 34 35 (r--> (lambda (x_1 t_1) e_body) 36 (-> t_1 (subst (x_1 t_1 e_body)))) 37 38 (r--> ((-> t_1 t_2) t_1) t_2) 39 40 (e--> (side-condition ((-> t_1 t) t_2) 41 (not (equal? (term t_1) (term t_2)))) 42 ,(format "app: domain error ~s and ~s" (term t_1) (term t_2))) 43 44 (e--> (num t_1) 45 ,(format "app: non function error ~s" (term t_1))) 46 47 (r--> (if bool t_1 t_1) t_1) 48 (e--> (side-condition (if bool t_1 t_2) 49 (not (equal? (term t_1) (term t_2)))) 50 ,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2))) 51 (e--> (side-condition (if t_1 t t) 52 (not (equal? (term t_1) 'bool))) 53 ,(format "if: test not boolean ~s" (term t_1))) 54 55 (r--> (= num num) bool) 56 (e--> (side-condition (= t_1 t_2) 57 (or (not (equal? (term t_1) 'num)) 58 (not (equal? (term t_2) 'num)))) 59 ,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2))) 60 61 with 62 63 [(--> (in-hole c_1 a) (in-hole c_1 b)) (r--> a b)] 64 [(--> (in-hole c a) b) (e--> a b)])) 65 66(traces reductions 67 '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1)) 68(traces reductions 69 '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1)) 70