|
| 1 | +(load "pmatch.scm") |
| 2 | + |
| 3 | +(define occur-free? |
| 4 | + (lambda (y exp) |
| 5 | + (pmatch exp |
| 6 | + [,x (guard (symbol? x)) (eq? y x)] |
| 7 | + [(lambda (,x) ,e) (and (not (eq? y x)) (occur-free? y e))] |
| 8 | + [(,rator ,rand) (or (occur-free? y rator) (occur-free? y rand))]))) |
| 9 | + |
| 10 | +(define value? |
| 11 | + (lambda (exp) |
| 12 | + (pmatch exp |
| 13 | + [,x (guard (symbol? x)) #t] |
| 14 | + [(lambda (,x) ,e) #t] |
| 15 | + [(,rator ,rand) #f]))) |
| 16 | + |
| 17 | +(define app? (lambda (x) (not (value? x)))) |
| 18 | + |
| 19 | +(define term-length |
| 20 | + (lambda (exp) |
| 21 | + (pmatch exp |
| 22 | + [,x (guard (symbol? x)) 0] |
| 23 | + [(lambda (,x) ,e) (+ 1 (term-length e))] |
| 24 | + [(,rator ,rand) (+ 1 (term-length rator) (term-length rand))]))) |
| 25 | + |
| 26 | +; call-by-name compiler to S, K, I |
| 27 | +(define compile |
| 28 | + (lambda (exp) |
| 29 | + (pmatch exp |
| 30 | + [,x (guard (symbol? x)) x] |
| 31 | + [(,M ,N) `(,(compile M) ,(compile N))] |
| 32 | + [(lambda (,x) (,M ,y)) |
| 33 | + (guard (eq? x y) (not (occur-free? x M))) (compile M)] |
| 34 | + [(lambda (,x) ,y) (guard (eq? x y)) `I] |
| 35 | + [(lambda (,x) (,M ,N)) (guard (or (occur-free? x M) (occur-free? x N))) |
| 36 | + `((S ,(compile `(lambda (,x) ,M))) ,(compile `(lambda (,x) ,N)))] |
| 37 | + [(lambda (,x) ,M) (guard (not (occur-free? x M))) `(K ,(compile M))] |
| 38 | + [(lambda (,x) ,M) (guard (occur-free? x M)) |
| 39 | + (compile `(lambda (,x) ,(compile M)))]))) |
| 40 | + |
| 41 | +; call-by-name compiler to S, K, I, B, C |
| 42 | +(define compile-bc |
| 43 | + (lambda (exp) |
| 44 | + (pmatch exp |
| 45 | + [,x (guard (symbol? x)) x] |
| 46 | + [(,M ,N) `(,(compile-bc M) ,(compile-bc N))] |
| 47 | + [(lambda (,x) ,y) (guard (eq? x y)) `I] |
| 48 | + [(lambda (,x) (,M ,y)) |
| 49 | + (guard (eq? x y) (not (occur-free? x M))) (compile-bc M)] |
| 50 | + [(lambda (,x) (,M ,N)) (guard (and (not (occur-free? x M)) (occur-free? x N))) |
| 51 | + `((B ,(compile-bc M)) ,(compile-bc `(lambda (,x) ,N)))] |
| 52 | + [(lambda (,x) (,M ,N)) (guard (and (occur-free? x M) (not (occur-free? x N)))) |
| 53 | + `((C ,(compile-bc `(lambda (,x) ,M))) ,(compile-bc N))] |
| 54 | + [(lambda (,x) (,M ,N)) (guard (or (occur-free? x M) (occur-free? x N))) |
| 55 | + `((S ,(compile-bc `(lambda (,x) ,M))) ,(compile-bc `(lambda (,x) ,N)))] |
| 56 | + [(lambda (,x) ,M) (guard (not (occur-free? x M))) `(K ,(compile-bc M))] |
| 57 | + [(lambda (,x) ,M) (guard (occur-free? x M)) |
| 58 | + (compile-bc `(lambda (,x) ,(compile-bc M)))]))) |
| 59 | + |
| 60 | + |
| 61 | + |
| 62 | +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
| 63 | +;; ski->lanbda converter |
| 64 | +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
| 65 | +;; create gensyms |
| 66 | +(define fv |
| 67 | + (let ((n -1)) |
| 68 | + (lambda (x) |
| 69 | + (set! n (+ 1 n)) |
| 70 | + (string->symbol |
| 71 | + (string-append (symbol->string x) "." (number->string n)))))) |
| 72 | + |
| 73 | +;; substitution with free variable capturing avoiding |
| 74 | +(define subst |
| 75 | + (lambda (x y exp) |
| 76 | + (pmatch exp |
| 77 | + [,u (guard (symbol? u)) (if (eq? u x) y u)] |
| 78 | + [(lambda (,u) ,e) |
| 79 | + (cond |
| 80 | + [(eq? u x) exp] |
| 81 | + [(occur-free? u y) ; possible capture, switch names |
| 82 | + (let* ([u* (fv u)] |
| 83 | + [e* (subst u u* e)]) |
| 84 | + `(lambda (,u*) ,(subst x y e*)))] |
| 85 | + [else |
| 86 | + `(lambda (,u) ,(subst x y e))])] |
| 87 | + [(,e1 ,e2) `(,(subst x y e1) ,(subst x y e2))] |
| 88 | + [,exp exp]))) |
| 89 | + |
| 90 | + |
| 91 | +; combinator definitions |
| 92 | +(define com-table |
| 93 | + '((S . (lambda (f) (lambda (g) (lambda (x) ((f x) (g x)))))) |
| 94 | + (K . (lambda (x) (lambda (y) x))) |
| 95 | + (I . (lambda (x) x)) |
| 96 | + (B . (lambda (f) (lambda (g) (lambda (x) (f (g x)))))) |
| 97 | + (C . (lambda (a) (lambda (b) (lambda (c) ((a c) b))))))) |
| 98 | + |
| 99 | +; substitute combinator with their lambda term definitions |
| 100 | +(define sub-com |
| 101 | + (lambda (exp defs) |
| 102 | + (cond |
| 103 | + [(null? defs) exp] |
| 104 | + [else (sub-com (subst (caar defs) (cdar defs) exp) (cdr defs))]))) |
| 105 | + |
| 106 | +(define ski->lambda |
| 107 | + (lambda (exp) |
| 108 | + (sub-com exp com-table))) |
| 109 | + |
| 110 | + |
| 111 | +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
| 112 | +;; tests |
| 113 | +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
| 114 | +(define to-number `(lambda (n) ((n (lambda (x) (,add1 x))) 0))) |
| 115 | + |
| 116 | +(interp `(,to-number ,(ski->lambda (compile-bc `(,!-n ,lfive))))) |
| 117 | +; => 120 |
| 118 | +(term-length `(,! ,lfive)) |
| 119 | +; => 93 |
| 120 | +(term-length (compile `(,! ,lfive))) |
| 121 | +; => 144 |
| 122 | +(term-length (compile-bc `(,! ,lfive))) |
| 123 | +; => 73 |
| 124 | + |
0 commit comments