eval order CL
[lambda.git] / topics / _week7_eval_cl.mdwn
1 <!-- λ Λ ∀ ≡ α β ω Ω -->
2
3 [[!toc levels=2]]
4
5 # Reasoning about evaluation order in Combinatory Logic
6
7 We've discussed evaluation order before, primarily in connection with
8 the untyped lambda calculus.  Whenever a term has more than one redex,
9 we have to choose which one to reduce, and this choice can make a
10 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
11 leftmost redex first, the term reduces to the normal form `I` in one
12 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
13 we do not arrive at a normal form, and are in danger of entering an
14 infinite loop.
15
16 Thanks to the introduction of sum types (disjoint union), we are now
17 in a position to gain a deeper understanding by writing a program that
18 allows us to experiment with different evaluation order strategies.
19
20 One thing we'll see is that it is all too easy for the evaluation
21 order properties of an evaluator to depend on the evaluation order
22 properties of the programming language in which the evaluator is
23 written.  We will seek to write an evaluator in which the order of
24 evaluation is insensitive to the evaluator language.  The goal is to
25 find an order-insensitive way to reason about evaluation order.
26
27 The first evaluator we develop will evaluate terms in Combinatory
28 Logic.  That will significantly simplify the program, since we won't
29 need to worry about variables or substitution.  As we develop and
30 extend our evaluator in future weeks, we'll switch to lambdas, but for
31 now, working with the elegant simplicity of Combinatory Logic will
32 make the evaluation order issues easier to grasp.
33
34 A brief review: a term in CL is the combination of three basic
35 expressions, `S`, `K`, and `I`, governed by the following reduction
36 rules:
37
38     Ia ~~> a
39     Kab ~~> b
40     Sabc ~~> ac(bc)
41
42 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
43 that how to embed the untyped lambda calculus in CL, so it's no
44 surprise that the same evaluation order issues arise in CL.
45
46     skomega = SII(SII)
47             ~~> I(SII)(I(SII))
48             ~~> SII(SII)
49
50 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
51 here, though we'll use the same symbol, `Ω`.  If we consider the term
52
53     KIΩ == KI(SII(SII))
54
55 we can choose to reduce the leftmost redex by firing the reduction
56 rule for `K`, in which case the term reduces to the normal form `I` in
57 one step; or we can choose to reduce the skomega part, by firing the
58 reduction rule fo `S`, in which case we do not get a normal form,
59 we're headed towards an infinite loop.
60
61 With sum types, we can define terms in CL in OCaml as follows:
62
63     type term = I | S | K | FA of (term * term)
64
65     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
66     let test1 = FA (FA (K,I), skomega)
67
68 This recursive type definition says that a term in CL is either one of
69 the three simple expressions, or else a pair of CL expressions.
70 Following Heim and Kratzer, `FA` stands for Functional Application.
71 With this type definition, we can encode skomega, as well as other
72 terms whose reduction behavior we want to control.
73
74 Using pattern matching, it is easy to code the one-step reduction
75 rules for CL:
76
77     let reduce_one_step (t:term):term = match t with
78         FA(I,a) -> a
79       | FA(FA(K,a),b) -> a
80       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
81       | _ -> t
82
83     # reduce_one_step (FA(FA(K,S),I));;
84     - : term = S
85     # reduce_one_step skomega;;
86     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
87
88 The need to explicitly insert the type constructor `FA` obscures
89 things a bit, but it's still possible to see how the one-step
90 reduction function is just the reduction rules for CL.  The
91 OCaml interpreter shows us that the function faithfully recognizes
92 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
93
94 We can now say precisely what it means to be a redex in CL.
95
96     let is_redex (t:term):bool = not (t = reduce_one_step t)
97
98     # is_redex K;;
99     - : bool = false
100     # is_redex (FA(K,I));;
101     - : bool = false
102     # is_redex (FA(FA(K,I),S));;
103     - : bool = true
104     # is_redex skomega;;
105     - : book = true
106
107 Warning: this definition relies on the fact that the one-step
108 reduction of a CL term is never identical to the original term.  This
109 would not work for the untyped lambda calculus, since
110 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
111 order to decide whether two terms are equal, OCaml has to recursively
112 compare the elements of complex CL terms.  It is able to figure out
113 how to do this because we provided an explicit definition of the
114 datatype Term.
115
116 As you would expect, a term in CL is in normal form when it contains
117 no redexes.
118
119 In order to fully reduce a term, we need to be able to reduce redexes
120 that are not at the top level of the term.
121
122     (KKI)SI ~~> KSI ~~> S
123
124 That is, we want to be able to first evaluate the redex `KKI` that is
125 a proper subpart of the larger term to produce a new intermediate term
126 that we can then evaluate to the final normal form.
127
128 Because we need to process subparts, and because the result after
129 processing a subpart may require further processing, the recursive
130 structure of our evaluation function has to be quite subtle.  To truly
131 understand it, you will need to do some sophisticated thinking about
132 how recursion works.  We'll show you how to keep track of what is
133 going on by constructing an recursive execution trace of inputs and
134 outputs.
135
136 We'll develop our full reduction function in stages.  Once we have it
137 working, we'll then consider some variants.  Just to be precise, we'll
138 distinguish each microvariant with its own index number embedded in
139 its name.
140
141     let rec reduce1 (t:term):term = 
142       if (is_redex t) then reduce1 (reduce_one_step t)
143                       else t
144
145 If the input is a redex, we ship it off to `reduce_one_step` for
146 processing.  But just in case the result of the one-step reduction is
147 itself a redex, we recursively call `reduce1`.  The recursion will
148 continue until the result is no longer a redex.
149
150     #trace reduce1;;
151     reduce1 is now traced.
152     # reduce1 (FA (I, FA (I, K)));;
153     reduce1 <-- FA (I, FA (I, K))
154       reduce1 <-- FA (I, K)
155         reduce1 <-- K
156         reduce1 --> K
157       reduce1 --> K
158     reduce1 --> K
159     - : term = K
160
161 Since the initial input (`I(IK)`) is a redex, the result after the
162 one-step reduction is `IK`.  We recursively call `reduce1` on this
163 input.  Since `IK` is itself a redex, the result after one-step
164 reduction is `K`.  We recursively call `reduce1` on this input.  Since
165 `K` is not a redex, the recursion bottoms out, and we simply return
166 it.  
167
168 But this function doesn't do enough reduction.
169
170     # reduce1 (FA (FA (I, I), K));;
171     - : term = FA (FA (I, I), K)
172
173 Because the top-level term is not a redex, `reduce1` returns it
174 without any evaluation.  What we want is to evaluate the subparts of a
175 complex term.
176
177     let rec reduce2 (t:term):term = match t with
178         I -> I
179       | K -> K
180       | S -> S
181       | FA (a, b) -> 
182           let t' = FA (reduce2 a, reduce2 b) in
183             if (is_redex t') then reduce2 (reduce_one_step t')
184                              else t'
185
186 Since we need access to the subterms, we do pattern matching on the
187 input term.  If the input is simple, we return it.  If the input is
188 complex, we first process the subexpressions, and only then see if we
189 have a redex.  To understand how this works, follow the trace
190 carefully:
191
192     # reduce2 (FA(FA(I,I),K));;
193     reduce2 <-- FA (FA (I, I), K)
194
195       reduce2 <-- K          ; first main recursive call
196       reduce2 --> K
197
198       reduce2 <-- FA (I, I)  ; second main recursive call
199         reduce2 <-- I
200         reduce2 --> I
201         reduce2 <-- I
202         reduce2 --> I
203       reduce2 <-- I
204
205       reduce2 --> I           ; third main recursive call
206       reduce2 --> I
207
208       reduce2 <-- K           ; fourth
209       reduce2 --> K
210     reduce2 --> K
211     - : term = K
212
213 Ok, there's a lot going on here.  Since the input is complex, the
214 first thing the function does is construct `t'`.  In order to do this,
215 it must reduce the two main subexpressions, `II` and `K`.  But we see
216 from the trace that it begins with the right-hand expression, `K`.  We
217 didn't explicitly tell it to begin with the right-hand subexpression,
218 so control over evaluation order is starting to spin out of our
219 control.  (We'll get it back later, don't worry.)
220
221 In any case, in the second main recursive call, we evaluate `II`.  The
222 result is `I`.  The third main recursive call tests whether this
223 result needs any further processing; it doesn't.  
224
225 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
226 redex, we ship it off to reduce_one_step, getting the term `K` as a
227 result.  The fourth recursive call checks that there is no more
228 reduction work to be done (there isn't), and that's our final result.
229
230 You can see in more detail what is going on by tracing both reduce2
231 and reduce_one_step, but that makes for some long traces.
232
233 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
234 K`, as desired.
235
236 Because the OCaml interpreter evaluates the rightmost expression  
237 in the course of building `t'`, however, it will always evaluate the
238 right hand subexpression, whether it needs to or not.  And sure
239 enough,
240
241     # reduce2 (FA(FA(K,I),skomega));;
242       C-c C-cInterrupted.
243
244 instead of performing the leftmost reduction first, and recognizing 
245 that this term reduces to the normal form `I`, we get lost endlessly
246 trying to reduce skomega.
247
248 To emphasize that our evaluation order here is at the mercy of the
249 evaluation order of OCaml, here is the exact same program translated
250 into Haskell.  We'll put them side by side to emphasize the exact parallel.
251
252 <pre>
253 OCaml                                                          Haskell
254 ==========================================================     =========================================================
255
256 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
257                                                                                                                       
258 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
259                                                                                                                       
260                                                                reduce_one_step :: Term -> Term                                
261 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
262     FA(I,a) -> a                                                 FA I a -> a                                                  
263   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
264   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
265   | _ -> t                                                       _ -> t                                               
266                                                                                                                       
267                                                                is_redex :: Term -> Bool                               
268 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
269                                                                                                                       
270                                                                reduce2 :: Term -> Term                                        
271 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
272     I -> I                                                       I -> I                                               
273   | K -> K                                                       K -> K                                               
274   | S -> S                                                       S -> S                                               
275   | FA (a, b) ->                                                 FA a b ->                                                    
276       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
277         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
278                          else t'                                                      else t'                                
279 </pre>
280
281 There are some differences in the way types are made explicit, and in
282 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
283 Haskell).  But the two programs are essentially identical.
284
285 Yet the Haskell program finds the normal form for KI -->
286
287 [[!toc levels=2]]
288
289 # Reasoning about evaluation order in Combinatory Logic
290
291 We've discussed evaluation order before, primarily in connection with
292 the untyped lambda calculus.  Whenever a term has more than one redex,
293 we have to choose which one to reduce, and this choice can make a
294 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
295 leftmost redex first, the term reduces to the normal form `I` in one
296 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
297 we do not arrive at a normal form, and are in danger of entering an
298 infinite loop.
299
300 Thanks to the introduction of sum types (disjoint union), we are now
301 in a position to gain a deeper understanding by writing a program that
302 allows us to experiment with different evaluation order strategies.
303
304 One thing we'll see is that it is all too easy for the evaluation
305 order properties of an evaluator to depend on the evaluation order
306 properties of the programming language in which the evaluator is
307 written.  We will seek to write an evaluator in which the order of
308 evaluation is insensitive to the evaluator language.  The goal is to
309 find an order-insensitive way to reason about evaluation order.
310
311 The first evaluator we develop will evaluate terms in Combinatory
312 Logic.  That will significantly simplify the program, since we won't
313 need to worry about variables or substitution.  As we develop and
314 extend our evaluator in future weeks, we'll switch to lambdas, but for
315 now, working with the elegant simplicity of Combinatory Logic will
316 make the evaluation order issues easier to grasp.
317
318 A brief review: a term in CL is the combination of three basic
319 expressions, `S`, `K`, and `I`, governed by the following reduction
320 rules:
321
322     Ia ~~> a
323     Kab ~~> b
324     Sabc ~~> ac(bc)
325
326 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
327 that how to embed the untyped lambda calculus in CL, so it's no
328 surprise that the same evaluation order issues arise in CL.
329
330     skomega = SII(SII)
331             ~~> I(SII)(I(SII))
332             ~~> SII(SII)
333
334 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
335 here, though we'll use the same symbol, `Ω`.  If we consider the term
336
337     KIΩ == KI(SII(SII))
338
339 we can choose to reduce the leftmost redex by firing the reduction
340 rule for `K`, in which case the term reduces to the normal form `I` in
341 one step; or we can choose to reduce the skomega part, by firing the
342 reduction rule fo `S`, in which case we do not get a normal form,
343 we're headed towards an infinite loop.
344
345 With sum types, we can define terms in CL in OCaml as follows:
346
347     type term = I | S | K | FA of (term * term)
348
349     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
350     let test1 = FA (FA (K,I), skomega)
351
352 This recursive type definition says that a term in CL is either one of
353 the three simple expressions, or else a pair of CL expressions.
354 Following Heim and Kratzer, `FA` stands for Functional Application.
355 With this type definition, we can encode skomega, as well as other
356 terms whose reduction behavior we want to control.
357
358 Using pattern matching, it is easy to code the one-step reduction
359 rules for CL:
360
361     let reduce_one_step (t:term):term = match t with
362         FA(I,a) -> a
363       | FA(FA(K,a),b) -> a
364       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
365       | _ -> t
366
367     # reduce_one_step (FA(FA(K,S),I));;
368     - : term = S
369     # reduce_one_step skomega;;
370     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
371
372 The need to explicitly insert the type constructor `FA` obscures
373 things a bit, but it's still possible to see how the one-step
374 reduction function is just the reduction rules for CL.  The
375 OCaml interpreter shows us that the function faithfully recognizes
376 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
377
378 We can now say precisely what it means to be a redex in CL.
379
380     let is_redex (t:term):bool = not (t = reduce_one_step t)
381
382     # is_redex K;;
383     - : bool = false
384     # is_redex (FA(K,I));;
385     - : bool = false
386     # is_redex (FA(FA(K,I),S));;
387     - : bool = true
388     # is_redex skomega;;
389     - : book = true
390
391 Warning: this definition relies on the fact that the one-step
392 reduction of a CL term is never identical to the original term.  This
393 would not work for the untyped lambda calculus, since
394 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
395 order to decide whether two terms are equal, OCaml has to recursively
396 compare the elements of complex CL terms.  It is able to figure out
397 how to do this because we provided an explicit definition of the
398 datatype Term.
399
400 As you would expect, a term in CL is in normal form when it contains
401 no redexes.
402
403 In order to fully reduce a term, we need to be able to reduce redexes
404 that are not at the top level of the term.
405
406     (KKI)SI ~~> KSI ~~> S
407
408 That is, we want to be able to first evaluate the redex `KKI` that is
409 a proper subpart of the larger term to produce a new intermediate term
410 that we can then evaluate to the final normal form.
411
412 Because we need to process subparts, and because the result after
413 processing a subpart may require further processing, the recursive
414 structure of our evaluation function has to be quite subtle.  To truly
415 understand it, you will need to do some sophisticated thinking about
416 how recursion works.  We'll show you how to keep track of what is
417 going on by constructing an recursive execution trace of inputs and
418 outputs.
419
420 We'll develop our full reduction function in stages.  Once we have it
421 working, we'll then consider some variants.  Just to be precise, we'll
422 distinguish each microvariant with its own index number embedded in
423 its name.
424
425     let rec reduce1 (t:term):term = 
426       if (is_redex t) then reduce1 (reduce_one_step t)
427                       else t
428
429 If the input is a redex, we ship it off to `reduce_one_step` for
430 processing.  But just in case the result of the one-step reduction is
431 itself a redex, we recursively call `reduce1`.  The recursion will
432 continue until the result is no longer a redex.
433
434     #trace reduce1;;
435     reduce1 is now traced.
436     # reduce1 (FA (I, FA (I, K)));;
437     reduce1 <-- FA (I, FA (I, K))
438       reduce1 <-- FA (I, K)
439         reduce1 <-- K
440         reduce1 --> K
441       reduce1 --> K
442     reduce1 --> K
443     - : term = K
444
445 Since the initial input (`I(IK)`) is a redex, the result after the
446 one-step reduction is `IK`.  We recursively call `reduce1` on this
447 input.  Since `IK` is itself a redex, the result after one-step
448 reduction is `K`.  We recursively call `reduce1` on this input.  Since
449 `K` is not a redex, the recursion bottoms out, and we simply return
450 it.  
451
452 But this function doesn't do enough reduction.
453
454     # reduce1 (FA (FA (I, I), K));;
455     - : term = FA (FA (I, I), K)
456
457 Because the top-level term is not a redex, `reduce1` returns it
458 without any evaluation.  What we want is to evaluate the subparts of a
459 complex term.
460
461     let rec reduce2 (t:term):term = match t with
462         I -> I
463       | K -> K
464       | S -> S
465       | FA (a, b) -> 
466           let t' = FA (reduce2 a, reduce2 b) in
467             if (is_redex t') then reduce2 (reduce_one_step t')
468                              else t'
469
470 Since we need access to the subterms, we do pattern matching on the
471 input term.  If the input is simple, we return it.  If the input is
472 complex, we first process the subexpressions, and only then see if we
473 have a redex.  To understand how this works, follow the trace
474 carefully:
475
476     # reduce2 (FA(FA(I,I),K));;
477     reduce2 <-- FA (FA (I, I), K)
478
479       reduce2 <-- K          ; first main recursive call
480       reduce2 --> K
481
482       reduce2 <-- FA (I, I)  ; second main recursive call
483         reduce2 <-- I
484         reduce2 --> I
485         reduce2 <-- I
486         reduce2 --> I
487       reduce2 <-- I
488
489       reduce2 --> I           ; third main recursive call
490       reduce2 --> I
491
492       reduce2 <-- K           ; fourth
493       reduce2 --> K
494     reduce2 --> K
495     - : term = K
496
497 Ok, there's a lot going on here.  Since the input is complex, the
498 first thing the function does is construct `t'`.  In order to do this,
499 it must reduce the two main subexpressions, `II` and `K`.  But we see
500 from the trace that it begins with the right-hand expression, `K`.  We
501 didn't explicitly tell it to begin with the right-hand subexpression,
502 so control over evaluation order is starting to spin out of our
503 control.  (We'll get it back later, don't worry.)
504
505 In any case, in the second main recursive call, we evaluate `II`.  The
506 result is `I`.  The third main recursive call tests whether this
507 result needs any further processing; it doesn't.  
508
509 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
510 redex, we ship it off to reduce_one_step, getting the term `K` as a
511 result.  The fourth recursive call checks that there is no more
512 reduction work to be done (there isn't), and that's our final result.
513
514 You can see in more detail what is going on by tracing both reduce2
515 and reduce_one_step, but that makes for some long traces.
516
517 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
518 K`, as desired.
519
520 Because the OCaml interpreter evaluates the rightmost expression  
521 in the course of building `t'`, however, it will always evaluate the
522 right hand subexpression, whether it needs to or not.  And sure
523 enough,
524
525     # reduce2 (FA(FA(K,I),skomega));;
526       C-c C-cInterrupted.
527
528 instead of performing the leftmost reduction first, and recognizing 
529 that this term reduces to the normal form `I`, we get lost endlessly
530 trying to reduce skomega.
531
532 To emphasize that our evaluation order here is at the mercy of the
533 evaluation order of OCaml, here is the exact same program translated
534 into Haskell.  We'll put them side by side to emphasize the exact parallel.
535
536 <pre>
537 OCaml                                                          Haskell
538 ==========================================================     =========================================================
539
540 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
541                                                                                                                       
542 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
543                                                                                                                       
544                                                                reduce_one_step :: Term -> Term                                
545 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
546     FA(I,a) -> a                                                 FA I a -> a                                                  
547   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
548   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
549   | _ -> t                                                       _ -> t                                               
550                                                                                                                       
551                                                                is_redex :: Term -> Bool                               
552 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
553                                                                                                                       
554                                                                reduce2 :: Term -> Term                                        
555 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
556     I -> I                                                       I -> I                                               
557   | K -> K                                                       K -> K                                               
558   | S -> S                                                       S -> S                                               
559   | FA (a, b) ->                                                 FA a b ->                                                    
560       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
561         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
562                          else t'                                                      else t'                                
563 </pre>
564
565 There are some differences in the way types are made explicit, and in
566 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
567 Haskell).  But the two programs are essentially identical.
568
569 Yet the Haskell program finds the normal form for KI -->
570
571 [[!toc levels=2]]
572
573 # Reasoning about evaluation order in Combinatory Logic
574
575 We've discussed evaluation order before, primarily in connection with
576 the untyped lambda calculus.  Whenever a term has more than one redex,
577 we have to choose which one to reduce, and this choice can make a
578 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
579 leftmost redex first, the term reduces to the normal form `I` in one
580 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
581 we do not arrive at a normal form, and are in danger of entering an
582 infinite loop.
583
584 Thanks to the introduction of sum types (disjoint union), we are now
585 in a position to gain a deeper understanding by writing a program that
586 allows us to experiment with different evaluation order strategies.
587
588 One thing we'll see is that it is all too easy for the evaluation
589 order properties of an evaluator to depend on the evaluation order
590 properties of the programming language in which the evaluator is
591 written.  We will seek to write an evaluator in which the order of
592 evaluation is insensitive to the evaluator language.  The goal is to
593 find an order-insensitive way to reason about evaluation order.
594
595 The first evaluator we develop will evaluate terms in Combinatory
596 Logic.  That will significantly simplify the program, since we won't
597 need to worry about variables or substitution.  As we develop and
598 extend our evaluator in future weeks, we'll switch to lambdas, but for
599 now, working with the elegant simplicity of Combinatory Logic will
600 make the evaluation order issues easier to grasp.
601
602 A brief review: a term in CL is the combination of three basic
603 expressions, `S`, `K`, and `I`, governed by the following reduction
604 rules:
605
606     Ia ~~> a
607     Kab ~~> b
608     Sabc ~~> ac(bc)
609
610 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
611 that how to embed the untyped lambda calculus in CL, so it's no
612 surprise that the same evaluation order issues arise in CL.
613
614     skomega = SII(SII)
615             ~~> I(SII)(I(SII))
616             ~~> SII(SII)
617
618 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
619 here, though we'll use the same symbol, `Ω`.  If we consider the term
620
621     KIΩ == KI(SII(SII))
622
623 we can choose to reduce the leftmost redex by firing the reduction
624 rule for `K`, in which case the term reduces to the normal form `I` in
625 one step; or we can choose to reduce the skomega part, by firing the
626 reduction rule fo `S`, in which case we do not get a normal form,
627 we're headed towards an infinite loop.
628
629 With sum types, we can define terms in CL in OCaml as follows:
630
631     type term = I | S | K | FA of (term * term)
632
633     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
634     let test1 = FA (FA (K,I), skomega)
635
636 This recursive type definition says that a term in CL is either one of
637 the three simple expressions, or else a pair of CL expressions.
638 Following Heim and Kratzer, `FA` stands for Functional Application.
639 With this type definition, we can encode skomega, as well as other
640 terms whose reduction behavior we want to control.
641
642 Using pattern matching, it is easy to code the one-step reduction
643 rules for CL:
644
645     let reduce_one_step (t:term):term = match t with
646         FA(I,a) -> a
647       | FA(FA(K,a),b) -> a
648       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
649       | _ -> t
650
651     # reduce_one_step (FA(FA(K,S),I));;
652     - : term = S
653     # reduce_one_step skomega;;
654     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
655
656 The need to explicitly insert the type constructor `FA` obscures
657 things a bit, but it's still possible to see how the one-step
658 reduction function is just the reduction rules for CL.  The
659 OCaml interpreter shows us that the function faithfully recognizes
660 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
661
662 We can now say precisely what it means to be a redex in CL.
663
664     let is_redex (t:term):bool = not (t = reduce_one_step t)
665
666     # is_redex K;;
667     - : bool = false
668     # is_redex (FA(K,I));;
669     - : bool = false
670     # is_redex (FA(FA(K,I),S));;
671     - : bool = true
672     # is_redex skomega;;
673     - : book = true
674
675 Warning: this definition relies on the fact that the one-step
676 reduction of a CL term is never identical to the original term.  This
677 would not work for the untyped lambda calculus, since
678 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
679 order to decide whether two terms are equal, OCaml has to recursively
680 compare the elements of complex CL terms.  It is able to figure out
681 how to do this because we provided an explicit definition of the
682 datatype Term.
683
684 As you would expect, a term in CL is in normal form when it contains
685 no redexes.
686
687 In order to fully reduce a term, we need to be able to reduce redexes
688 that are not at the top level of the term.
689
690     (KKI)SI ~~> KSI ~~> S
691
692 That is, we want to be able to first evaluate the redex `KKI` that is
693 a proper subpart of the larger term to produce a new intermediate term
694 that we can then evaluate to the final normal form.
695
696 Because we need to process subparts, and because the result after
697 processing a subpart may require further processing, the recursive
698 structure of our evaluation function has to be quite subtle.  To truly
699 understand it, you will need to do some sophisticated thinking about
700 how recursion works.  We'll show you how to keep track of what is
701 going on by constructing an recursive execution trace of inputs and
702 outputs.
703
704 We'll develop our full reduction function in stages.  Once we have it
705 working, we'll then consider some variants.  Just to be precise, we'll
706 distinguish each microvariant with its own index number embedded in
707 its name.
708
709     let rec reduce1 (t:term):term = 
710       if (is_redex t) then reduce1 (reduce_one_step t)
711                       else t
712
713 If the input is a redex, we ship it off to `reduce_one_step` for
714 processing.  But just in case the result of the one-step reduction is
715 itself a redex, we recursively call `reduce1`.  The recursion will
716 continue until the result is no longer a redex.
717
718     #trace reduce1;;
719     reduce1 is now traced.
720     # reduce1 (FA (I, FA (I, K)));;
721     reduce1 <-- FA (I, FA (I, K))
722       reduce1 <-- FA (I, K)
723         reduce1 <-- K
724         reduce1 --> K
725       reduce1 --> K
726     reduce1 --> K
727     - : term = K
728
729 Since the initial input (`I(IK)`) is a redex, the result after the
730 one-step reduction is `IK`.  We recursively call `reduce1` on this
731 input.  Since `IK` is itself a redex, the result after one-step
732 reduction is `K`.  We recursively call `reduce1` on this input.  Since
733 `K` is not a redex, the recursion bottoms out, and we simply return
734 it.  
735
736 But this function doesn't do enough reduction.
737
738     # reduce1 (FA (FA (I, I), K));;
739     - : term = FA (FA (I, I), K)
740
741 Because the top-level term is not a redex, `reduce1` returns it
742 without any evaluation.  What we want is to evaluate the subparts of a
743 complex term.
744
745     let rec reduce2 (t:term):term = match t with
746         I -> I
747       | K -> K
748       | S -> S
749       | FA (a, b) -> 
750           let t' = FA (reduce2 a, reduce2 b) in
751             if (is_redex t') then reduce2 (reduce_one_step t')
752                              else t'
753
754 Since we need access to the subterms, we do pattern matching on the
755 input term.  If the input is simple, we return it.  If the input is
756 complex, we first process the subexpressions, and only then see if we
757 have a redex.  To understand how this works, follow the trace
758 carefully:
759
760     # reduce2 (FA(FA(I,I),K));;
761     reduce2 <-- FA (FA (I, I), K)
762
763       reduce2 <-- K          ; first main recursive call
764       reduce2 --> K
765
766       reduce2 <-- FA (I, I)  ; second main recursive call
767         reduce2 <-- I
768         reduce2 --> I
769         reduce2 <-- I
770         reduce2 --> I
771       reduce2 <-- I
772
773       reduce2 --> I           ; third main recursive call
774       reduce2 --> I
775
776       reduce2 <-- K           ; fourth
777       reduce2 --> K
778     reduce2 --> K
779     - : term = K
780
781 Ok, there's a lot going on here.  Since the input is complex, the
782 first thing the function does is construct `t'`.  In order to do this,
783 it must reduce the two main subexpressions, `II` and `K`.  But we see
784 from the trace that it begins with the right-hand expression, `K`.  We
785 didn't explicitly tell it to begin with the right-hand subexpression,
786 so control over evaluation order is starting to spin out of our
787 control.  (We'll get it back later, don't worry.)
788
789 In any case, in the second main recursive call, we evaluate `II`.  The
790 result is `I`.  The third main recursive call tests whether this
791 result needs any further processing; it doesn't.  
792
793 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
794 redex, we ship it off to reduce_one_step, getting the term `K` as a
795 result.  The fourth recursive call checks that there is no more
796 reduction work to be done (there isn't), and that's our final result.
797
798 You can see in more detail what is going on by tracing both reduce2
799 and reduce_one_step, but that makes for some long traces.
800
801 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
802 K`, as desired.
803
804 Because the OCaml interpreter evaluates the rightmost expression  
805 in the course of building `t'`, however, it will always evaluate the
806 right hand subexpression, whether it needs to or not.  And sure
807 enough,
808
809     # reduce2 (FA(FA(K,I),skomega));;
810       C-c C-cInterrupted.
811
812 instead of performing the leftmost reduction first, and recognizing 
813 that this term reduces to the normal form `I`, we get lost endlessly
814 trying to reduce skomega.
815
816 To emphasize that our evaluation order here is at the mercy of the
817 evaluation order of OCaml, here is the exact same program translated
818 into Haskell.  We'll put them side by side to emphasize the exact parallel.
819
820 <pre>
821 OCaml                                                          Haskell
822 ==========================================================     =========================================================
823
824 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
825                                                                                                                       
826 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
827                                                                                                                       
828                                                                reduce_one_step :: Term -> Term                                
829 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
830     FA(I,a) -> a                                                 FA I a -> a                                                  
831   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
832   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
833   | _ -> t                                                       _ -> t                                               
834                                                                                                                       
835                                                                is_redex :: Term -> Bool                               
836 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
837                                                                                                                       
838                                                                reduce2 :: Term -> Term                                        
839 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
840     I -> I                                                       I -> I                                               
841   | K -> K                                                       K -> K                                               
842   | S -> S                                                       S -> S                                               
843   | FA (a, b) ->                                                 FA a b ->                                                    
844       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
845         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
846                          else t'                                                      else t'                                
847 </pre>
848
849 There are some differences in the way types are made explicit, and in
850 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
851 Haskell).  But the two programs are essentially identical.
852
853 Yet the Haskell program finds the normal form for KI -->
854
855 [[!toc levels=2]]
856
857 # Reasoning about evaluation order in Combinatory Logic
858
859 We've discussed evaluation order before, primarily in connection with
860 the untyped lambda calculus.  Whenever a term has more than one redex,
861 we have to choose which one to reduce, and this choice can make a
862 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
863 leftmost redex first, the term reduces to the normal form `I` in one
864 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
865 we do not arrive at a normal form, and are in danger of entering an
866 infinite loop.
867
868 Thanks to the introduction of sum types (disjoint union), we are now
869 in a position to gain a deeper understanding by writing a program that
870 allows us to experiment with different evaluation order strategies.
871
872 One thing we'll see is that it is all too easy for the evaluation
873 order properties of an evaluator to depend on the evaluation order
874 properties of the programming language in which the evaluator is
875 written.  We will seek to write an evaluator in which the order of
876 evaluation is insensitive to the evaluator language.  The goal is to
877 find an order-insensitive way to reason about evaluation order.
878
879 The first evaluator we develop will evaluate terms in Combinatory
880 Logic.  That will significantly simplify the program, since we won't
881 need to worry about variables or substitution.  As we develop and
882 extend our evaluator in future weeks, we'll switch to lambdas, but for
883 now, working with the elegant simplicity of Combinatory Logic will
884 make the evaluation order issues easier to grasp.
885
886 A brief review: a term in CL is the combination of three basic
887 expressions, `S`, `K`, and `I`, governed by the following reduction
888 rules:
889
890     Ia ~~> a
891     Kab ~~> b
892     Sabc ~~> ac(bc)
893
894 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
895 that how to embed the untyped lambda calculus in CL, so it's no
896 surprise that the same evaluation order issues arise in CL.
897
898     skomega = SII(SII)
899             ~~> I(SII)(I(SII))
900             ~~> SII(SII)
901
902 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
903 here, though we'll use the same symbol, `Ω`.  If we consider the term
904
905     KIΩ == KI(SII(SII))
906
907 we can choose to reduce the leftmost redex by firing the reduction
908 rule for `K`, in which case the term reduces to the normal form `I` in
909 one step; or we can choose to reduce the skomega part, by firing the
910 reduction rule fo `S`, in which case we do not get a normal form,
911 we're headed towards an infinite loop.
912
913 With sum types, we can define terms in CL in OCaml as follows:
914
915     type term = I | S | K | FA of (term * term)
916
917     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
918     let test1 = FA (FA (K,I), skomega)
919
920 This recursive type definition says that a term in CL is either one of
921 the three simple expressions, or else a pair of CL expressions.
922 Following Heim and Kratzer, `FA` stands for Functional Application.
923 With this type definition, we can encode skomega, as well as other
924 terms whose reduction behavior we want to control.
925
926 Using pattern matching, it is easy to code the one-step reduction
927 rules for CL:
928
929     let reduce_one_step (t:term):term = match t with
930         FA(I,a) -> a
931       | FA(FA(K,a),b) -> a
932       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
933       | _ -> t
934
935     # reduce_one_step (FA(FA(K,S),I));;
936     - : term = S
937     # reduce_one_step skomega;;
938     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
939
940 The need to explicitly insert the type constructor `FA` obscures
941 things a bit, but it's still possible to see how the one-step
942 reduction function is just the reduction rules for CL.  The
943 OCaml interpreter shows us that the function faithfully recognizes
944 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
945
946 We can now say precisely what it means to be a redex in CL.
947
948     let is_redex (t:term):bool = not (t = reduce_one_step t)
949
950     # is_redex K;;
951     - : bool = false
952     # is_redex (FA(K,I));;
953     - : bool = false
954     # is_redex (FA(FA(K,I),S));;
955     - : bool = true
956     # is_redex skomega;;
957     - : book = true
958
959 Warning: this definition relies on the fact that the one-step
960 reduction of a CL term is never identical to the original term.  This
961 would not work for the untyped lambda calculus, since
962 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
963 order to decide whether two terms are equal, OCaml has to recursively
964 compare the elements of complex CL terms.  It is able to figure out
965 how to do this because we provided an explicit definition of the
966 datatype Term.
967
968 As you would expect, a term in CL is in normal form when it contains
969 no redexes.
970
971 In order to fully reduce a term, we need to be able to reduce redexes
972 that are not at the top level of the term.
973
974     (KKI)SI ~~> KSI ~~> S
975
976 That is, we want to be able to first evaluate the redex `KKI` that is
977 a proper subpart of the larger term to produce a new intermediate term
978 that we can then evaluate to the final normal form.
979
980 Because we need to process subparts, and because the result after
981 processing a subpart may require further processing, the recursive
982 structure of our evaluation function has to be quite subtle.  To truly
983 understand it, you will need to do some sophisticated thinking about
984 how recursion works.  We'll show you how to keep track of what is
985 going on by constructing an recursive execution trace of inputs and
986 outputs.
987
988 We'll develop our full reduction function in stages.  Once we have it
989 working, we'll then consider some variants.  Just to be precise, we'll
990 distinguish each microvariant with its own index number embedded in
991 its name.
992
993     let rec reduce1 (t:term):term = 
994       if (is_redex t) then reduce1 (reduce_one_step t)
995                       else t
996
997 If the input is a redex, we ship it off to `reduce_one_step` for
998 processing.  But just in case the result of the one-step reduction is
999 itself a redex, we recursively call `reduce1`.  The recursion will
1000 continue until the result is no longer a redex.
1001
1002     #trace reduce1;;
1003     reduce1 is now traced.
1004     # reduce1 (FA (I, FA (I, K)));;
1005     reduce1 <-- FA (I, FA (I, K))
1006       reduce1 <-- FA (I, K)
1007         reduce1 <-- K
1008         reduce1 --> K
1009       reduce1 --> K
1010     reduce1 --> K
1011     - : term = K
1012
1013 Since the initial input (`I(IK)`) is a redex, the result after the
1014 one-step reduction is `IK`.  We recursively call `reduce1` on this
1015 input.  Since `IK` is itself a redex, the result after one-step
1016 reduction is `K`.  We recursively call `reduce1` on this input.  Since
1017 `K` is not a redex, the recursion bottoms out, and we simply return
1018 it.  
1019
1020 But this function doesn't do enough reduction.
1021
1022     # reduce1 (FA (FA (I, I), K));;
1023     - : term = FA (FA (I, I), K)
1024
1025 Because the top-level term is not a redex, `reduce1` returns it
1026 without any evaluation.  What we want is to evaluate the subparts of a
1027 complex term.
1028
1029     let rec reduce2 (t:term):term = match t with
1030         I -> I
1031       | K -> K
1032       | S -> S
1033       | FA (a, b) -> 
1034           let t' = FA (reduce2 a, reduce2 b) in
1035             if (is_redex t') then reduce2 (reduce_one_step t')
1036                              else t'
1037
1038 Since we need access to the subterms, we do pattern matching on the
1039 input term.  If the input is simple, we return it.  If the input is
1040 complex, we first process the subexpressions, and only then see if we
1041 have a redex.  To understand how this works, follow the trace
1042 carefully:
1043
1044     # reduce2 (FA(FA(I,I),K));;
1045     reduce2 <-- FA (FA (I, I), K)
1046
1047       reduce2 <-- K          ; first main recursive call
1048       reduce2 --> K
1049
1050       reduce2 <-- FA (I, I)  ; second main recursive call
1051         reduce2 <-- I
1052         reduce2 --> I
1053         reduce2 <-- I
1054         reduce2 --> I
1055       reduce2 <-- I
1056
1057       reduce2 --> I           ; third main recursive call
1058       reduce2 --> I
1059
1060       reduce2 <-- K           ; fourth
1061       reduce2 --> K
1062     reduce2 --> K
1063     - : term = K
1064
1065 Ok, there's a lot going on here.  Since the input is complex, the
1066 first thing the function does is construct `t'`.  In order to do this,
1067 it must reduce the two main subexpressions, `II` and `K`.  But we see
1068 from the trace that it begins with the right-hand expression, `K`.  We
1069 didn't explicitly tell it to begin with the right-hand subexpression,
1070 so control over evaluation order is starting to spin out of our
1071 control.  (We'll get it back later, don't worry.)
1072
1073 In any case, in the second main recursive call, we evaluate `II`.  The
1074 result is `I`.  The third main recursive call tests whether this
1075 result needs any further processing; it doesn't.  
1076
1077 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
1078 redex, we ship it off to reduce_one_step, getting the term `K` as a
1079 result.  The fourth recursive call checks that there is no more
1080 reduction work to be done (there isn't), and that's our final result.
1081
1082 You can see in more detail what is going on by tracing both reduce2
1083 and reduce_one_step, but that makes for some long traces.
1084
1085 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
1086 K`, as desired.
1087
1088 Because the OCaml interpreter evaluates the rightmost expression  
1089 in the course of building `t'`, however, it will always evaluate the
1090 right hand subexpression, whether it needs to or not.  And sure
1091 enough,
1092
1093     # reduce2 (FA(FA(K,I),skomega));;
1094       C-c C-cInterrupted.
1095
1096 instead of performing the leftmost reduction first, and recognizing 
1097 that this term reduces to the normal form `I`, we get lost endlessly
1098 trying to reduce skomega.
1099
1100 To emphasize that our evaluation order here is at the mercy of the
1101 evaluation order of OCaml, here is the exact same program translated
1102 into Haskell.  We'll put them side by side to emphasize the exact parallel.
1103
1104 <pre>
1105 OCaml                                                          Haskell
1106 ==========================================================     =========================================================
1107
1108 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
1109                                                                                                                       
1110 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
1111                                                                                                                       
1112                                                                reduce_one_step :: Term -> Term                                
1113 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
1114     FA(I,a) -> a                                                 FA I a -> a                                                  
1115   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
1116   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
1117   | _ -> t                                                       _ -> t                                               
1118                                                                                                                       
1119                                                                is_redex :: Term -> Bool                               
1120 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
1121                                                                                                                       
1122                                                                reduce2 :: Term -> Term                                        
1123 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
1124     I -> I                                                       I -> I                                               
1125   | K -> K                                                       K -> K                                               
1126   | S -> S                                                       S -> S                                               
1127   | FA (a, b) ->                                                 FA a b ->                                                    
1128       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
1129         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
1130                          else t'                                                      else t'                                
1131 </pre>
1132
1133 There are some differences in the way types are made explicit, and in
1134 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
1135 Haskell).  But the two programs are essentially identical.
1136
1137 Yet the Haskell program finds the normal form for KI -->
1138
1139 [[!toc levels=2]]
1140
1141 # Reasoning about evaluation order in Combinatory Logic
1142
1143 We've discussed evaluation order before, primarily in connection with
1144 the untyped lambda calculus.  Whenever a term has more than one redex,
1145 we have to choose which one to reduce, and this choice can make a
1146 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
1147 leftmost redex first, the term reduces to the normal form `I` in one
1148 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
1149 we do not arrive at a normal form, and are in danger of entering an
1150 infinite loop.
1151
1152 Thanks to the introduction of sum types (disjoint union), we are now
1153 in a position to gain a deeper understanding by writing a program that
1154 allows us to experiment with different evaluation order strategies.
1155
1156 One thing we'll see is that it is all too easy for the evaluation
1157 order properties of an evaluator to depend on the evaluation order
1158 properties of the programming language in which the evaluator is
1159 written.  We will seek to write an evaluator in which the order of
1160 evaluation is insensitive to the evaluator language.  The goal is to
1161 find an order-insensitive way to reason about evaluation order.
1162
1163 The first evaluator we develop will evaluate terms in Combinatory
1164 Logic.  That will significantly simplify the program, since we won't
1165 need to worry about variables or substitution.  As we develop and
1166 extend our evaluator in future weeks, we'll switch to lambdas, but for
1167 now, working with the elegant simplicity of Combinatory Logic will
1168 make the evaluation order issues easier to grasp.
1169
1170 A brief review: a term in CL is the combination of three basic
1171 expressions, `S`, `K`, and `I`, governed by the following reduction
1172 rules:
1173
1174     Ia ~~> a
1175     Kab ~~> b
1176     Sabc ~~> ac(bc)
1177
1178 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
1179 that how to embed the untyped lambda calculus in CL, so it's no
1180 surprise that the same evaluation order issues arise in CL.
1181
1182     skomega = SII(SII)
1183             ~~> I(SII)(I(SII))
1184             ~~> SII(SII)
1185
1186 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
1187 here, though we'll use the same symbol, `Ω`.  If we consider the term
1188
1189     KIΩ == KI(SII(SII))
1190
1191 we can choose to reduce the leftmost redex by firing the reduction
1192 rule for `K`, in which case the term reduces to the normal form `I` in
1193 one step; or we can choose to reduce the skomega part, by firing the
1194 reduction rule fo `S`, in which case we do not get a normal form,
1195 we're headed towards an infinite loop.
1196
1197 With sum types, we can define terms in CL in OCaml as follows:
1198
1199     type term = I | S | K | FA of (term * term)
1200
1201     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
1202     let test1 = FA (FA (K,I), skomega)
1203
1204 This recursive type definition says that a term in CL is either one of
1205 the three simple expressions, or else a pair of CL expressions.
1206 Following Heim and Kratzer, `FA` stands for Functional Application.
1207 With this type definition, we can encode skomega, as well as other
1208 terms whose reduction behavior we want to control.
1209
1210 Using pattern matching, it is easy to code the one-step reduction
1211 rules for CL:
1212
1213     let reduce_one_step (t:term):term = match t with
1214         FA(I,a) -> a
1215       | FA(FA(K,a),b) -> a
1216       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
1217       | _ -> t
1218
1219     # reduce_one_step (FA(FA(K,S),I));;
1220     - : term = S
1221     # reduce_one_step skomega;;
1222     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
1223
1224 The need to explicitly insert the type constructor `FA` obscures
1225 things a bit, but it's still possible to see how the one-step
1226 reduction function is just the reduction rules for CL.  The
1227 OCaml interpreter shows us that the function faithfully recognizes
1228 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
1229
1230 We can now say precisely what it means to be a redex in CL.
1231
1232     let is_redex (t:term):bool = not (t = reduce_one_step t)
1233
1234     # is_redex K;;
1235     - : bool = false
1236     # is_redex (FA(K,I));;
1237     - : bool = false
1238     # is_redex (FA(FA(K,I),S));;
1239     - : bool = true
1240     # is_redex skomega;;
1241     - : book = true
1242
1243 Warning: this definition relies on the fact that the one-step
1244 reduction of a CL term is never identical to the original term.  This
1245 would not work for the untyped lambda calculus, since
1246 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
1247 order to decide whether two terms are equal, OCaml has to recursively
1248 compare the elements of complex CL terms.  It is able to figure out
1249 how to do this because we provided an explicit definition of the
1250 datatype Term.
1251
1252 As you would expect, a term in CL is in normal form when it contains
1253 no redexes.
1254
1255 In order to fully reduce a term, we need to be able to reduce redexes
1256 that are not at the top level of the term.
1257
1258     (KKI)SI ~~> KSI ~~> S
1259
1260 That is, we want to be able to first evaluate the redex `KKI` that is
1261 a proper subpart of the larger term to produce a new intermediate term
1262 that we can then evaluate to the final normal form.
1263
1264 Because we need to process subparts, and because the result after
1265 processing a subpart may require further processing, the recursive
1266 structure of our evaluation function has to be quite subtle.  To truly
1267 understand it, you will need to do some sophisticated thinking about
1268 how recursion works.  We'll show you how to keep track of what is
1269 going on by constructing an recursive execution trace of inputs and
1270 outputs.
1271
1272 We'll develop our full reduction function in stages.  Once we have it
1273 working, we'll then consider some variants.  Just to be precise, we'll
1274 distinguish each microvariant with its own index number embedded in
1275 its name.
1276
1277     let rec reduce1 (t:term):term = 
1278       if (is_redex t) then reduce1 (reduce_one_step t)
1279                       else t
1280
1281 If the input is a redex, we ship it off to `reduce_one_step` for
1282 processing.  But just in case the result of the one-step reduction is
1283 itself a redex, we recursively call `reduce1`.  The recursion will
1284 continue until the result is no longer a redex.
1285
1286     #trace reduce1;;
1287     reduce1 is now traced.
1288     # reduce1 (FA (I, FA (I, K)));;
1289     reduce1 <-- FA (I, FA (I, K))
1290       reduce1 <-- FA (I, K)
1291         reduce1 <-- K
1292         reduce1 --> K
1293       reduce1 --> K
1294     reduce1 --> K
1295     - : term = K
1296
1297 Since the initial input (`I(IK)`) is a redex, the result after the
1298 one-step reduction is `IK`.  We recursively call `reduce1` on this
1299 input.  Since `IK` is itself a redex, the result after one-step
1300 reduction is `K`.  We recursively call `reduce1` on this input.  Since
1301 `K` is not a redex, the recursion bottoms out, and we simply return
1302 it.  
1303
1304 But this function doesn't do enough reduction.
1305
1306     # reduce1 (FA (FA (I, I), K));;
1307     - : term = FA (FA (I, I), K)
1308
1309 Because the top-level term is not a redex, `reduce1` returns it
1310 without any evaluation.  What we want is to evaluate the subparts of a
1311 complex term.
1312
1313     let rec reduce2 (t:term):term = match t with
1314         I -> I
1315       | K -> K
1316       | S -> S
1317       | FA (a, b) -> 
1318           let t' = FA (reduce2 a, reduce2 b) in
1319             if (is_redex t') then reduce2 (reduce_one_step t')
1320                              else t'
1321
1322 Since we need access to the subterms, we do pattern matching on the
1323 input term.  If the input is simple, we return it.  If the input is
1324 complex, we first process the subexpressions, and only then see if we
1325 have a redex.  To understand how this works, follow the trace
1326 carefully:
1327
1328     # reduce2 (FA(FA(I,I),K));;
1329     reduce2 <-- FA (FA (I, I), K)
1330
1331       reduce2 <-- K          ; first main recursive call
1332       reduce2 --> K
1333
1334       reduce2 <-- FA (I, I)  ; second main recursive call
1335         reduce2 <-- I
1336         reduce2 --> I
1337         reduce2 <-- I
1338         reduce2 --> I
1339       reduce2 <-- I
1340
1341       reduce2 --> I           ; third main recursive call
1342       reduce2 --> I
1343
1344       reduce2 <-- K           ; fourth
1345       reduce2 --> K
1346     reduce2 --> K
1347     - : term = K
1348
1349 Ok, there's a lot going on here.  Since the input is complex, the
1350 first thing the function does is construct `t'`.  In order to do this,
1351 it must reduce the two main subexpressions, `II` and `K`.  But we see
1352 from the trace that it begins with the right-hand expression, `K`.  We
1353 didn't explicitly tell it to begin with the right-hand subexpression,
1354 so control over evaluation order is starting to spin out of our
1355 control.  (We'll get it back later, don't worry.)
1356
1357 In any case, in the second main recursive call, we evaluate `II`.  The
1358 result is `I`.  The third main recursive call tests whether this
1359 result needs any further processing; it doesn't.  
1360
1361 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
1362 redex, we ship it off to reduce_one_step, getting the term `K` as a
1363 result.  The fourth recursive call checks that there is no more
1364 reduction work to be done (there isn't), and that's our final result.
1365
1366 You can see in more detail what is going on by tracing both reduce2
1367 and reduce_one_step, but that makes for some long traces.
1368
1369 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
1370 K`, as desired.
1371
1372 Because the OCaml interpreter evaluates the rightmost expression  
1373 in the course of building `t'`, however, it will always evaluate the
1374 right hand subexpression, whether it needs to or not.  And sure
1375 enough,
1376
1377     # reduce2 (FA(FA(K,I),skomega));;
1378       C-c C-cInterrupted.
1379
1380 instead of performing the leftmost reduction first, and recognizing 
1381 that this term reduces to the normal form `I`, we get lost endlessly
1382 trying to reduce skomega.
1383
1384 To emphasize that our evaluation order here is at the mercy of the
1385 evaluation order of OCaml, here is the exact same program translated
1386 into Haskell.  We'll put them side by side to emphasize the exact parallel.
1387
1388 <pre>
1389 OCaml                                                          Haskell
1390 ==========================================================     =========================================================
1391
1392 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
1393                                                                                                                       
1394 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
1395                                                                                                                       
1396                                                                reduce_one_step :: Term -> Term                                
1397 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
1398     FA(I,a) -> a                                                 FA I a -> a                                                  
1399   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
1400   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
1401   | _ -> t                                                       _ -> t                                               
1402                                                                                                                       
1403                                                                is_redex :: Term -> Bool                               
1404 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
1405                                                                                                                       
1406                                                                reduce2 :: Term -> Term                                        
1407 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
1408     I -> I                                                       I -> I                                               
1409   | K -> K                                                       K -> K                                               
1410   | S -> S                                                       S -> S                                               
1411   | FA (a, b) ->                                                 FA a b ->                                                    
1412       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
1413         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
1414                          else t'                                                      else t'                                
1415 </pre>
1416
1417 There are some differences in the way types are made explicit, and in
1418 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
1419 Haskell).  But the two programs are essentially identical.
1420
1421 Yet the Haskell program finds the normal form for KI -->
1422
1423 [[!toc levels=2]]
1424
1425 # Reasoning about evaluation order in Combinatory Logic
1426
1427 We've discussed evaluation order before, primarily in connection with
1428 the untyped lambda calculus.  Whenever a term has more than one redex,
1429 we have to choose which one to reduce, and this choice can make a
1430 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
1431 leftmost redex first, the term reduces to the normal form `I` in one
1432 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
1433 we do not arrive at a normal form, and are in danger of entering an
1434 infinite loop.
1435
1436 Thanks to the introduction of sum types (disjoint union), we are now
1437 in a position to gain a deeper understanding by writing a program that
1438 allows us to experiment with different evaluation order strategies.
1439
1440 One thing we'll see is that it is all too easy for the evaluation
1441 order properties of an evaluator to depend on the evaluation order
1442 properties of the programming language in which the evaluator is
1443 written.  We will seek to write an evaluator in which the order of
1444 evaluation is insensitive to the evaluator language.  The goal is to
1445 find an order-insensitive way to reason about evaluation order.
1446
1447 The first evaluator we develop will evaluate terms in Combinatory
1448 Logic.  That will significantly simplify the program, since we won't
1449 need to worry about variables or substitution.  As we develop and
1450 extend our evaluator in future weeks, we'll switch to lambdas, but for
1451 now, working with the elegant simplicity of Combinatory Logic will
1452 make the evaluation order issues easier to grasp.
1453
1454 A brief review: a term in CL is the combination of three basic
1455 expressions, `S`, `K`, and `I`, governed by the following reduction
1456 rules:
1457
1458     Ia ~~> a
1459     Kab ~~> b
1460     Sabc ~~> ac(bc)
1461
1462 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
1463 that how to embed the untyped lambda calculus in CL, so it's no
1464 surprise that the same evaluation order issues arise in CL.
1465
1466     skomega = SII(SII)
1467             ~~> I(SII)(I(SII))
1468             ~~> SII(SII)
1469
1470 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
1471 here, though we'll use the same symbol, `Ω`.  If we consider the term
1472
1473     KIΩ == KI(SII(SII))
1474
1475 we can choose to reduce the leftmost redex by firing the reduction
1476 rule for `K`, in which case the term reduces to the normal form `I` in
1477 one step; or we can choose to reduce the skomega part, by firing the
1478 reduction rule fo `S`, in which case we do not get a normal form,
1479 we're headed towards an infinite loop.
1480
1481 With sum types, we can define terms in CL in OCaml as follows:
1482
1483     type term = I | S | K | FA of (term * term)
1484
1485     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
1486     let test1 = FA (FA (K,I), skomega)
1487
1488 This recursive type definition says that a term in CL is either one of
1489 the three simple expressions, or else a pair of CL expressions.
1490 Following Heim and Kratzer, `FA` stands for Functional Application.
1491 With this type definition, we can encode skomega, as well as other
1492 terms whose reduction behavior we want to control.
1493
1494 Using pattern matching, it is easy to code the one-step reduction
1495 rules for CL:
1496
1497     let reduce_one_step (t:term):term = match t with
1498         FA(I,a) -> a
1499       | FA(FA(K,a),b) -> a
1500       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
1501       | _ -> t
1502
1503     # reduce_one_step (FA(FA(K,S),I));;
1504     - : term = S
1505     # reduce_one_step skomega;;
1506     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
1507
1508 The need to explicitly insert the type constructor `FA` obscures
1509 things a bit, but it's still possible to see how the one-step
1510 reduction function is just the reduction rules for CL.  The
1511 OCaml interpreter shows us that the function faithfully recognizes
1512 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
1513
1514 We can now say precisely what it means to be a redex in CL.
1515
1516     let is_redex (t:term):bool = not (t = reduce_one_step t)
1517
1518     # is_redex K;;
1519     - : bool = false
1520     # is_redex (FA(K,I));;
1521     - : bool = false
1522     # is_redex (FA(FA(K,I),S));;
1523     - : bool = true
1524     # is_redex skomega;;
1525     - : book = true
1526
1527 Warning: this definition relies on the fact that the one-step
1528 reduction of a CL term is never identical to the original term.  This
1529 would not work for the untyped lambda calculus, since
1530 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
1531 order to decide whether two terms are equal, OCaml has to recursively
1532 compare the elements of complex CL terms.  It is able to figure out
1533 how to do this because we provided an explicit definition of the
1534 datatype Term.
1535
1536 As you would expect, a term in CL is in normal form when it contains
1537 no redexes.
1538
1539 In order to fully reduce a term, we need to be able to reduce redexes
1540 that are not at the top level of the term.
1541
1542     (KKI)SI ~~> KSI ~~> S
1543
1544 That is, we want to be able to first evaluate the redex `KKI` that is
1545 a proper subpart of the larger term to produce a new intermediate term
1546 that we can then evaluate to the final normal form.
1547
1548 Because we need to process subparts, and because the result after
1549 processing a subpart may require further processing, the recursive
1550 structure of our evaluation function has to be quite subtle.  To truly
1551 understand it, you will need to do some sophisticated thinking about
1552 how recursion works.  We'll show you how to keep track of what is
1553 going on by constructing an recursive execution trace of inputs and
1554 outputs.
1555
1556 We'll develop our full reduction function in stages.  Once we have it
1557 working, we'll then consider some variants.  Just to be precise, we'll
1558 distinguish each microvariant with its own index number embedded in
1559 its name.
1560
1561     let rec reduce1 (t:term):term = 
1562       if (is_redex t) then reduce1 (reduce_one_step t)
1563                       else t
1564
1565 If the input is a redex, we ship it off to `reduce_one_step` for
1566 processing.  But just in case the result of the one-step reduction is
1567 itself a redex, we recursively call `reduce1`.  The recursion will
1568 continue until the result is no longer a redex.
1569
1570     #trace reduce1;;
1571     reduce1 is now traced.
1572     # reduce1 (FA (I, FA (I, K)));;
1573     reduce1 <-- FA (I, FA (I, K))
1574       reduce1 <-- FA (I, K)
1575         reduce1 <-- K
1576         reduce1 --> K
1577       reduce1 --> K
1578     reduce1 --> K
1579     - : term = K
1580
1581 Since the initial input (`I(IK)`) is a redex, the result after the
1582 one-step reduction is `IK`.  We recursively call `reduce1` on this
1583 input.  Since `IK` is itself a redex, the result after one-step
1584 reduction is `K`.  We recursively call `reduce1` on this input.  Since
1585 `K` is not a redex, the recursion bottoms out, and we simply return
1586 it.  
1587
1588 But this function doesn't do enough reduction.
1589
1590     # reduce1 (FA (FA (I, I), K));;
1591     - : term = FA (FA (I, I), K)
1592
1593 Because the top-level term is not a redex, `reduce1` returns it
1594 without any evaluation.  What we want is to evaluate the subparts of a
1595 complex term.
1596
1597     let rec reduce2 (t:term):term = match t with
1598         I -> I
1599       | K -> K
1600       | S -> S
1601       | FA (a, b) -> 
1602           let t' = FA (reduce2 a, reduce2 b) in
1603             if (is_redex t') then reduce2 (reduce_one_step t')
1604                              else t'
1605
1606 Since we need access to the subterms, we do pattern matching on the
1607 input term.  If the input is simple, we return it.  If the input is
1608 complex, we first process the subexpressions, and only then see if we
1609 have a redex.  To understand how this works, follow the trace
1610 carefully:
1611
1612     # reduce2 (FA(FA(I,I),K));;
1613     reduce2 <-- FA (FA (I, I), K)
1614
1615       reduce2 <-- K          ; first main recursive call
1616       reduce2 --> K
1617
1618       reduce2 <-- FA (I, I)  ; second main recursive call
1619         reduce2 <-- I
1620         reduce2 --> I
1621         reduce2 <-- I
1622         reduce2 --> I
1623       reduce2 <-- I
1624
1625       reduce2 --> I           ; third main recursive call
1626       reduce2 --> I
1627
1628       reduce2 <-- K           ; fourth
1629       reduce2 --> K
1630     reduce2 --> K
1631     - : term = K
1632
1633 Ok, there's a lot going on here.  Since the input is complex, the
1634 first thing the function does is construct `t'`.  In order to do this,
1635 it must reduce the two main subexpressions, `II` and `K`.  But we see
1636 from the trace that it begins with the right-hand expression, `K`.  We
1637 didn't explicitly tell it to begin with the right-hand subexpression,
1638 so control over evaluation order is starting to spin out of our
1639 control.  (We'll get it back later, don't worry.)
1640
1641 In any case, in the second main recursive call, we evaluate `II`.  The
1642 result is `I`.  The third main recursive call tests whether this
1643 result needs any further processing; it doesn't.  
1644
1645 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
1646 redex, we ship it off to reduce_one_step, getting the term `K` as a
1647 result.  The fourth recursive call checks that there is no more
1648 reduction work to be done (there isn't), and that's our final result.
1649
1650 You can see in more detail what is going on by tracing both reduce2
1651 and reduce_one_step, but that makes for some long traces.
1652
1653 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
1654 K`, as desired.
1655
1656 Because the OCaml interpreter evaluates the rightmost expression  
1657 in the course of building `t'`, however, it will always evaluate the
1658 right hand subexpression, whether it needs to or not.  And sure
1659 enough,
1660
1661     # reduce2 (FA(FA(K,I),skomega));;
1662       C-c C-cInterrupted.
1663
1664 instead of performing the leftmost reduction first, and recognizing 
1665 that this term reduces to the normal form `I`, we get lost endlessly
1666 trying to reduce skomega.
1667
1668 To emphasize that our evaluation order here is at the mercy of the
1669 evaluation order of OCaml, here is the exact same program translated
1670 into Haskell.  We'll put them side by side to emphasize the exact parallel.
1671
1672 <pre>
1673 OCaml                                                          Haskell
1674 ==========================================================     =========================================================
1675
1676 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
1677                                                                                                                       
1678 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
1679                                                                                                                       
1680                                                                reduce_one_step :: Term -> Term                                
1681 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
1682     FA(I,a) -> a                                                 FA I a -> a                                                  
1683   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
1684   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
1685   | _ -> t                                                       _ -> t                                               
1686                                                                                                                       
1687                                                                is_redex :: Term -> Bool                               
1688 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
1689                                                                                                                       
1690                                                                reduce2 :: Term -> Term                                        
1691 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
1692     I -> I                                                       I -> I                                               
1693   | K -> K                                                       K -> K                                               
1694   | S -> S                                                       S -> S                                               
1695   | FA (a, b) ->                                                 FA a b ->                                                    
1696       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
1697         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
1698                          else t'                                                      else t'                                
1699 </pre>
1700
1701 There are some differences in the way types are made explicit, and in
1702 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
1703 Haskell).  But the two programs are essentially identical.
1704
1705 Yet the Haskell program finds the normal form for KI -->
1706
1707 [[!toc levels=2]]
1708
1709 # Reasoning about evaluation order in Combinatory Logic
1710
1711 We've discussed evaluation order before, primarily in connection with
1712 the untyped lambda calculus.  Whenever a term has more than one redex,
1713 we have to choose which one to reduce, and this choice can make a
1714 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
1715 leftmost redex first, the term reduces to the normal form `I` in one
1716 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
1717 we do not arrive at a normal form, and are in danger of entering an
1718 infinite loop.
1719
1720 Thanks to the introduction of sum types (disjoint union), we are now
1721 in a position to gain a deeper understanding by writing a program that
1722 allows us to experiment with different evaluation order strategies.
1723
1724 One thing we'll see is that it is all too easy for the evaluation
1725 order properties of an evaluator to depend on the evaluation order
1726 properties of the programming language in which the evaluator is
1727 written.  We will seek to write an evaluator in which the order of
1728 evaluation is insensitive to the evaluator language.  The goal is to
1729 find an order-insensitive way to reason about evaluation order.
1730
1731 The first evaluator we develop will evaluate terms in Combinatory
1732 Logic.  That will significantly simplify the program, since we won't
1733 need to worry about variables or substitution.  As we develop and
1734 extend our evaluator in future weeks, we'll switch to lambdas, but for
1735 now, working with the elegant simplicity of Combinatory Logic will
1736 make the evaluation order issues easier to grasp.
1737
1738 A brief review: a term in CL is the combination of three basic
1739 expressions, `S`, `K`, and `I`, governed by the following reduction
1740 rules:
1741
1742     Ia ~~> a
1743     Kab ~~> b
1744     Sabc ~~> ac(bc)
1745
1746 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
1747 that how to embed the untyped lambda calculus in CL, so it's no
1748 surprise that the same evaluation order issues arise in CL.
1749
1750     skomega = SII(SII)
1751             ~~> I(SII)(I(SII))
1752             ~~> SII(SII)
1753
1754 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
1755 here, though we'll use the same symbol, `Ω`.  If we consider the term
1756
1757     KIΩ == KI(SII(SII))
1758
1759 we can choose to reduce the leftmost redex by firing the reduction
1760 rule for `K`, in which case the term reduces to the normal form `I` in
1761 one step; or we can choose to reduce the skomega part, by firing the
1762 reduction rule fo `S`, in which case we do not get a normal form,
1763 we're headed towards an infinite loop.
1764
1765 With sum types, we can define terms in CL in OCaml as follows:
1766
1767     type term = I | S | K | FA of (term * term)
1768
1769     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
1770     let test1 = FA (FA (K,I), skomega)
1771
1772 This recursive type definition says that a term in CL is either one of
1773 the three simple expressions, or else a pair of CL expressions.
1774 Following Heim and Kratzer, `FA` stands for Functional Application.
1775 With this type definition, we can encode skomega, as well as other
1776 terms whose reduction behavior we want to control.
1777
1778 Using pattern matching, it is easy to code the one-step reduction
1779 rules for CL:
1780
1781     let reduce_one_step (t:term):term = match t with
1782         FA(I,a) -> a
1783       | FA(FA(K,a),b) -> a
1784       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
1785       | _ -> t
1786
1787     # reduce_one_step (FA(FA(K,S),I));;
1788     - : term = S
1789     # reduce_one_step skomega;;
1790     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
1791
1792 The need to explicitly insert the type constructor `FA` obscures
1793 things a bit, but it's still possible to see how the one-step
1794 reduction function is just the reduction rules for CL.  The
1795 OCaml interpreter shows us that the function faithfully recognizes
1796 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
1797
1798 We can now say precisely what it means to be a redex in CL.
1799
1800     let is_redex (t:term):bool = not (t = reduce_one_step t)
1801
1802     # is_redex K;;
1803     - : bool = false
1804     # is_redex (FA(K,I));;
1805     - : bool = false
1806     # is_redex (FA(FA(K,I),S));;
1807     - : bool = true
1808     # is_redex skomega;;
1809     - : book = true
1810
1811 Warning: this definition relies on the fact that the one-step
1812 reduction of a CL term is never identical to the original term.  This
1813 would not work for the untyped lambda calculus, since
1814 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
1815 order to decide whether two terms are equal, OCaml has to recursively
1816 compare the elements of complex CL terms.  It is able to figure out
1817 how to do this because we provided an explicit definition of the
1818 datatype Term.
1819
1820 As you would expect, a term in CL is in normal form when it contains
1821 no redexes.
1822
1823 In order to fully reduce a term, we need to be able to reduce redexes
1824 that are not at the top level of the term.
1825
1826     (KKI)SI ~~> KSI ~~> S
1827
1828 That is, we want to be able to first evaluate the redex `KKI` that is
1829 a proper subpart of the larger term to produce a new intermediate term
1830 that we can then evaluate to the final normal form.
1831
1832 Because we need to process subparts, and because the result after
1833 processing a subpart may require further processing, the recursive
1834 structure of our evaluation function has to be quite subtle.  To truly
1835 understand it, you will need to do some sophisticated thinking about
1836 how recursion works.  We'll show you how to keep track of what is
1837 going on by constructing an recursive execution trace of inputs and
1838 outputs.
1839
1840 We'll develop our full reduction function in stages.  Once we have it
1841 working, we'll then consider some variants.  Just to be precise, we'll
1842 distinguish each microvariant with its own index number embedded in
1843 its name.
1844
1845     let rec reduce1 (t:term):term = 
1846       if (is_redex t) then reduce1 (reduce_one_step t)
1847                       else t
1848
1849 If the input is a redex, we ship it off to `reduce_one_step` for
1850 processing.  But just in case the result of the one-step reduction is
1851 itself a redex, we recursively call `reduce1`.  The recursion will
1852 continue until the result is no longer a redex.
1853
1854     #trace reduce1;;
1855     reduce1 is now traced.
1856     # reduce1 (FA (I, FA (I, K)));;
1857     reduce1 <-- FA (I, FA (I, K))
1858       reduce1 <-- FA (I, K)
1859         reduce1 <-- K
1860         reduce1 --> K
1861       reduce1 --> K
1862     reduce1 --> K
1863     - : term = K
1864
1865 Since the initial input (`I(IK)`) is a redex, the result after the
1866 one-step reduction is `IK`.  We recursively call `reduce1` on this
1867 input.  Since `IK` is itself a redex, the result after one-step
1868 reduction is `K`.  We recursively call `reduce1` on this input.  Since
1869 `K` is not a redex, the recursion bottoms out, and we simply return
1870 it.  
1871
1872 But this function doesn't do enough reduction.
1873
1874     # reduce1 (FA (FA (I, I), K));;
1875     - : term = FA (FA (I, I), K)
1876
1877 Because the top-level term is not a redex, `reduce1` returns it
1878 without any evaluation.  What we want is to evaluate the subparts of a
1879 complex term.
1880
1881     let rec reduce2 (t:term):term = match t with
1882         I -> I
1883       | K -> K
1884       | S -> S
1885       | FA (a, b) -> 
1886           let t' = FA (reduce2 a, reduce2 b) in
1887             if (is_redex t') then reduce2 (reduce_one_step t')
1888                              else t'
1889
1890 Since we need access to the subterms, we do pattern matching on the
1891 input term.  If the input is simple, we return it.  If the input is
1892 complex, we first process the subexpressions, and only then see if we
1893 have a redex.  To understand how this works, follow the trace
1894 carefully:
1895
1896     # reduce2 (FA(FA(I,I),K));;
1897     reduce2 <-- FA (FA (I, I), K)
1898
1899       reduce2 <-- K          ; first main recursive call
1900       reduce2 --> K
1901
1902       reduce2 <-- FA (I, I)  ; second main recursive call
1903         reduce2 <-- I
1904         reduce2 --> I
1905         reduce2 <-- I
1906         reduce2 --> I
1907       reduce2 <-- I
1908
1909       reduce2 --> I           ; third main recursive call
1910       reduce2 --> I
1911
1912       reduce2 <-- K           ; fourth
1913       reduce2 --> K
1914     reduce2 --> K
1915     - : term = K
1916
1917 Ok, there's a lot going on here.  Since the input is complex, the
1918 first thing the function does is construct `t'`.  In order to do this,
1919 it must reduce the two main subexpressions, `II` and `K`.  But we see
1920 from the trace that it begins with the right-hand expression, `K`.  We
1921 didn't explicitly tell it to begin with the right-hand subexpression,
1922 so control over evaluation order is starting to spin out of our
1923 control.  (We'll get it back later, don't worry.)
1924
1925 In any case, in the second main recursive call, we evaluate `II`.  The
1926 result is `I`.  The third main recursive call tests whether this
1927 result needs any further processing; it doesn't.  
1928
1929 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
1930 redex, we ship it off to reduce_one_step, getting the term `K` as a
1931 result.  The fourth recursive call checks that there is no more
1932 reduction work to be done (there isn't), and that's our final result.
1933
1934 You can see in more detail what is going on by tracing both reduce2
1935 and reduce_one_step, but that makes for some long traces.
1936
1937 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
1938 K`, as desired.
1939
1940 Because the OCaml interpreter evaluates the rightmost expression  
1941 in the course of building `t'`, however, it will always evaluate the
1942 right hand subexpression, whether it needs to or not.  And sure
1943 enough,
1944
1945     # reduce2 (FA(FA(K,I),skomega));;
1946       C-c C-cInterrupted.
1947
1948 instead of performing the leftmost reduction first, and recognizing 
1949 that this term reduces to the normal form `I`, we get lost endlessly
1950 trying to reduce skomega.
1951
1952 To emphasize that our evaluation order here is at the mercy of the
1953 evaluation order of OCaml, here is the exact same program translated
1954 into Haskell.  We'll put them side by side to emphasize the exact parallel.
1955
1956 <pre>
1957 OCaml                                                          Haskell
1958 ==========================================================     =========================================================
1959
1960 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
1961                                                                                                                       
1962 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
1963                                                                                                                       
1964                                                                reduce_one_step :: Term -> Term                                
1965 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
1966     FA(I,a) -> a                                                 FA I a -> a                                                  
1967   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
1968   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
1969   | _ -> t                                                       _ -> t                                               
1970                                                                                                                       
1971                                                                is_redex :: Term -> Bool                               
1972 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
1973                                                                                                                       
1974                                                                reduce2 :: Term -> Term                                        
1975 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
1976     I -> I                                                       I -> I                                               
1977   | K -> K                                                       K -> K                                               
1978   | S -> S                                                       S -> S                                               
1979   | FA (a, b) ->                                                 FA a b ->                                                    
1980       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
1981         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
1982                          else t'                                                      else t'                                
1983 </pre>
1984
1985 There are some differences in the way types are made explicit, and in
1986 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
1987 Haskell).  But the two programs are essentially identical.
1988
1989 Yet the Haskell program finds the normal form for KI -->
1990
1991 [[!toc levels=2]]
1992
1993 # Reasoning about evaluation order in Combinatory Logic
1994
1995 We've discussed evaluation order before, primarily in connection with
1996 the untyped lambda calculus.  Whenever a term has more than one redex,
1997 we have to choose which one to reduce, and this choice can make a
1998 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
1999 leftmost redex first, the term reduces to the normal form `I` in one
2000 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
2001 we do not arrive at a normal form, and are in danger of entering an
2002 infinite loop.
2003
2004 Thanks to the introduction of sum types (disjoint union), we are now
2005 in a position to gain a deeper understanding by writing a program that
2006 allows us to experiment with different evaluation order strategies.
2007
2008 One thing we'll see is that it is all too easy for the evaluation
2009 order properties of an evaluator to depend on the evaluation order
2010 properties of the programming language in which the evaluator is
2011 written.  We will seek to write an evaluator in which the order of
2012 evaluation is insensitive to the evaluator language.  The goal is to
2013 find an order-insensitive way to reason about evaluation order.
2014
2015 The first evaluator we develop will evaluate terms in Combinatory
2016 Logic.  That will significantly simplify the program, since we won't
2017 need to worry about variables or substitution.  As we develop and
2018 extend our evaluator in future weeks, we'll switch to lambdas, but for
2019 now, working with the elegant simplicity of Combinatory Logic will
2020 make the evaluation order issues easier to grasp.
2021
2022 A brief review: a term in CL is the combination of three basic
2023 expressions, `S`, `K`, and `I`, governed by the following reduction
2024 rules:
2025
2026     Ia ~~> a
2027     Kab ~~> b
2028     Sabc ~~> ac(bc)
2029
2030 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
2031 that how to embed the untyped lambda calculus in CL, so it's no
2032 surprise that the same evaluation order issues arise in CL.
2033
2034     skomega = SII(SII)
2035             ~~> I(SII)(I(SII))
2036             ~~> SII(SII)
2037
2038 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
2039 here, though we'll use the same symbol, `Ω`.  If we consider the term
2040
2041     KIΩ == KI(SII(SII))
2042
2043 we can choose to reduce the leftmost redex by firing the reduction
2044 rule for `K`, in which case the term reduces to the normal form `I` in
2045 one step; or we can choose to reduce the skomega part, by firing the
2046 reduction rule fo `S`, in which case we do not get a normal form,
2047 we're headed towards an infinite loop.
2048
2049 With sum types, we can define terms in CL in OCaml as follows:
2050
2051     type term = I | S | K | FA of (term * term)
2052
2053     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
2054     let test1 = FA (FA (K,I), skomega)
2055
2056 This recursive type definition says that a term in CL is either one of
2057 the three simple expressions, or else a pair of CL expressions.
2058 Following Heim and Kratzer, `FA` stands for Functional Application.
2059 With this type definition, we can encode skomega, as well as other
2060 terms whose reduction behavior we want to control.
2061
2062 Using pattern matching, it is easy to code the one-step reduction
2063 rules for CL:
2064
2065     let reduce_one_step (t:term):term = match t with
2066         FA(I,a) -> a
2067       | FA(FA(K,a),b) -> a
2068       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
2069       | _ -> t
2070
2071     # reduce_one_step (FA(FA(K,S),I));;
2072     - : term = S
2073     # reduce_one_step skomega;;
2074     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
2075
2076 The need to explicitly insert the type constructor `FA` obscures
2077 things a bit, but it's still possible to see how the one-step
2078 reduction function is just the reduction rules for CL.  The
2079 OCaml interpreter shows us that the function faithfully recognizes
2080 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
2081
2082 We can now say precisely what it means to be a redex in CL.
2083
2084     let is_redex (t:term):bool = not (t = reduce_one_step t)
2085
2086     # is_redex K;;
2087     - : bool = false
2088     # is_redex (FA(K,I));;
2089     - : bool = false
2090     # is_redex (FA(FA(K,I),S));;
2091     - : bool = true
2092     # is_redex skomega;;
2093     - : book = true
2094
2095 Warning: this definition relies on the fact that the one-step
2096 reduction of a CL term is never identical to the original term.  This
2097 would not work for the untyped lambda calculus, since
2098 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
2099 order to decide whether two terms are equal, OCaml has to recursively
2100 compare the elements of complex CL terms.  It is able to figure out
2101 how to do this because we provided an explicit definition of the
2102 datatype Term.
2103
2104 As you would expect, a term in CL is in normal form when it contains
2105 no redexes.
2106
2107 In order to fully reduce a term, we need to be able to reduce redexes
2108 that are not at the top level of the term.
2109
2110     (KKI)SI ~~> KSI ~~> S
2111
2112 That is, we want to be able to first evaluate the redex `KKI` that is
2113 a proper subpart of the larger term to produce a new intermediate term
2114 that we can then evaluate to the final normal form.
2115
2116 Because we need to process subparts, and because the result after
2117 processing a subpart may require further processing, the recursive
2118 structure of our evaluation function has to be quite subtle.  To truly
2119 understand it, you will need to do some sophisticated thinking about
2120 how recursion works.  We'll show you how to keep track of what is
2121 going on by constructing an recursive execution trace of inputs and
2122 outputs.
2123
2124 We'll develop our full reduction function in stages.  Once we have it
2125 working, we'll then consider some variants.  Just to be precise, we'll
2126 distinguish each microvariant with its own index number embedded in
2127 its name.
2128
2129     let rec reduce1 (t:term):term = 
2130       if (is_redex t) then reduce1 (reduce_one_step t)
2131                       else t
2132
2133 If the input is a redex, we ship it off to `reduce_one_step` for
2134 processing.  But just in case the result of the one-step reduction is
2135 itself a redex, we recursively call `reduce1`.  The recursion will
2136 continue until the result is no longer a redex.
2137
2138     #trace reduce1;;
2139     reduce1 is now traced.
2140     # reduce1 (FA (I, FA (I, K)));;
2141     reduce1 <-- FA (I, FA (I, K))
2142       reduce1 <-- FA (I, K)
2143         reduce1 <-- K
2144         reduce1 --> K
2145       reduce1 --> K
2146     reduce1 --> K
2147     - : term = K
2148
2149 Since the initial input (`I(IK)`) is a redex, the result after the
2150 one-step reduction is `IK`.  We recursively call `reduce1` on this
2151 input.  Since `IK` is itself a redex, the result after one-step
2152 reduction is `K`.  We recursively call `reduce1` on this input.  Since
2153 `K` is not a redex, the recursion bottoms out, and we simply return
2154 it.  
2155
2156 But this function doesn't do enough reduction.
2157
2158     # reduce1 (FA (FA (I, I), K));;
2159     - : term = FA (FA (I, I), K)
2160
2161 Because the top-level term is not a redex, `reduce1` returns it
2162 without any evaluation.  What we want is to evaluate the subparts of a
2163 complex term.
2164
2165     let rec reduce2 (t:term):term = match t with
2166         I -> I
2167       | K -> K
2168       | S -> S
2169       | FA (a, b) -> 
2170           let t' = FA (reduce2 a, reduce2 b) in
2171             if (is_redex t') then reduce2 (reduce_one_step t')
2172                              else t'
2173
2174 Since we need access to the subterms, we do pattern matching on the
2175 input term.  If the input is simple, we return it.  If the input is
2176 complex, we first process the subexpressions, and only then see if we
2177 have a redex.  To understand how this works, follow the trace
2178 carefully:
2179
2180     # reduce2 (FA(FA(I,I),K));;
2181     reduce2 <-- FA (FA (I, I), K)
2182
2183       reduce2 <-- K          ; first main recursive call
2184       reduce2 --> K
2185
2186       reduce2 <-- FA (I, I)  ; second main recursive call
2187         reduce2 <-- I
2188         reduce2 --> I
2189         reduce2 <-- I
2190         reduce2 --> I
2191       reduce2 <-- I
2192
2193       reduce2 --> I           ; third main recursive call
2194       reduce2 --> I
2195
2196       reduce2 <-- K           ; fourth
2197       reduce2 --> K
2198     reduce2 --> K
2199     - : term = K
2200
2201 Ok, there's a lot going on here.  Since the input is complex, the
2202 first thing the function does is construct `t'`.  In order to do this,
2203 it must reduce the two main subexpressions, `II` and `K`.  But we see
2204 from the trace that it begins with the right-hand expression, `K`.  We
2205 didn't explicitly tell it to begin with the right-hand subexpression,
2206 so control over evaluation order is starting to spin out of our
2207 control.  (We'll get it back later, don't worry.)
2208
2209 In any case, in the second main recursive call, we evaluate `II`.  The
2210 result is `I`.  The third main recursive call tests whether this
2211 result needs any further processing; it doesn't.  
2212
2213 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
2214 redex, we ship it off to reduce_one_step, getting the term `K` as a
2215 result.  The fourth recursive call checks that there is no more
2216 reduction work to be done (there isn't), and that's our final result.
2217
2218 You can see in more detail what is going on by tracing both reduce2
2219 and reduce_one_step, but that makes for some long traces.
2220
2221 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
2222 K`, as desired.
2223
2224 Because the OCaml interpreter evaluates the rightmost expression  
2225 in the course of building `t'`, however, it will always evaluate the
2226 right hand subexpression, whether it needs to or not.  And sure
2227 enough,
2228
2229     # reduce2 (FA(FA(K,I),skomega));;
2230       C-c C-cInterrupted.
2231
2232 instead of performing the leftmost reduction first, and recognizing 
2233 that this term reduces to the normal form `I`, we get lost endlessly
2234 trying to reduce skomega.
2235
2236 To emphasize that our evaluation order here is at the mercy of the
2237 evaluation order of OCaml, here is the exact same program translated
2238 into Haskell.  We'll put them side by side to emphasize the exact parallel.
2239
2240 <pre>
2241 OCaml                                                          Haskell
2242 ==========================================================     =========================================================
2243
2244 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
2245                                                                                                                       
2246 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
2247                                                                                                                       
2248                                                                reduce_one_step :: Term -> Term                                
2249 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
2250     FA(I,a) -> a                                                 FA I a -> a                                                  
2251   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
2252   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
2253   | _ -> t                                                       _ -> t                                               
2254                                                                                                                       
2255                                                                is_redex :: Term -> Bool                               
2256 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
2257                                                                                                                       
2258                                                                reduce2 :: Term -> Term                                        
2259 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
2260     I -> I                                                       I -> I                                               
2261   | K -> K                                                       K -> K                                               
2262   | S -> S                                                       S -> S                                               
2263   | FA (a, b) ->                                                 FA a b ->                                                    
2264       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
2265         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
2266                          else t'                                                      else t'                                
2267 </pre>
2268
2269 There are some differences in the way types are made explicit, and in
2270 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
2271 Haskell).  But the two programs are essentially identical.
2272
2273 Yet the Haskell program finds the normal form for KI -->
2274
2275 [[!toc levels=2]]
2276
2277 # Reasoning about evaluation order in Combinatory Logic
2278
2279 We've discussed evaluation order before, primarily in connection with
2280 the untyped lambda calculus.  Whenever a term has more than one redex,
2281 we have to choose which one to reduce, and this choice can make a
2282 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
2283 leftmost redex first, the term reduces to the normal form `I` in one
2284 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
2285 we do not arrive at a normal form, and are in danger of entering an
2286 infinite loop.
2287
2288 Thanks to the introduction of sum types (disjoint union), we are now
2289 in a position to gain a deeper understanding by writing a program that
2290 allows us to experiment with different evaluation order strategies.
2291
2292 One thing we'll see is that it is all too easy for the evaluation
2293 order properties of an evaluator to depend on the evaluation order
2294 properties of the programming language in which the evaluator is
2295 written.  We will seek to write an evaluator in which the order of
2296 evaluation is insensitive to the evaluator language.  The goal is to
2297 find an order-insensitive way to reason about evaluation order.
2298
2299 The first evaluator we develop will evaluate terms in Combinatory
2300 Logic.  That will significantly simplify the program, since we won't
2301 need to worry about variables or substitution.  As we develop and
2302 extend our evaluator in future weeks, we'll switch to lambdas, but for
2303 now, working with the elegant simplicity of Combinatory Logic will
2304 make the evaluation order issues easier to grasp.
2305
2306 A brief review: a term in CL is the combination of three basic
2307 expressions, `S`, `K`, and `I`, governed by the following reduction
2308 rules:
2309
2310     Ia ~~> a
2311     Kab ~~> b
2312     Sabc ~~> ac(bc)
2313
2314 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
2315 that how to embed the untyped lambda calculus in CL, so it's no
2316 surprise that the same evaluation order issues arise in CL.
2317
2318     skomega = SII(SII)
2319             ~~> I(SII)(I(SII))
2320             ~~> SII(SII)
2321
2322 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
2323 here, though we'll use the same symbol, `Ω`.  If we consider the term
2324
2325     KIΩ == KI(SII(SII))
2326
2327 we can choose to reduce the leftmost redex by firing the reduction
2328 rule for `K`, in which case the term reduces to the normal form `I` in
2329 one step; or we can choose to reduce the skomega part, by firing the
2330 reduction rule fo `S`, in which case we do not get a normal form,
2331 we're headed towards an infinite loop.
2332
2333 With sum types, we can define terms in CL in OCaml as follows:
2334
2335     type term = I | S | K | FA of (term * term)
2336
2337     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
2338     let test1 = FA (FA (K,I), skomega)
2339
2340 This recursive type definition says that a term in CL is either one of
2341 the three simple expressions, or else a pair of CL expressions.
2342 Following Heim and Kratzer, `FA` stands for Functional Application.
2343 With this type definition, we can encode skomega, as well as other
2344 terms whose reduction behavior we want to control.
2345
2346 Using pattern matching, it is easy to code the one-step reduction
2347 rules for CL:
2348
2349     let reduce_one_step (t:term):term = match t with
2350         FA(I,a) -> a
2351       | FA(FA(K,a),b) -> a
2352       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
2353       | _ -> t
2354
2355     # reduce_one_step (FA(FA(K,S),I));;
2356     - : term = S
2357     # reduce_one_step skomega;;
2358     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
2359
2360 The need to explicitly insert the type constructor `FA` obscures
2361 things a bit, but it's still possible to see how the one-step
2362 reduction function is just the reduction rules for CL.  The
2363 OCaml interpreter shows us that the function faithfully recognizes
2364 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
2365
2366 We can now say precisely what it means to be a redex in CL.
2367
2368     let is_redex (t:term):bool = not (t = reduce_one_step t)
2369
2370     # is_redex K;;
2371     - : bool = false
2372     # is_redex (FA(K,I));;
2373     - : bool = false
2374     # is_redex (FA(FA(K,I),S));;
2375     - : bool = true
2376     # is_redex skomega;;
2377     - : book = true
2378
2379 Warning: this definition relies on the fact that the one-step
2380 reduction of a CL term is never identical to the original term.  This
2381 would not work for the untyped lambda calculus, since
2382 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
2383 order to decide whether two terms are equal, OCaml has to recursively
2384 compare the elements of complex CL terms.  It is able to figure out
2385 how to do this because we provided an explicit definition of the
2386 datatype Term.
2387
2388 As you would expect, a term in CL is in normal form when it contains
2389 no redexes.
2390
2391 In order to fully reduce a term, we need to be able to reduce redexes
2392 that are not at the top level of the term.
2393
2394     (KKI)SI ~~> KSI ~~> S
2395
2396 That is, we want to be able to first evaluate the redex `KKI` that is
2397 a proper subpart of the larger term to produce a new intermediate term
2398 that we can then evaluate to the final normal form.
2399
2400 Because we need to process subparts, and because the result after
2401 processing a subpart may require further processing, the recursive
2402 structure of our evaluation function has to be quite subtle.  To truly
2403 understand it, you will need to do some sophisticated thinking about
2404 how recursion works.  We'll show you how to keep track of what is
2405 going on by constructing an recursive execution trace of inputs and
2406 outputs.
2407
2408 We'll develop our full reduction function in stages.  Once we have it
2409 working, we'll then consider some variants.  Just to be precise, we'll
2410 distinguish each microvariant with its own index number embedded in
2411 its name.
2412
2413     let rec reduce1 (t:term):term = 
2414       if (is_redex t) then reduce1 (reduce_one_step t)
2415                       else t
2416
2417 If the input is a redex, we ship it off to `reduce_one_step` for
2418 processing.  But just in case the result of the one-step reduction is
2419 itself a redex, we recursively call `reduce1`.  The recursion will
2420 continue until the result is no longer a redex.
2421
2422     #trace reduce1;;
2423     reduce1 is now traced.
2424     # reduce1 (FA (I, FA (I, K)));;
2425     reduce1 <-- FA (I, FA (I, K))
2426       reduce1 <-- FA (I, K)
2427         reduce1 <-- K
2428         reduce1 --> K
2429       reduce1 --> K
2430     reduce1 --> K
2431     - : term = K
2432
2433 Since the initial input (`I(IK)`) is a redex, the result after the
2434 one-step reduction is `IK`.  We recursively call `reduce1` on this
2435 input.  Since `IK` is itself a redex, the result after one-step
2436 reduction is `K`.  We recursively call `reduce1` on this input.  Since
2437 `K` is not a redex, the recursion bottoms out, and we simply return
2438 it.  
2439
2440 But this function doesn't do enough reduction.
2441
2442     # reduce1 (FA (FA (I, I), K));;
2443     - : term = FA (FA (I, I), K)
2444
2445 Because the top-level term is not a redex, `reduce1` returns it
2446 without any evaluation.  What we want is to evaluate the subparts of a
2447 complex term.
2448
2449     let rec reduce2 (t:term):term = match t with
2450         I -> I
2451       | K -> K
2452       | S -> S
2453       | FA (a, b) -> 
2454           let t' = FA (reduce2 a, reduce2 b) in
2455             if (is_redex t') then reduce2 (reduce_one_step t')
2456                              else t'
2457
2458 Since we need access to the subterms, we do pattern matching on the
2459 input term.  If the input is simple, we return it.  If the input is
2460 complex, we first process the subexpressions, and only then see if we
2461 have a redex.  To understand how this works, follow the trace
2462 carefully:
2463
2464     # reduce2 (FA(FA(I,I),K));;
2465     reduce2 <-- FA (FA (I, I), K)
2466
2467       reduce2 <-- K          ; first main recursive call
2468       reduce2 --> K
2469
2470       reduce2 <-- FA (I, I)  ; second main recursive call
2471         reduce2 <-- I
2472         reduce2 --> I
2473         reduce2 <-- I
2474         reduce2 --> I
2475       reduce2 <-- I
2476
2477       reduce2 --> I           ; third main recursive call
2478       reduce2 --> I
2479
2480       reduce2 <-- K           ; fourth
2481       reduce2 --> K
2482     reduce2 --> K
2483     - : term = K
2484
2485 Ok, there's a lot going on here.  Since the input is complex, the
2486 first thing the function does is construct `t'`.  In order to do this,
2487 it must reduce the two main subexpressions, `II` and `K`.  But we see
2488 from the trace that it begins with the right-hand expression, `K`.  We
2489 didn't explicitly tell it to begin with the right-hand subexpression,
2490 so control over evaluation order is starting to spin out of our
2491 control.  (We'll get it back later, don't worry.)
2492
2493 In any case, in the second main recursive call, we evaluate `II`.  The
2494 result is `I`.  The third main recursive call tests whether this
2495 result needs any further processing; it doesn't.  
2496
2497 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
2498 redex, we ship it off to reduce_one_step, getting the term `K` as a
2499 result.  The fourth recursive call checks that there is no more
2500 reduction work to be done (there isn't), and that's our final result.
2501
2502 You can see in more detail what is going on by tracing both reduce2
2503 and reduce_one_step, but that makes for some long traces.
2504
2505 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
2506 K`, as desired.
2507
2508 Because the OCaml interpreter evaluates the rightmost expression  
2509 in the course of building `t'`, however, it will always evaluate the
2510 right hand subexpression, whether it needs to or not.  And sure
2511 enough,
2512
2513     # reduce2 (FA(FA(K,I),skomega));;
2514       C-c C-cInterrupted.
2515
2516 instead of performing the leftmost reduction first, and recognizing 
2517 that this term reduces to the normal form `I`, we get lost endlessly
2518 trying to reduce skomega.
2519
2520 To emphasize that our evaluation order here is at the mercy of the
2521 evaluation order of OCaml, here is the exact same program translated
2522 into Haskell.  We'll put them side by side to emphasize the exact parallel.
2523
2524 <pre>
2525 OCaml                                                          Haskell
2526 ==========================================================     =========================================================
2527
2528 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
2529                                                                                                                       
2530 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
2531                                                                                                                       
2532                                                                reduce_one_step :: Term -> Term                                
2533 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
2534     FA(I,a) -> a                                                 FA I a -> a                                                  
2535   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
2536   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
2537   | _ -> t                                                       _ -> t                                               
2538                                                                                                                       
2539                                                                is_redex :: Term -> Bool                               
2540 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
2541                                                                                                                       
2542                                                                reduce2 :: Term -> Term                                        
2543 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
2544     I -> I                                                       I -> I                                               
2545   | K -> K                                                       K -> K                                               
2546   | S -> S                                                       S -> S                                               
2547   | FA (a, b) ->                                                 FA a b ->                                                    
2548       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
2549         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
2550                          else t'                                                      else t'                                
2551 </pre>
2552
2553 There are some differences in the way types are made explicit, and in
2554 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
2555 Haskell).  But the two programs are essentially identical.
2556
2557 Yet the Haskell program finds the normal form for KI -->
2558
2559 [[!toc levels=2]]
2560
2561 # Reasoning about evaluation order in Combinatory Logic
2562
2563 We've discussed evaluation order before, primarily in connection with
2564 the untyped lambda calculus.  Whenever a term has more than one redex,
2565 we have to choose which one to reduce, and this choice can make a
2566 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
2567 leftmost redex first, the term reduces to the normal form `I` in one
2568 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
2569 we do not arrive at a normal form, and are in danger of entering an
2570 infinite loop.
2571
2572 Thanks to the introduction of sum types (disjoint union), we are now
2573 in a position to gain a deeper understanding by writing a program that
2574 allows us to experiment with different evaluation order strategies.
2575
2576 One thing we'll see is that it is all too easy for the evaluation
2577 order properties of an evaluator to depend on the evaluation order
2578 properties of the programming language in which the evaluator is
2579 written.  We will seek to write an evaluator in which the order of
2580 evaluation is insensitive to the evaluator language.  The goal is to
2581 find an order-insensitive way to reason about evaluation order.
2582
2583 The first evaluator we develop will evaluate terms in Combinatory
2584 Logic.  That will significantly simplify the program, since we won't
2585 need to worry about variables or substitution.  As we develop and
2586 extend our evaluator in future weeks, we'll switch to lambdas, but for
2587 now, working with the elegant simplicity of Combinatory Logic will
2588 make the evaluation order issues easier to grasp.
2589
2590 A brief review: a term in CL is the combination of three basic
2591 expressions, `S`, `K`, and `I`, governed by the following reduction
2592 rules:
2593
2594     Ia ~~> a
2595     Kab ~~> b
2596     Sabc ~~> ac(bc)
2597
2598 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
2599 that how to embed the untyped lambda calculus in CL, so it's no
2600 surprise that the same evaluation order issues arise in CL.
2601
2602     skomega = SII(SII)
2603             ~~> I(SII)(I(SII))
2604             ~~> SII(SII)
2605
2606 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
2607 here, though we'll use the same symbol, `Ω`.  If we consider the term
2608
2609     KIΩ == KI(SII(SII))
2610
2611 we can choose to reduce the leftmost redex by firing the reduction
2612 rule for `K`, in which case the term reduces to the normal form `I` in
2613 one step; or we can choose to reduce the skomega part, by firing the
2614 reduction rule fo `S`, in which case we do not get a normal form,
2615 we're headed towards an infinite loop.
2616
2617 With sum types, we can define terms in CL in OCaml as follows:
2618
2619     type term = I | S | K | FA of (term * term)
2620
2621     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
2622     let test1 = FA (FA (K,I), skomega)
2623
2624 This recursive type definition says that a term in CL is either one of
2625 the three simple expressions, or else a pair of CL expressions.
2626 Following Heim and Kratzer, `FA` stands for Functional Application.
2627 With this type definition, we can encode skomega, as well as other
2628 terms whose reduction behavior we want to control.
2629
2630 Using pattern matching, it is easy to code the one-step reduction
2631 rules for CL:
2632
2633     let reduce_one_step (t:term):term = match t with
2634         FA(I,a) -> a
2635       | FA(FA(K,a),b) -> a
2636       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
2637       | _ -> t
2638
2639     # reduce_one_step (FA(FA(K,S),I));;
2640     - : term = S
2641     # reduce_one_step skomega;;
2642     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
2643
2644 The need to explicitly insert the type constructor `FA` obscures
2645 things a bit, but it's still possible to see how the one-step
2646 reduction function is just the reduction rules for CL.  The
2647 OCaml interpreter shows us that the function faithfully recognizes
2648 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
2649
2650 We can now say precisely what it means to be a redex in CL.
2651
2652     let is_redex (t:term):bool = not (t = reduce_one_step t)
2653
2654     # is_redex K;;
2655     - : bool = false
2656     # is_redex (FA(K,I));;
2657     - : bool = false
2658     # is_redex (FA(FA(K,I),S));;
2659     - : bool = true
2660     # is_redex skomega;;
2661     - : book = true
2662
2663 Warning: this definition relies on the fact that the one-step
2664 reduction of a CL term is never identical to the original term.  This
2665 would not work for the untyped lambda calculus, since
2666 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
2667 order to decide whether two terms are equal, OCaml has to recursively
2668 compare the elements of complex CL terms.  It is able to figure out
2669 how to do this because we provided an explicit definition of the
2670 datatype Term.
2671
2672 As you would expect, a term in CL is in normal form when it contains
2673 no redexes.
2674
2675 In order to fully reduce a term, we need to be able to reduce redexes
2676 that are not at the top level of the term.
2677
2678     (KKI)SI ~~> KSI ~~> S
2679
2680 That is, we want to be able to first evaluate the redex `KKI` that is
2681 a proper subpart of the larger term to produce a new intermediate term
2682 that we can then evaluate to the final normal form.
2683
2684 Because we need to process subparts, and because the result after
2685 processing a subpart may require further processing, the recursive
2686 structure of our evaluation function has to be quite subtle.  To truly
2687 understand it, you will need to do some sophisticated thinking about
2688 how recursion works.  We'll show you how to keep track of what is
2689 going on by constructing an recursive execution trace of inputs and
2690 outputs.
2691
2692 We'll develop our full reduction function in stages.  Once we have it
2693 working, we'll then consider some variants.  Just to be precise, we'll
2694 distinguish each microvariant with its own index number embedded in
2695 its name.
2696
2697     let rec reduce1 (t:term):term = 
2698       if (is_redex t) then reduce1 (reduce_one_step t)
2699                       else t
2700
2701 If the input is a redex, we ship it off to `reduce_one_step` for
2702 processing.  But just in case the result of the one-step reduction is
2703 itself a redex, we recursively call `reduce1`.  The recursion will
2704 continue until the result is no longer a redex.
2705
2706     #trace reduce1;;
2707     reduce1 is now traced.
2708     # reduce1 (FA (I, FA (I, K)));;
2709     reduce1 <-- FA (I, FA (I, K))
2710       reduce1 <-- FA (I, K)
2711         reduce1 <-- K
2712         reduce1 --> K
2713       reduce1 --> K
2714     reduce1 --> K
2715     - : term = K
2716
2717 Since the initial input (`I(IK)`) is a redex, the result after the
2718 one-step reduction is `IK`.  We recursively call `reduce1` on this
2719 input.  Since `IK` is itself a redex, the result after one-step
2720 reduction is `K`.  We recursively call `reduce1` on this input.  Since
2721 `K` is not a redex, the recursion bottoms out, and we simply return
2722 it.  
2723
2724 But this function doesn't do enough reduction.
2725
2726     # reduce1 (FA (FA (I, I), K));;
2727     - : term = FA (FA (I, I), K)
2728
2729 Because the top-level term is not a redex, `reduce1` returns it
2730 without any evaluation.  What we want is to evaluate the subparts of a
2731 complex term.
2732
2733     let rec reduce2 (t:term):term = match t with
2734         I -> I
2735       | K -> K
2736       | S -> S
2737       | FA (a, b) -> 
2738           let t' = FA (reduce2 a, reduce2 b) in
2739             if (is_redex t') then reduce2 (reduce_one_step t')
2740                              else t'
2741
2742 Since we need access to the subterms, we do pattern matching on the
2743 input term.  If the input is simple, we return it.  If the input is
2744 complex, we first process the subexpressions, and only then see if we
2745 have a redex.  To understand how this works, follow the trace
2746 carefully:
2747
2748     # reduce2 (FA(FA(I,I),K));;
2749     reduce2 <-- FA (FA (I, I), K)
2750
2751       reduce2 <-- K          ; first main recursive call
2752       reduce2 --> K
2753
2754       reduce2 <-- FA (I, I)  ; second main recursive call
2755         reduce2 <-- I
2756         reduce2 --> I
2757         reduce2 <-- I
2758         reduce2 --> I
2759       reduce2 <-- I
2760
2761       reduce2 --> I           ; third main recursive call
2762       reduce2 --> I
2763
2764       reduce2 <-- K           ; fourth
2765       reduce2 --> K
2766     reduce2 --> K
2767     - : term = K
2768
2769 Ok, there's a lot going on here.  Since the input is complex, the
2770 first thing the function does is construct `t'`.  In order to do this,
2771 it must reduce the two main subexpressions, `II` and `K`.  But we see
2772 from the trace that it begins with the right-hand expression, `K`.  We
2773 didn't explicitly tell it to begin with the right-hand subexpression,
2774 so control over evaluation order is starting to spin out of our
2775 control.  (We'll get it back later, don't worry.)
2776
2777 In any case, in the second main recursive call, we evaluate `II`.  The
2778 result is `I`.  The third main recursive call tests whether this
2779 result needs any further processing; it doesn't.  
2780
2781 At this point, we have constructed `t' == FA(I,K)`.  Since that's a
2782 redex, we ship it off to reduce_one_step, getting the term `K` as a
2783 result.  The fourth recursive call checks that there is no more
2784 reduction work to be done (there isn't), and that's our final result.
2785
2786 You can see in more detail what is going on by tracing both reduce2
2787 and reduce_one_step, but that makes for some long traces.
2788
2789 So we've solved our first problem: reduce2 recognizes that `IIK ~~>
2790 K`, as desired.
2791
2792 Because the OCaml interpreter evaluates the rightmost expression  
2793 in the course of building `t'`, however, it will always evaluate the
2794 right hand subexpression, whether it needs to or not.  And sure
2795 enough,
2796
2797     # reduce2 (FA(FA(K,I),skomega));;
2798       C-c C-cInterrupted.
2799
2800 instead of performing the leftmost reduction first, and recognizing 
2801 that this term reduces to the normal form `I`, we get lost endlessly
2802 trying to reduce skomega.
2803
2804 To emphasize that our evaluation order here is at the mercy of the
2805 evaluation order of OCaml, here is the exact same program translated
2806 into Haskell.  We'll put them side by side to emphasize the exact parallel.
2807
2808 <pre>
2809 OCaml                                                          Haskell
2810 ==========================================================     =========================================================
2811
2812 type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
2813                                                                                                                       
2814 let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))          skomega = (FA (FA (FA S I) I) (FA (FA S I) I))                 
2815                                                                                                                       
2816                                                                reduce_one_step :: Term -> Term                                
2817 let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                  
2818     FA(I,a) -> a                                                 FA I a -> a                                                  
2819   | FA(FA(K,a),b) -> a                                           FA (FA K a) b -> a                                           
2820   | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))                   FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)                 
2821   | _ -> t                                                       _ -> t                                               
2822                                                                                                                       
2823                                                                is_redex :: Term -> Bool                               
2824 let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
2825                                                                                                                       
2826                                                                reduce2 :: Term -> Term                                        
2827 let rec reduce2 (t:term):term = match t with                   reduce2 t = case t of                                          
2828     I -> I                                                       I -> I                                               
2829   | K -> K                                                       K -> K                                               
2830   | S -> S                                                       S -> S                                               
2831   | FA (a, b) ->                                                 FA a b ->                                                    
2832       let t' = FA (reduce2 a, reduce2 b) in                        let t' = FA (reduce2 a) (reduce2 b) in                     
2833         if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
2834                          else t'                                                      else t'                                
2835 </pre>
2836
2837 There are some differences in the way types are made explicit, and in
2838 the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
2839 Haskell).  But the two programs are essentially identical.
2840
2841 Yet the Haskell program finds the normal form for KI
2842  -->
2843
2844 [[!toc levels=2]]
2845
2846 # Reasoning about evaluation order in Combinatory Logic
2847
2848 We've discussed evaluation order before, primarily in connection with
2849 the untyped lambda calculus.  Whenever a term has more than one redex,
2850 we have to choose which one to reduce, and this choice can make a
2851 difference.  For instance, in the term `((\x.I)(ωω)`, if we reduce the
2852 leftmost redex first, the term reduces to the normal form `I` in one
2853 step.  But if we reduce the left most redex instead (namely, `(ωω)`),
2854 we do not arrive at a normal form, and are in danger of entering an
2855 infinite loop.
2856
2857 Thanks to the introduction of sum types (disjoint union), we are now
2858 in a position to gain a deeper understanding by writing a program that
2859 allows us to experiment with different evaluation order strategies.
2860
2861 One thing we'll see is that it is all too easy for the evaluation
2862 order properties of an evaluator to depend on the evaluation order
2863 properties of the programming language in which the evaluator is
2864 written.  We will seek to write an evaluator in which the order of
2865 evaluation is insensitive to the evaluator language.  The goal is to
2866 find an order-insensitive way to reason about evaluation order.
2867
2868 The first evaluator we develop will evaluate terms in Combinatory
2869 Logic.  That will significantly simplify the program, since we won't
2870 need to worry about variables or substitution.  As we develop and
2871 extend our evaluator in future weeks, we'll switch to lambdas, but for
2872 now, working with the elegant simplicity of Combinatory Logic will
2873 make the evaluation order issues easier to grasp.
2874
2875 A brief review: a term in CL is the combination of three basic
2876 expressions, `S`, `K`, and `I`, governed by the following reduction
2877 rules:
2878
2879     Ia ~~> a
2880     Kab ~~> b
2881     Sabc ~~> ac(bc)
2882
2883 where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
2884 that how to embed the untyped lambda calculus in CL, so it's no
2885 surprise that the same evaluation order issues arise in CL.
2886
2887     skomega = SII(SII)
2888             ~~> I(SII)(I(SII))
2889             ~~> SII(SII)
2890
2891 Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
2892 here, though we'll use the same symbol, `Ω`.  If we consider the term
2893
2894     KIΩ == KI(SII(SII))
2895
2896 we can choose to reduce the leftmost redex by firing the reduction
2897 rule for `K`, in which case the term reduces to the normal form `I` in
2898 one step; or we can choose to reduce the skomega part, by firing the
2899 reduction rule fo `S`, in which case we do not get a normal form,
2900 we're headed towards an infinite loop.
2901
2902 With sum types, we can define terms in CL in OCaml as follows:
2903
2904     type term = I | S | K | FA of (term * term)
2905
2906     let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
2907     let test1 = FA (FA (K,I), skomega)
2908
2909 This recursive type definition says that a term in CL is either one of
2910 the three simple expressions, or else a pair of CL expressions.
2911 Following Heim and Kratzer, `FA` stands for Functional Application.
2912 With this type definition, we can encode skomega, as well as other
2913 terms whose reduction behavior we want to control.
2914
2915 Using pattern matching, it is easy to code the one-step reduction
2916 rules for CL:
2917
2918     let reduce_one_step (t:term):term = match t with
2919         FA(I,a) -> a
2920       | FA(FA(K,a),b) -> a
2921       | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
2922       | _ -> t
2923
2924     # reduce_one_step (FA(FA(K,S),I));;
2925     - : term = S
2926     # reduce_one_step skomega;;
2927     - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
2928
2929 The need to explicitly insert the type constructor `FA` obscures
2930 things a bit, but it's still possible to see how the one-step
2931 reduction function is just the reduction rules for CL.  The
2932 OCaml interpreter shows us that the function faithfully recognizes
2933 that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
2934
2935 We can now say precisely what it means to be a redex in CL.
2936
2937     let is_redex (t:term):bool = not (t = reduce_one_step t)
2938
2939     # is_redex K;;
2940     - : bool = false
2941     # is_redex (FA(K,I));;
2942     - : bool = false
2943     # is_redex (FA(FA(K,I),S));;
2944     - : bool = true
2945     # is_redex skomega;;
2946     - : book = true
2947
2948 Warning: this definition relies on the fact that the one-step
2949 reduction of a CL term is never identical to the original term.  This
2950 would not work for the untyped lambda calculus, since
2951 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.  Note that in
2952 order to decide whether two terms are equal, OCaml has to recursively
2953 compare the elements of complex CL terms.  It is able to figure out
2954 how to do this because we provided an explicit definition of the
2955 datatype Term.
2956
2957 As you would expect, a term in CL is in normal form when it contains
2958 no redexes.
2959
2960 In order to fully reduce a term, we need to be able to reduce redexes
2961 that are not at the top level of the term.
2962
2963     (KKI)SI ~~> KSI ~~> S
2964
2965 That is, we want to be able to first evaluate the redex `KKI` that is
2966 a proper subpart of the larger term to produce a new intermediate term
2967 that we can then evaluate to the final normal form.
2968
2969 Because we need to process subparts, and because the result after
2970 processing a subpart may require further processing, the recursive
2971 structure of our evaluation function has to be quite subtle.  To truly
2972 understand it, you will need to do some sophisticated thinking about
2973 how recursion works.  We'll show you how to keep track of what is
2974 going on by constructing an recursive execution trace of inputs and
2975 outputs.
2976
2977 We'll develop our full reduction function in stages.  Once we have it
2978 working, we'll then consider some variants.  Just to be precise, we'll
2979 distinguish each microvariant with its own index number embedded in
2980 its name.
2981
2982     let rec reduce1 (t:term):term = 
2983       if (is_redex t) then reduce1 (reduce_one_step t)
2984                       else t
2985
2986 If the input is a redex, we ship it off to `reduce_one_step` for
2987 processing.  But just in case the result of the one-step reduction is
2988 itself a redex, we recursively call `reduce1`.  The recursion will
2989 continue until the result is no longer a redex.
2990
2991     #trace reduce1;;
2992     reduce1 is now traced.
2993     # reduce1 (FA (I, FA (I, K)));;
2994     reduce1 <-- FA (I, FA (I, K))
2995       reduce1 <-- FA (I, K)
2996         reduce1 <-- K
2997         reduce1 --> K
2998       reduce1 --> K
2999     reduce1 --> K
3000     - : term = K
3001
3002 Since the initial input (`I(IK)`) is a redex, the result after the
3003 one-step reduction is `IK`.  We recursively call `reduce1` on this
3004 input.  Since `IK` is itself a redex, the result after one-step
3005 reduction is `K`.  We recursively call `reduce1` on this input.  Since
3006 `K` is not a redex, the recursion bottoms out, and we simply return
3007 it.  
3008
3009 But this function doesn't do enough reduction.
3010
3011     # reduce1 (FA (FA (I, I), K));;
3012     - : term = FA (FA (I, I), K)
3013
3014 Because the top-level term is not a redex, `reduce1` returns it
3015 without any evaluation.  What we want is to evaluate the subparts of a
3016 complex term.
3017
3018     let rec reduce2 (t:term):term = match t with
3019         I -> I
3020       | K -> K
3021       | S -> S
3022       | FA (a, b) -> 
3023           let t' = FA (reduce2 a, reduce2 b) in
3024             if (is_redex t') then reduce2 (reduce_one_step t')
3025                              else t'
3026
3027 Since we need access to the subterms, we do pattern matching on the
3028 input term.  If the input is simple, we return it.  If the input is
3029 complex, we first process the subexpressions, and only then see if we
3030 have a redex.  To understand how this works, follow the trace
3031 carefully:
3032
3033     # reduce2 (FA(FA(I,I),K));;
3034     reduce2 <-- FA (FA (I, I), K)
3035
3036       reduce2 <-- K          ; first main recursive call
3037       reduce2 --> K
3038
3039       reduce2 <-- FA (I, I)  ; second main recursive call
3040         reduce2 <-- I
3041         reduce2 --> I
3042         reduce2 <-- I
3043         reduce2 --> I
3044       reduce2 <-- I
3045
3046       reduce2 --> I           ; third main recursive call
3047       reduce2 --> I
3048
3049       reduce2 <-- K           ; fourth
3050       reduce2 --> K
3051     reduce2 --> K
3052     - : term = K
3053
3054 Ok, there's a lot going on here.  Since the input is complex, the
3055 first thing the function does is&