tweak lists_and_numbers
[lambda.git] / lists_and_numbers.mdwn
1 Building Lists
2 ==============
3
4 To build a data-structure, you begin by deciding what the data-structure needs to do. When we built booleans, what they needed to do was select between two choices. When we built ordered pairs, what we needed was a way to wrap two elements into the pair, and ways to operate on the wrapped elements, especially a way to extract a specified one of them.
5
6 Now we're going to try to build lists. First, let's explain what is the difference bwteen a list and a pair.
7
8 A list can two elements, but it can also have more elements, or fewer. A list can even have zero elements: this is called the empty list. Sometimes this is written `nil`. In Scheme it's also written `'()` and `(list)`, and in OCaml it's written `[]`. Those languages are nice and have list structures pre-built into them. But we're going to build lists ourselves, from scratch.
9
10 OK, so a list doesn't have to have two elements, but still, what's the difference between a two-element list and a pair? And the difference between a three-element list and a triple?
11
12 The difference has to do with types. In the untyped lambda calculus we don't explicitly refer to or manipulate types, however even here we'll need to pay attention to which types of arguments we're giving to which functions. For instance, if you wrote:
13
14         and get-third-of-triple make-pair
15
16 This would evaluate to something, but it's not immediately obvious what it would be, and it's not likely to be especially useful. Even in the untyped lambda calculus, if we want computations that are easy to work with and reason about, we're going to want to pay some attention to the types we're treating formulas to have. For example, we're only going to want to pass formulas that represent boolean values as arguments to `and`. The computation may well terminate even when we don't. But the result won't be one we're in a position to make any good use of.
17
18 Moreover, lists and pairs (and triples, and so on), are data structures we'll find in many typed languages as well. Thinking about types is the way to understand what makes these data structures different.
19
20 The differences are:
21
22 *       A list is type-homegeneous, that is, all its elements must be (or be treatable as being) of the same type.
23
24 *       Not so a pair: its elements need not be of the same type.
25
26 We regard two pairs as being of the same type when their corresponding members are of the same type.
27
28 Another difference between lists and pairs:
29
30 *       The length of a list is not essential to its type. A two-element list can be of the same type as a three-element list (whose members are of the right type).
31
32 *       Not so a pair: no pair is of the same type as any triple, no matter what the types of their elements.
33
34 Q: Sometimes mathematicians <em>identify</em> the triple (1,2,3) with the pair (1,(2,3)), whose first member is 1 and whose second member is the pair (2,3). Wouldn't then a triple have the same type as pair, namely the pair it's identical to?
35
36 A: This is not an identity but an implementation. The claim that the triple (1,2,3) is not the same type as any pair is akin to the claim that the integer 1 is not the same type as any set. It allows you to go on and build set-theoretic constructions whose structure matches the desired behavior of the integers, and so is a reasonable implementation of them. This is exactly what we did when building higher-order functions to implement pairs, in the first place.
37
38 It is true, there are interesting and difficult questions here in the philosophical foundations of mathematics. But I hope we can proceed nonetheless.
39
40
41 Version 1
42 ---------
43
44 OK, then, what sort of behavior do we want out of lists?
45
46 Well we need something to serve as the empty list. And we need a way to take an arbitrary object `hd`, and a list (possibly the empty list) `tl`, and return the list whose **head** is `hd` and whose **tail** is `tl`. And we need a way to tell, of an arbitrary list, whether it's the empty list. And we need a way to extract, from a non-empty list, that list's head and its tail. That's it. Given these basic operations, we should be able to do whatever else we want to do with lists: count their length, reverse them, or whatever. We'll explore how to do those more complex operations in the assignment.
47
48 It's natural to help ourselves to pairs as bricks to use in constructing lists. The way we described building a new list out of a head `hd` and a tail `tl`, for instance, sounds a lot like building a new pair `(hd, tl)`. But we also have to think about what the empty list will be---and more importantly, how to tell the empty list apart from other lists.
49
50 We'll work through a couple of different ways to do this. They'll get more principled as we proceed.
51
52 First, one way to handle the issue of "Is this the empty list or not?" is to have every list contain a boolean flag set to `true` if it's the empty list, and `false` if it isn't. Perhaps the lists could be, not pairs, but triples. The conventional implementation of this idea makes them instead a pair whose first member is the boolean flag, and whose second member, when the list is non-empty, is the list's head and tail. So a (non-empty) list whose head is `hd` and whose tail is `tl` would be represented by:
53
54         (false, (hd, tl))
55
56 What about the empty list? Well we know it will be:
57
58         (true, N)
59
60 for some `N`. What should stand in for `N`?
61
62 No particular choice seems forced here. One strategy would be to go ahead and build your family of list operations, and see whether any particular choice for `N` made some of the other operations easier to define, or more elegant. Heres's an example. We shouldn't expect the result of extracting the head of the empty list to be meaningful. But what about the result of extracting its tail? You could argue that this operation should also be meaningless. Or you could argue that the empty list should be its own tail. If we went the latter way, it would be nice to let `N` in our construction of the empty list be some value, such that, when we tried to extract the empty list's tail in the same way we try to extract other lists' tails, we got back the empty list itself. And in fact it's possible to do this. (However, it requires a fixed-point combinator, which we won't discuss until next week.)
63
64 <!--
65 would be nice if nil tail = nil
66         nil tail = (t, N) get-second get-second = N get-second
67         so N get-second should be (t,N)
68         e.g. N = K (t,N)
69                    = (\n. K (t,n)) N
70         How to do that?
71         a fixed point g_ of g : g_ = (g g_)
72         (Y g) = g (Y g)
73         N = (\n. K (t,n)) N is of the form N = g N
74         So if we just set N = Y g, we'll have what we want. N = (Y g) = g (Y g) = g N
75         
76         i.e. N = Y g = Y (\n. K (t,n))
77         and nil = (t, N) = (t, Y (\n. K (t, n)))
78
79         nil get-second get-second ~~>
80                 Y (\n. K (t, n)) get-second     ~~>
81                 (\n. K (t, n)) (Y (\n. K (t,n))) get-second ~~>
82                 K (t, Y (\n. K (t,n))) get-second ~~>
83                 (t, Y (\n. K (t,n)))
84 -->
85
86 For the time being, though, let's not worry about what stands in for `N` in our construction of the empty list. What should our other primitive list operations look like?
87
88 Well, building a list from a new element `hd` and an existing list `tl` isn't hard: we just build a pair whose first value is false and whose second value is a pair of `hd` and `tl`:
89
90         make-pair false (make-pair hd tl)
91
92 Determining whether a list is the empty list is just a matter of extracting the first element of the (outer) pair:
93
94         some-list get-first
95
96 Given a non-empty list, extracting its head is just a matter of extracting the pair that is its second element, and extracting the first element of that pair:
97
98         some-non-empty-list get-second get-first
99
100 and so on.
101
102
103 Version 2
104 ---------
105
106 OK, version 1 works. But it might look ad hoc. Plus there's that matter of the `N` in the construction of the empty list that we don't know what should be.
107
108 If we do things just a bit differently, it will be easier to see some systematic rationale for them.
109
110 We've already seen some **enumerations**, These are data-structures that consist of several discrete values: such as true and false, or black and white, or red and green and blue. (Sometimes these groups are understood to have an order, but that's not important for our purposes.)
111
112 We've already seen how to build up data structures like this. For instance, red could be:
113
114         \rd gn bl. rd
115
116 that is a function that waits to be supplied with three choices: the "if-you-are-red" choice, the "if-you-are-blue" choice, and the "if-you-are-green" choice, and then yields the "if-you-are-red" choice.
117
118 Now what if we wanted one of the enumerated possibilities to be associated with some further parameter. For instance, we wanted a structure that represented things as being (just) blue, or (just) green, or as *having some specific degree* of redness. How could we do that?
119
120 We might do it by adopting the convention that the "if-you-are-red" selection be not just an arbitrary value, but specifically a function that expected to be supplied with the degree of redness we're dealing with.
121
122 In other words, given an member `colored` of this new data structure, we'd use it like this:
123
124         colored (\deg. colored-is-red-to-degree-deg)  colored-is-instead-green colored-is-instead-blue
125
126 and then if `colored` had the blue value from our data structure, this would evaluate to `colored-is-instead-blue`. If `colored` had a red-to-degree-deg value, it would evaluate to the result of supplying the relevant degree `deg` to the function `(\deg. colored-is-red-to-degree-deg)`.
127
128 To build a value of red-to-degree-deg, we'd replace our original:
129
130         \rd gn bl. rd
131
132 with:
133
134         \rd gn bl. rd deg
135
136 Understand?
137
138 If so, then you should be able to understand the underlying rationale of a list. We've just considered a data-structure that models an exclusive choice from among being-red-to-a-given-degree, just being green, or just being blue. Eliminate the blue choice. And let's associate a second parameter with being red, so that we have being-red-to-a-given-degree-and-illuminated-to-a-different-degree. Our red value would then look like this:
139
140         \rd gn. rd deg illum
141
142 And our green value would look like this:
143
144         \rd gn. gn
145
146 Why are we talking about this? Can you anticipate?
147
148 Answer: For "green", substitute "empty list". For "red", substitute "non-empty list". For "degree-of-redness", substitute "head of the non-empty list." for "degree-of-illumination," substitute "tail of the non-eempty list." And voil&agrave;!
149
150 Spelling it out explicitly, we say:
151
152 >       **nil** is defined to be `\if-non-empty if-empty. if-empty`
153
154 >       **make-list** is defined to be `\hd tl. \if-non-empty if-empty. if-non-empty hd tl`
155
156 Defining **isnil** and the head- and tail- extractors takes some more thought. When operating with any list implemented as we're proposing, we have to pass the list an "if-you're-non-empty" handler and a "if-you're-empty handler." If the list is non-empty, this will evaluate to the result of supplying the list's head and tail as arguments to the handler. If the list is empty, it will instead give us back the empty-handler, unprocessed.
157
158 So to check whether the list is empty, we could pass it an empty-handler of `true`, and a non-empty handler which accepts a head and tail argument, and then just returns the constant false:
159
160         some-list (\hd tl. false) true
161
162 What about extracting the head of a list? It only makes sense to do this when the list is known to be non-empty. In that case, the empty-handler can be anything since we know it's going to be discarded. We'll designate this dummy handler `H`. On the other hand, it's easy to see what our non-empty handler should be:
163
164         some-list (\hd tl. hd) H
165
166 Similarly for extracting the tail of a list.
167
168 When we get to discussing types, you'll see that the strategy deployed here has great generality. (Moreover, you can see the version 1 strategy as an approximate implementation of it.)
169
170
171 There are other reasonable choices you could make for how to implement lists. We'll come back later and discuss a third. If you're creative, you'll be able to design more yourself. The hard part is making the design principled and minimizing extraneous cruft, like the `N` and the `H` in our above discussion.
172
173
174 Building Numbers
175 ================
176
177 Now how might we go about building numbers? We'll just try to build the natural numbers: 0, 1, 2, ...
178
179 If you think about lists and numbers, you should start to see some interesting similarities between them. In each case there's a base value (the empty list, 0). And then further values are always the result of some operation (appending a new head to, taking the successor of) on an existing value.
180
181 Because of this underlying similarity, we could in fact use either of the strategies described above to implement numbers.
182
183 Following the version 1 strategy for lists, we could let 0 be:
184
185         (true, Z)
186
187 for some useful---or, if need be, arbitrary---value `Z`. And given a number `n`, we could let the successor of `n` be:
188
189         (false, n)
190
191 Given this implementation of the numbers, it would be an easy matter to determine whether a given number was zero. (How would you do it?) And it would also be an easy matter to determine the predecessor of any number that wasn't zero. (How would you do it?) Other arithmetic operations, however, would be more complicated. We haven't yet learned the tools that would be needed to determine whether two numbers were equal, or to add two numbers.
192
193 Following the version 2 strategy for lists, we could adopt the convention that we'd operate on numbers by passing them an "if-you're-non-zero" handler and a "if-you're-zero" handler. If the number is non-zero, it will evaluate to the result of supplying the number's predecessor as an argument to the handler. If the number is zero, it will instead give us back the zero handler, unprocessed.
194
195 With that convention, we could let 0 be:
196
197         \if-non-zero if-zero. if-zero
198
199 and we could let the successor function be:
200
201         \n. \if-non-zero if-zero. if-non-zero n
202
203 This is a more principled implementation, and would again make some arithmetic operations easy to implement. But as before, others would be more difficult.
204
205
206 Composition
207 ===========
208
209 We're going now to describe a third strategy, which goes in a different direction.
210
211 The **composition** of two functions is the operation that first applies one of them, and then applies the second. For instance, the arithmetic operation that maps a real number *r* to *r<sup>2</sup>+1* is the composition of the squaring function and the successor function. This complex function is standardly written:
212
213 <pre><code>successor &#8728; square</code></pre> 
214
215 and in general:
216
217 <pre><code>(s &#8728; f) z</code></pre>
218
219 should be understood as:
220
221         s (f z)
222
223 Now consider the following series:
224
225         z
226         s z
227         s (s z)
228         s (s (s z))
229         ...
230
231 Remembering that I is the identity combinator, this could also be written:
232
233 <pre><code>(I) z
234 (s) z
235 (s &#8728; s) z
236 (s &#8728; s &#8728; s) z
237 ...</code></pre>
238
239 And we might adopt the following natural shorthand for this:
240
241 <pre><code>s<sup>0</sup> z
242 s<sup>1</sup> z
243 s<sup>2</sup> z
244 s<sup>3</sup> z
245 ...</code></pre>
246
247 We haven't introduced any new constants 0, 1, 2 into the object language, nor any new form of syntactic combination. This is all just a metalanguage abbreviation for:
248
249         z
250         s z
251         s (s z)
252         s (s (s z))
253         ...
254
255 Church had the idea to implement the number *n* by an operation that accepted an arbitrary function `s` and base value `z` as arguments, and returned <code>s<sup><em>n</em></sup> z</code> as a result. In other words:
256
257 <pre><code>zero &equiv; \s z. s<sup>0</sup> z &equiv; \s z. z
258 one &equiv; \s z. s<sup>1</sup> z &equiv; \s z. s z
259 two &equiv; \s z. s<sup>2</sup> z &equiv; \s z. s (s z)
260 three &equiv; \s z. s<sup>3</sup> z &equiv; \s z. s (s (s z))
261 ...</code></pre>
262
263 This is a very elegant idea. Implementing numbers this way, we'd let the successor function be:
264
265 <pre><code>succ &equiv; \n. \s z. s (n s z)</code></pre>
266
267 So, for example:
268
269 <pre><code>    succ two
270   &equiv; (\n. \s z. s (n s z)) (\s z. s (s z))
271 ~~> \s z. s ((\s z, s (s z)) s z)
272 ~~> \s z. s (s (s z))</code></pre> 
273
274 Adding *m* to *n* is a matter of applying the successor function to *n* *m* times. And we know how to apply an arbitrary function s to *n* *m* times: we just give that function s, and the base-value *n*, to *m* as arguments. Because that's what the function we're using to implement *m* *does*. Hence **add** can be defined to be, simply:
275
276         \m \n. m succ n
277
278 Isn't that nice?
279
280 How would we tell whether a number was 0? Well, look again at the implementations of the first few numbers:
281
282 <pre><code>zero &equiv; \s z. s<sup>0</sup> z &equiv; \s z. z
283 one &equiv; \s z. s<sup>1</sup> z &equiv; \s z. s z
284 two &equiv; \s z. s<sup>2</sup> z &equiv; \s z. s (s z)
285 three &equiv; \s z. s<sup>3</sup> z &equiv; \s z. s (s (s z))
286 ...</code></pre>
287
288 We can see that with the non-zero numbers, the function s is always applied to an argument at least once. With zero, on the other hand, we just get back the base-value. Hence we can determine whether a number is zero as follows:
289
290         some-number (\x. false) true
291
292 If some-number is zero, this will evaluate to the base value true. If some-number is non-zero, then it will evaluate to the result of applying (\x. false) to the result of applying ... to the result of applying (\x. false) to the base value true. But the result of applying (\x. false) to any argument is always false. So when some-number is non-zero, this expressions evaluates to false.
293
294 Perhaps not as elegant as addition, but still decently principled.
295
296 Multiplication is even more elegant. Consider that applying an arbitrary function s to a base value z *m &times; n* times is a matter of applying s to z *n* times, and then doing that again, and again, and so on...for *m* repetitions. In other words, it's a matter of applying the function (\z. n s z) to z *m* times. In other words, *m &times; n* can be represented as:
297
298         &nbsp;   \s z. m (\z. n s z) z
299         ~~> \s z. m n s z
300
301 which eta-reduces to:
302
303         m n
304
305 Isn't that nice?
306
307 However, at this point the elegance gives out. The predecessor function is substantially more difficult to construct on this implementation. As with all of these operations, there are several ways to do it, but they all take at least a bit of ingenuity. If you're only first learning programming right now, it would be unreasonable to expect you to be able to figure out how to do it.
308
309 However, if on the other hand you do have some experience programming, consider how you might construct a predecessor function for numbers implemented in this way. Using only the resources we've so far discussed. (So you have no general facility for performing recursion, for instance.)
310
311
312
313
314
315
316 (list?)
317 nil
318 cons
319 nil?, (pair?)
320 head
321 tail
322
323 Chris's lists:
324         nil = (t,N)  = \f. f true N
325         [a] = (f,(a,nil))
326         [b,a] = (f,(b,[a]))
327
328 isnil = get-first
329 head = L get-second get-first
330 tail = L get-second get-second
331
332
333
334 Lists 2:
335         nil = false
336         [a] = (a,nil)
337
338 L (\h\t.K deal_with_h_and_t) if-nil
339
340 We've already seen enumerations: true | false, red | green | blue
341 What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
342
343 could handle like this:
344         the-value if-red if-green (\n. handler-if-blue-to-degree-n)
345
346         then red = \r \g \b-handler. r
347                  green = \r \g \b-handler. g
348                  make-blue = \degree. \r \g \b-handler. b-handler degree
349
350 A list is basically: empty | non-empty <head,tail>
351
352                 empty = \non-empty-handler \if-empty. if-empty = false
353                 cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
354
355                 so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
356
357
358
359 Lists 3:
360 [a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
361
362 nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
363
364         so M could be \a \b. a, i.e. true
365         so nil = \f. true == K true == K K = \_ K
366
367         nil = K true
368         [a] = (a,nil)
369         [b,a] = (b,[a])
370
371 isnil = (\x\y.false)
372
373 nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
374 nil head = K true head = true. could mislead.
375
376
377
378 Church figured out how to encode integers and arithmetic operations
379 using lambda terms.  Here are the basics:
380
381 0 = \f\x.fx
382 1 = \f\x.f(fx)
383 2 = \f\x.f(f(fx))
384 3 = \f\x.f(f(f(fx)))
385 ...
386
387 Adding two integers involves applying a special function + such that 
388 (+ 1) 2 = 3.  Here is a term that works for +:
389
390 + = \m\n\f\x.m(f((n f) x))
391
392 So (+ 0) 0 =
393 (((\m\n\f\x.m(f((n f) x))) ;+
394   \f\x.fx)                 ;0
395   \f\x.fx)                 ;0
396
397 ~~>_beta targeting m for beta conversion
398
399 ((\n\f\x.[\f\x.fx](f((n f) x)))
400  \f\x.fx)
401
402 \f\x.[\f\x.fx](f(([\f\x.fx] f) x))
403
404 \f\x.[\f\x.fx](f(fx))
405
406 \f\x.\x.[f(fx)]x
407
408 \f\x.f(fx)
409
410
411
412
413
414
415
416
417
418 let t = <<fun y _ -> y>>
419 let f = <<fun _ n -> n>>
420 let b = <<fun f g x -> f (g x)>>
421 let k = << $t$ >>
422 let get1 = << $t$ >>
423 let get2 = << $f$ >>
424 let id = <<fun x -> x>>
425 let w = <<fun f -> f f>>
426 let w' = <<fun f n -> f f n>>
427 let pair = <<fun x y theta -> theta x y>>
428
429 let zero = <<fun s z -> z>>
430 let succ = <<fun n s z -> s (n s z)>>
431 let one = << $succ$ $zero$ >>
432 let two = << $succ$ $one$ >>
433 let three = << $succ$ $two$ >>
434 let four = << $succ$ $three$ >>
435 let five = << $succ$ $four$ >>
436 let six = << $succ$ $five$ >>
437 let seven = << $succ$ $six$ >>
438 let eight = << $succ$ $seven$ >>
439 let nine = << $succ$ $eight$ >>
440
441 (*
442 let pred = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) $id$ >>
443 *)
444 let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>
445 (* ifzero n withp whenz *)
446 let ifzero = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) (fun n' withp
447 whenz -> withp n') >>
448
449 let pred' =
450     let iszero = << fun n -> n (fun _ -> $f$) $t$ >> in
451     << fun n -> n ( fun f z' -> $iszero$ (f $one$) z' ($succ$ (f z')) ) ($k$ $zero$) $zero$ >>
452
453 (*
454     so n = zero ==> (k zero) zero
455        n = one  ==> f=(k zero) z'=zero  ==> z' i.e. zero
456        n = two  ==> g(g (k zero)) zero
457                     f = g(k zero) z'=zero
458                     f = fun z'->z'  z'=zero  ==> succ (f z') = succ(zero)
459        n = three ==> g(g(g (k zero))) zero
460                      f = g(g(k zero)) z'=zero
461                      f = fun z' -> succ(i z')  z'=zero
462                                              ==> succ (f z') ==> succ(succ(z'))
463 *)
464
465 let pred'' =
466     let shift = (* <n,_> -> <n+1,n> *)
467         <<fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) d1) >> in
468     <<fun n -> n $shift$ ($pair$ $zero$ $zero$) $get2$ >>
469
470
471
472 let add = <<fun m n -> n $succ$ m>>
473 (* let add = <<fun m n -> fun s z -> m s (n s z) >> *)
474 let mul = << fun m n -> n (fun z' -> $add$ m z') $zero$ >>
475
476
477 (* we create a pairs-list of the numbers up to m, and take the
478  * head of the nth tail. the tails are in the form (k tail), with
479  * the tail of mzero being instead (id). We unwrap the content by:
480  *      (k tail) tail_of_mzero
481  * or
482  *      (id) tail_of_mzero
483  * we let tail_of_mzero be the mzero itself, so the nth predecessor of
484  * zero will still be zero.
485  *)
486
487 let sub =
488     let mzero = << $pair$ $zero$ $id$ >> in
489     let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
490     let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
491     <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ >>
492
493 let min' = <<fun m n -> $sub$ m ($sub$ m n) >>
494 let max' = <<fun m n -> $add$ n ($sub$ m n) >>
495
496 let lt' =
497     let mzero = << $pair$ $zero$ $id$ >> in
498     let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
499     let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
500     <<fun n m -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $t$) $f$ >>
501
502 let leq' =
503     let mzero = << $pair$ $zero$ $id$ >> in
504     let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
505     let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
506     <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
507
508 let eq' =
509     (* like leq, but now we make mzero have a self-referential tail *)
510     let mzero = << $pair$ $zero$ ($k$ ($pair$ $one$ $id$))  >> in
511     let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
512     let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
513     <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
514
515 (*
516 let divmod' = << fun n d -> n 
517     (fun f' -> f' (fun d' m' ->
518         $lt'$ ($succ$ m') d ($pair$ d' ($succ$ m')) ($pair$ ($succ$ d') $zero$)
519     ))
520     ($pair$ $zero$ $zero$) >>
521 let div' = <<fun n d -> $divmod'$ n d $get1$ >>
522 let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
523 *)
524
525 let divmod' =
526     let triple = << fun d1 d2 d3 -> fun sel -> sel d1 d2 d3 >> in
527     let mzero = << $triple$ $succ$ ($k$ $zero$) $id$ >> in
528     let msucc = << fun d -> $triple$ $id$ $succ$ ($k$ d) >> in
529     let mtail = (* open in dhead *)
530         << fun d -> d (fun dz mz df mf drest ->
531                fun sel -> (drest dhead) (sel (df dz) (mf mz))) >> in
532     << fun n divisor ->
533         ( fun dhead -> n $mtail$ (fun sel -> dhead (sel $zero$ $zero$)) )
534         (divisor $msucc$ $mzero$ (fun _ _ d3 -> d3 _))
535         (fun dz mz _ _ _ -> $pair$ dz mz) >>
536
537 let div' = <<fun n d -> $divmod'$ n d $get1$ >>
538 let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
539
540 (*
541  ISZERO = lambda n. n (lambda x. false) true,
542
543   LE =  lambda x. lambda y. ISZERO (MONUS x y),
544   { ? x <= y ? }
545
546   MONUS = lambda a. lambda b. b PRED a,
547   {NB. assumes a >= b >= 0}
548
549   DIVMOD = lambda x. lambda y.
550     let rec dm = lambda q. lambda x.
551       if LE y x then {y <= x}
552         dm (SUCC q) (MONUS x y)
553       else pair q x
554     in dm ZERO x,
555 *) 
556
557 (* f n =def. phi n_prev f_prev *)
558 let bernays = <<fun phi z n -> n (fun d -> $pair$ (d (fun n_prev f_prev -> $succ$ n_prev)) (d phi)) ($pair$ $zero$ z) (fun n f -> f)>>
559
560
561 (*
562 let pred_b = << $bernays$ $k$ $zero$ >>
563 let fact_b = << $bernays$ (fun x p -> $mul$ ($succ$ x) p) $one$ >>
564
565 (* if m is zero, returns z; else returns withp (pred m) *)
566 let ifzero = <<fun z withp m -> $bernays$ (fun x p -> withp x) z m>>
567 let ifzero = <<fun z withp m -> m ($k$ (withp ($pred$ m))) z>>
568 *)
569
570 let y = <<fun f -> (fun u -> f (u u)) (fun u -> f (u u))>>
571 (* strict y-combinator from The Little Schemer, Crockford's http://www.crockford.com/javascript/little.html *)
572 let y' = <<fun f -> (fun u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>>
573 (*
574 let y'' = <<fun f -> (fun u n -> f (u u n)) (fun u n -> f (u u n))>>
575 *)
576
577 let turing = <<(fun u f -> f (u u f)) (fun u f -> f (u u f))>>
578 let turing' = <<(fun u f -> f (fun n -> u u f n)) (fun u f -> f (fun n -> u u f n))>>
579
580
581 let fact_w = << $w$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
582 p)) $one$)>>
583 let fact_w' = <<(fun f n -> f f n) (fun f n -> $ifzero$ n (fun p ->
584     $mul$ n (f f p)) $one$)>>
585 let fact_w'' = let u = <<(fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
586 p)) $one$)>> in <<fun n -> $u$ $u$ n>>
587
588 let fact_y = << $y$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
589 let fact_y' = << $y'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
590
591 let fact_turing = << $turing$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
592 let fact_turing' = << $turing'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
593
594
595
596 let zero_ = <<fun s z -> z>>;;
597 let succ_ = <<fun m s z -> s m (m s z)>>;;
598 let one_ = << $succ_$ $zero_$ >>;;
599 let two_ = << $succ_$ $one_$ >>;;
600 let three_ = << $succ_$ $two_$ >>;;
601 let four_ = << $succ_$ $three_$ >>;;
602 let five_ = << $succ_$ $four_$ >>;;
603 let six_ = << $succ_$ $five_$ >>;;
604 let seven_ = << $succ_$ $six_$ >>;;
605 let eight_ = << $succ_$ $seven_$ >>;;
606 let nine_ = << $succ_$ $eight_$ >>;;
607
608 let pred_ = <<fun n -> n (fun n' _ -> n') $zero_$ >>
609 let add_ = <<fun m n -> n (fun _ f' -> $succ_$ f') m>>
610 let mul_ = <<fun m n -> n (fun _ f' -> $add_$ m f') $zero_$ >>
611 (* let pow_ = *)
612
613 let sub_ = <<fun m n -> n (fun _ f' -> $pred_$ f') m>>
614 let min_ = <<fun m n -> $sub_$ m ($sub_$ m n)>>  (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *)
615 let max_ = <<fun m n -> $add_$ n ($sub_$ m n)>>  (* n+max(m-n,0) = max(m,n) *)
616
617 let eq_ = <<fun m -> m (fun _ fm' n -> n (fun n' _ -> fm' n') $f$) (fun n -> n (fun _ _ -> $f$) $t$)>>
618 let lt_ = <<fun m n -> ($sub_$ n m) (fun _ _ -> $t$) $f$ >>
619 let leq_ = << fun m n -> ($sub_$ m n) (fun _ _ -> $f$) $t$ >>
620
621 let divmod_ = << fun n d -> n 
622     (fun _ f' -> f' (fun d' m' ->
623         $lt_$ ($succ_$ m') d ($pair$ d' ($succ_$ m')) ($pair$ ($succ_$ d') $zero_$)
624     ))
625     ($pair$ $zero_$ $zero_$) >>
626 let div_ = <<fun n d -> $divmod_$ n d $get1$ >>
627 let mod_ = <<fun n d -> $divmod_$ n d $get2$ >>
628