|
| 1 | +;; |
| 2 | +;; Playground for untyped LC during reading TaPL book. |
| 3 | +;; |
| 4 | +;; Note: |
| 5 | +;; Since we don't have carrying in the interpeter we must define |
| 6 | +;; functions which can apply on many arguments as function with only |
| 7 | +;; one argument which returns another function from one argument, and so on. |
| 8 | +;; Furthermore, more verbose declarations of λ-combinators are easier to understand |
| 9 | +;; and read, because it's more like a regular notation for λ calculus. |
| 10 | +;; |
| 11 | +;; Head 4.2 |
| 12 | +;; Programming in the Lambda-Calculus |
| 13 | + |
| 14 | +;;----------------------------------------------------------------------------;; |
| 15 | +;; Head 4.2.1 |
| 16 | +;; Lambda combinators given by the book |
| 17 | +;;----------------------------------------------------------------------------;; |
| 18 | + |
| 19 | +(label tru (lambda (t) |
| 20 | + (lambda (f) |
| 21 | + t))) |
| 22 | + |
| 23 | +(label fls (lambda (t) |
| 24 | + (lambda (f) |
| 25 | + f))) |
| 26 | + |
| 27 | +(label test (lambda (l) |
| 28 | + (lambda (m) |
| 29 | + (lambda (n) |
| 30 | + (l m n))))) |
| 31 | + |
| 32 | +;; Logical AND cases: |
| 33 | +;; ((and tru fls) t f) => f |
| 34 | +;; ((and tru tru) t f) => t |
| 35 | +;; ((and fls tru) t f) => f |
| 36 | +;; ((and fls fls) t f) => f |
| 37 | +(label mand (lambda (b) |
| 38 | + (lambda (c) |
| 39 | + ((b c) fls)))) |
| 40 | + |
| 41 | +;;----------------------------------------------------------------------------;; |
| 42 | +;; Exercises 4.2.1: |
| 43 | +;; Define logical 'or', and 'not' combinators |
| 44 | +;;----------------------------------------------------------------------------;; |
| 45 | + |
| 46 | +;; Logical OR cases: |
| 47 | +;; ((or tru fls) t f) => t |
| 48 | +;; ((or tru tru) t f) => t |
| 49 | +;; ((or fls tru) t f) => t |
| 50 | +;; ((or fls fls) t f) => f |
| 51 | +(label mor (lambda (b) |
| 52 | + (lambda (c) |
| 53 | + ((b tru) c)))) |
| 54 | + |
| 55 | +;; Logical NOT cases: |
| 56 | +;; ((not tru) t f) => f |
| 57 | +;; ((not fls) t f) => t |
| 58 | +(label mnot (lambda (p) |
| 59 | + ((p fls) tru))) |
| 60 | + |
| 61 | +;;----------------------------------------------------------------------------;; |
| 62 | +;; Head 4.2.2 |
| 63 | +;; Pair of values |
| 64 | +;; Church Numerals |
| 65 | +;;----------------------------------------------------------------------------;; |
| 66 | + |
| 67 | +(label mpair (lambda (f) |
| 68 | + (lambda (s) |
| 69 | + (lambda (b) |
| 70 | + ((b f) s))))) |
| 71 | + |
| 72 | +;; (fst ((mpair 1) 2)) => 1 |
| 73 | +(label fst (lambda (p) |
| 74 | + (p tru))) |
| 75 | + |
| 76 | +;; (snd ((mpair 1) 2)) => 2 |
| 77 | +(label snd (lambda (p) |
| 78 | + (p fls))) |
| 79 | + |
| 80 | +;;----------------------------------------------------------------------------;; |
| 81 | +;; Just a several 'constants' |
| 82 | +;; |
| 83 | + |
| 84 | +(label c0 (lambda (s) |
| 85 | + (lambda (z) |
| 86 | + z))) |
| 87 | + |
| 88 | +(label c1 (lambda (s) |
| 89 | + (lambda (z) |
| 90 | + (s z)))) ;; Or you can substitute it with (s ((c0 s) z)) |
| 91 | + |
| 92 | +(label c2 (lambda (s) |
| 93 | + (lambda (z) |
| 94 | + (s (s z))))) ;; same here: (s ((c1 s) z)) |
| 95 | + |
| 96 | +(label c3 (lambda (s) |
| 97 | + (lambda (z) |
| 98 | + (s ((c2 s) z))))) |
| 99 | + |
| 100 | +;; Generally you can do (s ((cN s) z)), so you need only c0 defined which |
| 101 | +;; implies zero. |
| 102 | + |
| 103 | +;;----------------------------------------------------------------------------;; |
| 104 | +;; Exercise 4.2.3 |
| 105 | +;; Define term for calculating the successor of a number |
| 106 | +;;----------------------------------------------------------------------------;; |
| 107 | + |
| 108 | +;; Here we actually add natural numbers to our language, without it |
| 109 | +;; we can't think about Church numerals as a numbers, without it it's just |
| 110 | +;; an abstraction. |
| 111 | + |
| 112 | +;; At first I thought that zero should return function, but then I realized |
| 113 | +;; that here is the place to be breaking of abstraction. |
| 114 | +;; |
| 115 | +;; (label zero (lambda (r) 0)) |
| 116 | +;; |
| 117 | +;; So, zero and succ should operate on natural numbers and nothing else. |
| 118 | +;; It's obvious that with such semantics we can't do something like that (succ c1) => c2 |
| 119 | + |
| 120 | +(label zero 0) |
| 121 | +(label succ (lambda (r) |
| 122 | + (progn |
| 123 | + ;; (display "Ding") |
| 124 | + ;; (newline) |
| 125 | + (+ 1 r)))) |
| 126 | + |
| 127 | +;; Solutions from the book |
| 128 | +;; |
| 129 | +;; (label succ1 (lambda (n) |
| 130 | +;; (lambda (s) |
| 131 | +;; (lambda (z) |
| 132 | +;; (s ((n s) z)))))) |
| 133 | +;; |
| 134 | +;; (label succ2 (lambda (n) |
| 135 | +;; (lambda (s) |
| 136 | +;; (lambda (z) |
| 137 | +;; ((n s) (s z)))))) |
| 138 | +;; |
| 139 | +;; ;; Actually, this was the first solution that I've figured out |
| 140 | +;; (label succ3 (lambda (n) |
| 141 | +;; ((plus c1) n))) |
| 142 | +;; |
| 143 | + |
| 144 | + |
| 145 | +;;----------------------------------------------------------------------------;; |
| 146 | +;; Mind blowning staff starts here |
| 147 | +;; |
| 148 | + |
| 149 | +(label plus (lambda (m) |
| 150 | + (lambda (n) |
| 151 | + (lambda (s) |
| 152 | + (lambda (z) |
| 153 | + ((m s) ((n s) z))))))) |
| 154 | + |
| 155 | +;; Synonym for multiplication |
| 156 | +(label times (lambda (m) |
| 157 | + (lambda (n) |
| 158 | + ((m (plus n)) c0)))) |
| 159 | + |
| 160 | +;;----------------------------------------------------------------------------;; |
| 161 | +;; Exercise 4.2.4 |
| 162 | +;; Define power combinator |
| 163 | +;;----------------------------------------------------------------------------;; |
| 164 | +(label pow (lambda (m) |
| 165 | + (lambda (n) |
| 166 | + ((n (times m)) c1)))) |
| 167 | + |
| 168 | +;;----------------------------------------------------------------------------;; |
| 169 | +;; The madness continues... |
| 170 | +;; |
| 171 | + |
| 172 | +;; (((iszro c1) t) nil) => nil |
| 173 | +;; (((iszro c0) t) nil) => t |
| 174 | +(label iszro (lambda (m) |
| 175 | + ((m (lambda (x) fls)) tru))) |
| 176 | + |
| 177 | +;; What the hack is going on here? Let's look closer. |
| 178 | +;; |
| 179 | +;; Here we again have a broken abstraction. We need prd that can |
| 180 | +;; work directly with natural numbers as well as it does the succ combinator, |
| 181 | +;; but book gives us these declarations. |
| 182 | +(label zz ((mpair c0) c0)) |
| 183 | +(label ss (lambda (p) |
| 184 | + ((mpair (snd p)) ((plus c1) (snd p))))) |
| 185 | +(label prd (lambda (m) |
| 186 | + (fst ((m ss) zz)))) |
0 commit comments