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