1#lang racket 2(require redex) 3(provide λ λv red typeof) 4 5(define-language λ 6 (e (e e) 7 x 8 (λ (x τ) e) 9 (if0 e e e) 10 (+ e e) 11 number) 12 (τ (τ -> τ) num) 13 (x variable-not-otherwise-mentioned)) 14 15(define-extended-language λv λ 16 (v (λ (x τ) e) number) 17 (E hole 18 (v E) (E e) 19 (if0 E e e) 20 (+ E e) (+ v E)) 21 (Γ · (x τ Γ))) 22 23(define red 24 (reduction-relation 25 λv 26 (--> (in-hole E (+ number_1 number_2)) 27 (in-hole E (Σ number_1 number_2)) 28 "+") 29 (--> (in-hole E (if0 0 e_1 e_2)) 30 (in-hole E e_1) 31 "if0t") 32 (--> (in-hole E (if0 number e_1 e_2)) 33 (in-hole E e_2) 34 "if0f" 35 (side-condition 36 (not (= 0 (term number))))) 37 (--> (in-hole E ((λ (x τ) e) v)) 38 (in-hole E (subst x v e)) 39 "βv"))) 40 41(define-metafunction λv 42 Σ : number number -> number 43 [(Σ number_1 number_2) 44 ,(+ (term number_1) (term number_2))]) 45 46(define-metafunction λv 47 subst : x any any -> any 48 ;; 1. x_1 bound, so don't continue in λ body 49 [(subst x_1 any_1 (λ (x_1 τ_1) any_2)) 50 (λ (x_1 τ_1) any_2)] 51 ;; 2. general purpose capture avoiding case 52 [(subst x_1 any_1 (λ (x_2 τ_2) any_2)) 53 (λ (x_new τ_2) 54 (subst x_1 any_1 55 (subst-var x_2 x_new 56 any_2))) 57 (where (x_new) 58 ,(variables-not-in 59 (term (x_1 any_1 any_2)) 60 (term (x_2))))] 61 ;; 3. replace x_1 with e_1 62 [(subst x_1 any_1 x_1) any_1] 63 ;; 4. x_1 and x_2 are different, so don't replace 64 [(subst x_1 any_1 x_2) x_2] 65 ;; the last cases cover all other expressions 66 [(subst x_1 any_1 (any_2 ...)) 67 ((subst x_1 any_1 any_2) ...)] 68 [(subst x_1 any_1 any_2) any_2]) 69 70(define-metafunction λv 71 subst-var : x any any -> any 72 [(subst-var x_1 any_1 x_1) any_1] 73 [(subst-var x_1 any_1 (any_2 ...)) 74 ((subst-var x_1 any_1 any_2) ...)] 75 [(subst-var x_1 any_1 any_2) any_2]) 76 77(define-judgment-form λv 78 #:mode (typeof I I O) 79 #:contract (typeof Γ e τ) 80 81 [--------------------- 82 (typeof Γ number num)] 83 84 [(typeof Γ e_1 num) 85 (typeof Γ e_2 num) 86 -------------------------- 87 (typeof Γ (+ e_1 e_2) num)] 88 89 [(typeof Γ e_1 num) 90 (typeof Γ e_2 τ) 91 (typeof Γ e_3 τ) 92 ------------------------------ 93 (typeof Γ (if0 e_1 e_2 e_3) τ)] 94 95 [(where τ (lookup Γ x)) 96 ---------------------- 97 (typeof Γ x τ)] 98 99 [(typeof Γ e_1 (τ_2 -> τ)) 100 (typeof Γ e_2 τ_2) 101 -------------------------- 102 (typeof Γ (e_1 e_2) τ)] 103 104 [(typeof (x_1 τ_1 Γ) e τ) 105 ---------------------------------------- 106 (typeof Γ (λ (x_1 τ_1) e) (τ_1 -> τ))]) 107 108(define-metafunction λv 109 lookup : Γ x -> τ or #f 110 [(lookup (x τ Γ) x) τ] 111 [(lookup (x_1 τ Γ) x_2) (lookup Γ x_2)] 112 [(lookup · x) #f]) 113 114 115;; remove this #; to run an example 116#; 117(traces red 118 (term 119 (+ ((λ (n num) 120 (if0 n 121 1 122 0)) 123 (+ 2 2)) 124 2))) 125 126;; remove this #; to generate a random well-typed term 127#; 128(generate-term λv #:satisfying (typeof · e num) 5) 129 130 131(define (preservation e) 132 (define types (judgment-holds (typeof · ,e τ) τ)) 133 (unless (null? types) 134 (unless (= 1 (length types)) (error 'preservation "multiple types! ~s" e))) 135 (cond 136 [(null? types) #t] 137 [else 138 (for/and ([v (apply-reduction-relation* red e)]) 139 (equal? (judgment-holds (typeof · ,v τ) τ) 140 types))])) 141 142(define (try-it) 143 (redex-check λv 144 #:satisfying (typeof · e num) 145 (preservation (term e)))) 146 147(test-->> red (term ((λ (x num) x) 1)) 1) 148(test-->> red (term (((λ (x num) (λ (y num) x)) 1) 2)) 1) 149(test-->> red (term (((λ (x num) (λ (y num) y)) 1) 2)) 2) 150(test-->> red (term (((λ (x num) (λ (x num) x)) 1) 2)) 2) 151(test-->> red (term (((λ (x num) (λ (y num) x)) 1) 2)) 1) 152(test-->> red (term ((λ (x num) (+ x x)) 2)) 4) 153(test-->> red (term ((λ (x num) (if0 x x (+ x 1))) 2)) 3) 154(test-->> red (term ((λ (x num) (if0 x x (+ x 1))) 0)) 0) 155(test-->> red 156 (term (((λ (x num) (λ (y num) (λ (z num) x))) 1) 2)) 157 (term (λ (z num) 1))) 158(test-->> red 159 (term (+ (+ 1 2) (+ 3 4))) 160 (term 10)) 161 162(test-equal (term (subst x y x)) (term y)) 163(test-equal (term (subst x y z)) (term z)) 164(test-equal (term (subst x y (x (y z)))) (term (y (y z)))) 165(test-equal (term (subst x y ((λ (x num) x) ((λ (y1 num) y1) (λ (x num) z))))) 166 (term ((λ (x num) x) ((λ (y2 num) y2) (λ (x num) z))))) 167(test-equal (term (subst x y (if0 (+ 1 x) x x))) 168 (term (if0 (+ 1 y) y y))) 169(test-equal (term (subst x (λ (z num) y) (λ (y num) x))) 170 (term (λ (y1 num) (λ (z num) y)))) 171(test-equal (term (subst x 1 (λ (y num) x))) 172 (term (λ (y num) 1))) 173(test-equal (term (subst x y (λ (y num) x))) 174 (term (λ (y1 num) y))) 175(test-equal (term (subst x (λ (y num) y) (λ (z num) (z2 z)))) 176 (term (λ (z1 num) (z2 z1)))) 177(test-equal (term (subst x (λ (z num) z) (λ (z num) (z1 z)))) 178 (term (λ (z2 num) (z1 z2)))) 179(test-equal (term (subst x z (λ (z num) (z1 z)))) 180 (term (λ (z2 num) (z1 z2)))) 181(test-equal (term (subst x3 5 (λ (x2 num) x2))) 182 (term (λ (x1 num) x1))) 183(test-equal (term (subst z * (λ (z num) (λ (x num) 1)))) 184 (term (λ (z num) (λ (x num) 1)))) 185(test-equal (term (subst q (λ (x num) z) (λ (z num) (λ (x num) q)))) 186 (term (λ (z1 num) (λ (x1 num) (λ (x num) z))))) 187(test-equal (term (subst x 1 (λ (x num) (λ (x num) x)))) 188 (term (λ (x num) (λ (x num) x)))) 189 190(define (typecheck G e) 191 (match (judgment-holds (typeof ,G ,e τ) τ) 192 [(list) #f] 193 [(list t) t] 194 [_ (error 'typecheck 195 "multiple typing derivations for term ~a in environment ~a" 196 e G)])) 197 198(test-equal (typecheck (term ·) (term 1)) 199 (term num)) 200(test-equal (typecheck (term ·) (term (1 1))) 201 #f) 202(test-equal (typecheck (term (x num ·)) (term x)) 203 (term num)) 204(test-equal (typecheck (term ·) (term x)) 205 #f) 206(test-equal (typecheck (term ·) (term ((λ (x num) x) 1))) 207 (term num)) 208(test-equal (typecheck (term ·) (term (((λ (x num) x) 1) 2))) 209 #f) 210(test-equal (typecheck (term ·) 211 (term (((λ (f (num -> num)) 212 (λ (x num) 213 (f x))) 214 (λ (x num) x)) 215 1))) 216 (term num)) 217(test-equal (typecheck (term ·) 218 (term (((λ (f (num -> num)) 219 (λ (x num) 220 (f x))) 221 1) 222 (λ (x num) x)))) 223 #f) 224(test-equal (typecheck (term ·) (term (+ (+ 1 2) 3))) 225 (term num)) 226(test-equal (typecheck (term ·) (term (if0 1 (λ (x num) x) 3))) 227 #f) 228(test-equal (typecheck (term ·) (term (if0 1 2 3))) 229 (term num)) 230(test-equal (typecheck (term ·) (term (λ (x num) (x 2)))) 231 #f) 232(test-equal (typecheck (term ·) 233 (term (λ (x num) 234 (λ (x (num -> num)) 235 (x 0))))) 236 (term (num -> ((num -> num) -> num)))) 237(test-equal (typecheck (term ·) 238 (term (λ (x (num -> num)) 239 (λ (x num) 240 (x 0))))) 241 #f) 242 243(test-results) 244