1#lang racket 2(require redex) 3 4(provide (all-defined-out)) 5 6;; This semantics comes from the paper 7;; _A Natural Semantics for Lazy Evaluation_, 8;; by John Launchbury, POPL 1993 9;; extended with integers, +, and if0. 10 11(define-language L 12 (e ::= 13 v 14 (e x) 15 (let ([x e] ...) e) 16 x 17 (+ e e) ;; add addition 18 (if0 e e e)) ;; add conditional 19 (v ::= ;; don't use 'z' for values, 20 ;; because that's confusing 21 i ;; add integer constants 22 (λ (x) e)) 23 24 (i ::= integer) 25 (x y z ::= variable-not-otherwise-mentioned) 26 27 (Γ Δ Θ ::= · (Γ x ↦ e))) 28 29(define-judgment-form L 30 #:mode (⇓ I I O O) 31 #:contract (⇓ Γ e Δ v) 32 33 34 [----------- Value 35 (⇓ Γ v Γ v)] 36 37 38 [(⇓ Γ e Δ (λ (y) e_*)) 39 (⇓ Δ (subst e_* y x) Θ v) 40 ------------------------- Application 41 (⇓ Γ (e x) Θ v)] 42 43 44 [(where (Γ x ↦ e) (separate Γ_* x)) 45 (⇓ Γ e Δ v) 46 (where Δ_* (Δ x ↦ v)) 47 ---------------------------------- Variable 48 (⇓ Γ_* x Δ_* (^ Δ_* v))] 49 50 51 [(⇓ (extend Γ (x_i e_i) ...) e Δ v) 52 ---------------------------------- Let 53 (⇓ Γ (let ([x_i e_i] ...) e) Δ v)] 54 55 56 [(⇓ Γ e_1 Θ i_1) 57 (⇓ Θ e_2 Δ i_2) 58 ---------------------------------------------- Add 59 (⇓ Γ (+ e_1 e_2) Δ ,(+ (term i_1) (term i_2)))] 60 61 62 [(⇓ Γ e_1 Θ i) 63 (⇓ Θ (choose i e_2 e_3) Δ v) 64 ---------------------------- If 65 (⇓ Γ (if0 e_1 e_2 e_3) Δ v)]) 66 67(define-metafunction L 68 choose : i e e -> e 69 [(choose 0 e_1 e_2) e_1] 70 [(choose i e_1 e_2) e_2]) 71 72(define-metafunction L 73 separate : Γ x -> (Γ x ↦ e) or ⊥ 74 [(separate · x) ⊥] 75 [(separate (Γ x ↦ e) x) (Γ x ↦ e)] 76 [(separate (Γ y ↦ e_*) x) 77 ((Γ_* y ↦ e_*) x ↦ e) 78 (where (Γ_* x ↦ e) (separate Γ x))] 79 [(separate (Γ y ↦ e_*) x) ⊥ 80 (where ⊥ (separate Γ x))]) 81 82(define-metafunction L 83 extend : Γ (x e) ... -> Γ 84 [(extend Γ) Γ] 85 [(extend Γ (x e) (x_* e_*) ...) 86 (extend (Γ x ↦ e) (x_* e_*) ...)]) 87 88(define-metafunction L 89 subst : e x y -> e 90 [(subst e x y) 91 (subst/no-avoid (rename-bound e y y_*) x y) 92 (where y_* ,(variable-not-in (term (e x y)) (term y)))]) 93 94;; renames bound occurrences of 'x' to 'y' 95;; makes sense only when 'y' doesn't appear in 'e' 96(define-metafunction L 97 rename-bound : e x y -> e 98 [(rename-bound i x y) i] 99 [(rename-bound (λ (x) e) x y) (λ (y) (rename-all e x y))] 100 [(rename-bound (λ (z) e) x y) (λ (z) (rename-bound e x y))] 101 [(rename-bound (e z) x y) ((rename-bound e x y) z)] 102 [(rename-bound (let ([x_* e_*] ... [x e] [x_** e_**] ...) e_***) x y) 103 (let ([x_* (rename-bound e_* x y)] ... 104 [y (rename-bound e x y)] 105 [x_** (rename-bound e_** x y)] ...) 106 (rename-all e_*** x y))] 107 [(rename-bound (let ([z e] ...) e_*) x y) 108 (let ([z (rename-bound e x y)] ...) (rename-bound e_* x y))] 109 [(rename-bound z x y) z] 110 [(rename-bound (+ e_1 e_2) x y) (+ (rename-bound e_1 x y) (rename-bound e_2 x y))] 111 [(rename-bound (if0 e_1 e_2 e_3) x y) 112 (if0 (rename-bound e_1 x y) 113 (rename-bound e_2 x y) 114 (rename-bound e_3 x y))]) 115 116(define-metafunction L 117 subst/no-avoid : e x y -> e 118 [(subst/no-avoid i x y) i] 119 [(subst/no-avoid (λ (x) e) x y) (λ (x) e)] 120 [(subst/no-avoid (λ (z) e) x y) (λ (z) (subst/no-avoid e x y))] 121 [(subst/no-avoid (e z) x y) ((subst/no-avoid e x y) (subst/no-avoid z x y))] 122 [(subst/no-avoid (let ([z e] ... [x e_*] [z_** e_**] ...) e_***) x y) 123 (let ([z (subst/no-avoid e x y)] ... 124 [x (subst/no-avoid e_* x y)] 125 [z_** (subst/no-avoid e_** x y)] ...) 126 e_***)] 127 [(subst/no-avoid (let ([z e] ...) e_**) x y) 128 (let ([z (subst/no-avoid e x y)] ...) 129 (subst/no-avoid e_** x y))] 130 [(subst/no-avoid x x y) y] 131 [(subst/no-avoid z x y) z] 132 [(subst/no-avoid (+ e_1 e_2) x y) (+ (subst/no-avoid e_1 x y) (subst/no-avoid e_2 x y))] 133 [(subst/no-avoid (if0 e_1 e_2 e_3) x y) 134 (if0 (subst/no-avoid e_1 x y) 135 (subst/no-avoid e_2 x y) 136 (subst/no-avoid e_3 x y))]) 137 138;; renames all occurrences of 'x' to 'y' 139(define-metafunction L 140 rename-all : any x y -> any 141 [(rename-all x x y) y] 142 [(rename-all z x y) z] 143 [(rename-all (any ...) x y) ((rename-all any x y) ...)] 144 [(rename-all any x y) any]) 145 146;; The ^ function freshens all of the bound 147;; variables in the 'e' argument, making sure 148;; that none of the new variables appear in Δ. 149;; For example, (λ (x) x) turns into (λ (x1) x1) 150;; (assuming that x appears in Δ). 151;; The function is part of preserving the invariant 152;; that there are no duplicate variables bound 153;; in the environment in the first and third 154;; positions in the semantics. 155(define-metafunction L 156 ^ : Δ e -> e 157 [(^ Δ e) 158 e_* 159 (where (e_* (x ...)) (^/h Δ e ()))]) 160 161(define-metafunction L 162 ^/h : Δ e (z ...) -> (e (z ...)) 163 [(^/h Δ i (z ...)) (i (z ...))] 164 [(^/h Δ (λ (x) e) (z ...)) 165 ((λ (y) e_*) (z_* ...)) 166 (where y ,(variable-not-in (term (Δ z ...)) (term x))) 167 (where (e_* (z_* ...)) (^/h Δ (replace-free e (x y)) (y z ...)))] 168 [(^/h Δ (e x) (z ...)) 169 ((e_* x_*) (z ...)) 170 (where (e_* (z_* ...)) (^/h Δ e (z ...))) 171 (where (x_* (z_** ...)) (^/h Δ x (z_* ...)))] 172 [(^/h Δ (let () e) (z ...)) 173 ((let () e_*) (z_* ...)) 174 (where (e_* (z_* ...)) (^/h Δ e (z ...)))] 175 [(^/h Δ (let ([x_1 e_1] [x_2 e_2] ...) e) (z ...)) 176 ((let ([y_1 e_1*] [x_2* e_2*] ...) e_*) (z_** ...)) 177 (where y_1 ,(variable-not-in (term (Δ z ...)) (term x_1))) 178 (where ((let ([x_2* e_2*] ...) e_*) (z_* ...)) 179 (^/h Δ (let ([x_2 e_2] ...) (replace-free e (x_1 y_1))) (y_1 z ...))) 180 (where (e_1* (z_** ...)) (^/h Δ e_1 (z_* ...)))] 181 [(^/h Δ x (z ...)) (x (z ...))] 182 [(^/h Δ (+ e_1 e_2) (z ...)) 183 ((+ e_1* e_2*) (z_** ...)) 184 (where (e_1* (z_* ...)) (^/h Δ e_1 (z ...))) 185 (where (e_2* (z_** ...)) (^/h Δ e_2 (z_* ...)))] 186 [(^/h Δ (if0 e_1 e_2 e_3) (z ...)) 187 ((if0 e_1* e_2* e_3*) (z_* ...)) 188 (where ((+ (+ e_1* e_2*) e_3*) (z_* ...)) (^/h Δ (+ (+ e_1 e_2) e_3) (z ...)))]) 189 190(define-metafunction L 191 replace-free : e (x y) ... -> e 192 [(replace-free i (x y) ...) i] 193 [(replace-free (λ (x) e) (x_* y_*) ... (x y) (x_** y_**) ...) 194 (replace-free (λ (x) e) (x_* y_*) ... (x_** y_**) ...)] 195 [(replace-free (λ (z) e) (x y) ...) (λ (z) (replace-free e (x y) ...))] 196 [(replace-free (e z) (x y) ...) 197 ((replace-free e (x y) ...) (replace-free z (x y) ...))] 198 [(replace-free (let ([z e] ...) e_*) (x y) ...) 199 (let ([z (replace-free e (x y) ...)] ...) 200 (replace-free e_* (x_2 y_2) ...)) 201 (where ((x_2 y_2) ...) (remove-used-bindings ((x y) ...) (z ...)))] 202 [(replace-free x (x_1 x_2) ... (x y) (x_3 x_4) ...) y] 203 [(replace-free z (x y) ...) z] 204 [(replace-free (+ e_1 e_2) (x y) ...) 205 (+ (replace-free e_1 (x y) ...) (replace-free e_2 (x y) ...))] 206 [(replace-free (if0 e_1 e_2 e_3) (x y) ...) 207 (if0 (replace-free e_1 (x y) ...) 208 (replace-free e_2 (x y) ...) 209 (replace-free e_3 (x y) ...))]) 210 211(define-metafunction L 212 [(remove-used-bindings ((x_1 y_1) ... (x_2 y_2) (x_3 y_3) ...) 213 (x_4 ... x_2 x_5 ...)) 214 (remove-used-bindings ((x_1 y_1) ... (x_3 y_3) ...) 215 (x_4 ... x_2 x_5 ...))] 216 [(remove-used-bindings ((x y) ...) 217 (z ...)) 218 ((x y) ...)]) 219 220(define e? (redex-match? L e)) 221(define v? (redex-match? L v)) 222(define T-v? (redex-match? L (T v))) 223 224 225;; run a program to get it's result 226(define/contract (run p) 227 (-> e? (or/c v? #f)) 228 (define vs (judgment-holds (⇓ · ,p Δ v) v)) 229 (cond 230 [(pair? vs) 231 (unless (= 1 (length vs)) 232 (error 'run "multiple results ~s" vs)) 233 (car vs)] 234 [else #f])) 235 236;; opens a visualization of the derivation 237(define (show p) 238 (-> e? void?) 239 (show-derivations 240 (build-derivations 241 (⇓ · ,p Δ v)))) 242 243(module+ test 244 245 (test-equal (term (replace-free (let ([x x] [p q]) x) (x y))) 246 (term (let ([x y] [p q]) x))) 247 (test-equal (term (replace-free (let ([p q]) x) (x y))) 248 (term (let ([p q]) y))) 249 (test-equal (term (replace-free (λ (x) y) (y z))) 250 (term (λ (x) z))) 251 (test-equal (term (replace-free (λ (y) y) (y z))) 252 (term (λ (y) y))) 253 (test-equal (term (replace-free (if0 x y z) (y z))) 254 (term (if0 x z z))) 255 256 (test-equal (term (rename-bound (λ (x) x) x y)) 257 (term (λ (y) y))) 258 (test-equal (term (rename-bound (λ (y) x) x y)) 259 (term (λ (y) x))) 260 (test-equal (term (rename-bound (λ (x) (λ (x) x)) x y)) 261 (term (λ (y) (λ (y) y)))) 262 (test-equal (term (rename-bound (let ([x 1] [y 2]) x) x z)) 263 (term (let ([z 1] [y 2]) z))) 264 265 (test-equal (term (subst (λ (x) ((λ (y) x) y)) y z)) 266 (term (λ (x) ((λ (y) x) z)))) 267 (test-equal (term (subst (λ (x) ((λ (y) y) y)) y z)) 268 (term (λ (x) ((λ (y) y) z)))) 269 (test-equal (term (subst (λ (x) ((λ (q) y) y)) y z)) 270 (term (λ (x) ((λ (q) z) z)))) 271 (test-equal (term (subst (λ (y) x) x y)) 272 (term (λ (y1) y))) 273 (test-equal (term (subst (let ([x 1]) (+ x z)) z q)) 274 (term (let ([x 1]) (+ x q)))) 275 (test-equal (term (subst (let ([x 1][y 2][z 3]) (+ x y)) x q)) 276 (term (let ([x 1][y 2][z 3]) (+ x y)))) 277 278 (test-equal (term (separate · x)) (term ⊥)) 279 (test-equal (term (separate (· x ↦ 1) x)) (term (· x ↦ 1))) 280 (test-equal (term (separate ((· x ↦ 1) y ↦ 2) x)) 281 (term ((· y ↦ 2) x ↦ 1))) 282 (test-equal (term (separate (· x ↦ 1) y)) (term ⊥)) 283 284 (test-equal (term (^ (· x ↦ (λ (x) x)) (λ (x) x))) 285 (term (λ (x1) x1))) 286 (test-equal (term (^ · (λ (x) (λ (y) (x y))))) 287 (term (λ (x) (λ (y) (x y))))) 288 (test-equal (term (^ (· x ↦ y) (let ([x 1] [y 2]) x))) 289 (term (let ([x1 1] [y1 2]) x1))) 290 (test-equal (term (^ (· x ↦ x1) (λ (x) (+ x y)))) 291 (term (λ (x2) (+ x2 y)))) 292 (test-equal (term (^ (· tri ↦ (λ (x) (let ((x1 x)) x1))) 293 (λ (x) (let ((x1 x)) x1)))) 294 (term (λ (x2) (let ((x3 x2)) x3)))) 295 (test-equal (term (^ (· x ↦ 1) 296 (let ([x (let ([x 1]) x)]) 297 (let ([x (let ([x 2]) x)]) 298 x)))) 299 (term (let ([x1 (let ([x4 1]) x4)]) 300 (let ([x2 (let ([x3 2]) x3)]) 301 x2)))) 302 (test-equal (term (^ (· x ↦ 1) 303 (if0 x (λ (x) x) x))) 304 (term (if0 x (λ (x1) x1) x))) 305 306 (test-equal (judgment-holds (⇓ (· y ↦ 1) ((λ (x) x) y) Δ v) v) 307 (list (term 1))) 308 309 (test-equal (run (term 1)) 1) 310 (test-equal (run (term (let ([y 1]) 311 (let ([z ((λ (x) x) y)]) 312 2)))) 313 2) 314 (test-equal (run (term (let ([y 1]) y))) 1) 315 (test-equal (run (term (let ([y (λ (x) x)]) y))) (term (λ (x1) x1))) 316 (test-equal (run (term (let ([y 1]) ((λ (x) x) y)))) 1) 317 (test-equal (run (term 318 (let ([app (λ (f) (λ (x) (f x)))] 319 [f (λ (x) (λ (y) x))] 320 [o 1]) 321 (((app f) o) f)))) 322 1) 323 (test-equal (run (term (if0 0 1 2))) 1) 324 (test-equal (run (term (if0 1 2 3))) 3) 325 326 ;; free variable errors return no derivation 327 (test-equal (run (term (let ([x y]) x))) #f) 328 329 ;; as do runtime errors 330 (test-equal (run (term (let ([two 2]) (1 two)))) #f) 331 332 (test-equal (run 333 (term 334 (let ([o 1] 335 [t 2] 336 [r 3] 337 [f 4]) 338 (((((λ (x) 339 (λ (y) 340 (λ (z) 341 (λ (w) 342 (+ (+ x y) 343 (+ w z)))))) 344 o) 345 t) 346 r) 347 f)))) 348 10) 349 350 (test-equal (run (term 351 (let ([me (λ (x) x)]) 352 (let ([tri 353 (λ (x) 354 (let ([x1 (+ x -1)]) 355 (+ (me x1) x)))] 356 [five 5]) 357 (tri five))))) 358 9) 359 360 (test-equal (run (term (let ([tri 361 (λ (x) 362 (let ([x1 (+ x -1)]) 363 x))] 364 [five 5]) 365 (tri five)))) 366 5) 367 368 (test-equal (run (term 369 (let ([Y (λ (f) 370 (let ([g (λ (x) 371 (let ([xx (x x)]) 372 (f xx)))]) 373 (g g)))] 374 [tri 375 (λ (me) 376 (λ (x) 377 (if0 x 378 0 379 (let ([x1 (+ x -1)]) 380 (+ (me x1) x)))))] 381 [five 5]) 382 ((Y tri) five)))) 383 (+ 5 4 3 2 1 0)) 384 385 (test-results)) 386