1 <!-- λ Λ ∀ ≡ α β ω Ω -->
5 ## Reasoning about evaluation order in Combinatory Logic
7 We've discussed [[evaluation order|topics/week3_evaluation_order]]
8 before, primarily in connection with the untyped lambda calculus.
9 Whenever a term contains more than one redex, we have to choose which
10 one to reduce, and this choice can make a difference. For instance,
13 Ω == ωω == (\x.xx)(\x.xx)
17 ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
20 There are two redexes in this term; we've marked the operative lambdas
21 with a star. If we reduce the leftmost redex first, the term reduces
22 to the normal form `I` in one step. But if we reduce the rightmost
23 redex instead, the "reduced" form is `(\x.I)Ω` again, and we're starting off on an infinite loop.
25 Thanks to the introduction of sum types (disjoint union) in the last lecture, we
26 are now in a position to gain a deeper understanding of evaluation
27 order by writing a program that allows us to reason explicitly about evaluation.
29 One thing we'll see is that it is all too easy for the evaluation
30 order properties of an evaluator to depend on the evaluation order
31 properties of the programming language in which the evaluator is
32 written. We would like to write an evaluator in which the order of
33 evaluation is insensitive to the evaluator language. That is, the goal is to
34 find an order-insensitive way to reason about evaluation order. We
35 will not fully succeed in this first attempt, but we will make good
38 The first evaluator we will develop will evaluate terms in Combinatory
39 Logic. This significantly simplifies the discussion, since we won't
40 need to worry about variables or substitution. As we develop and
41 extend our evaluator in homework and other lectures, we'll switch to lambdas, but for
42 now, working with the simplicity of Combinatory Logic will make it
43 easier to highlight evaluation order issues.
45 A brief review of Combinatory Logic: a term in CL is the combination
46 of three basic expressions, `S`, `K`, and `I`, governed by the
47 following reduction rules:
53 where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
54 how to embed the untyped lambda calculus in CL, so it's no surprise
55 that evaluation order issues arise in CL. To illustrate, we'll use
56 the following definition:
59 Skomega = skomega skomega == SII(SII)
63 We'll use the same symbol, `Ω`, for Omega and Skomega: in a lambda
64 term, `Ω` refers to Omega, but in a CL term, `Ω` refers to Skomega as
67 Just as in the corresponding term in the lambda calculus, CL terms can
68 contain more than one redex:
73 We can choose to reduce the leftmost redex by applying the reduction
74 rule for `K`, in which case the term reduces to the normal form `I` in
75 one step; or we can choose to reduce the Skomega part, by applying the
76 reduction rule `S`, in which case we do not get a normal form, and
77 we're headed into an infinite loop.
79 With sum types, we can define CL terms in OCaml as follows:
81 type term = I | K | S | App of (term * term)
83 let skomega = App (App (App (S, I), I), App (App (S, I), I))
85 This type definition says that a term in CL is either one of the three
86 atomic expressions (`I`, `K`, or `S`), or else a pair of CL
87 expressions. `App` stands for Functional Application. With this type
88 definition, we can encode Skomega, as well as other terms whose
89 reduction behavior we want to try to control. We can *control* it because
90 the `App` variant of our datatype merely *encodes* the application of the
91 head to the argument, and doesn't actually *perform* that application.
92 We have to explicitly model the application ourself.
94 Using pattern matching, it is easy to code the one-step reduction
97 let reduce_if_redex (t:term) : term = match t with
99 | App(App(K,a),b) -> a
100 | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
103 # reduce_if_redex (App(App(K,S),I));;
105 # reduce_if_redex skomega;;
106 - : term = App (App (I, App (App (S, I), I)), App (I, App (App (S, I), I)))
108 The definition of `reduce_if_redex` explicitly says that it expects
109 its input argument `t` to have type `term`, and the second `: term`
110 says that the result the function delivers will also be of
113 The type constructor `App` obscures things a bit, but it's still
114 possible to see how the one-step reduction function is just the
115 reduction rules for CL. The OCaml interpreter responses given above show us that the
116 function faithfully recognizes that `KSI ~~> S`, and that `Skomega ~~>
119 As you would expect, a term in CL is in normal form when it contains
120 no redexes (analogously for head normal form, weak head normal form, etc.)
122 How can we tell whether a term is a redex? Here's one way:
124 let is_redex (t:term):bool = not (t = reduce_if_redex t)
128 # is_redex (App(K,I));;
130 # is_redex (App(App(K,I),S));;
135 In order to decide whether two terms are equal, OCaml has to
136 recursively compare the elements of complex CL terms. It is able to
137 figure out how to do this because we provided an explicit definition
138 of the datatype `term`.
140 Warning: this method for telling whether a term is a redex relies on the accidental fact that the
141 one-step reduction of a CL term is never identical to the original
142 term. This would not work for the untyped lambda calculus, since
143 `((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Neither would it work if
144 we had chosen some other combinators as primitives (`W W1 W2` reduces to
145 `W1 W2 W2`, so if they are all `W`s we'd be in trouble.) We will discuss
146 some alternative strategies in other notes.
148 So far, we've only asked whether a term _is_ a redex, not whether it _contains_ other redexes as subterms. But
149 in order to fully reduce a term, we need to be able to reduce redexes
150 that are not at the top level of the term. Because we need to process subterms, and because the result after
151 processing a subterm may require further processing, the recursive
152 structure of our evaluation function has to be somewhat subtle. To
153 truly understand, we will need to do some sophisticated thinking
154 about how recursion works.
156 We'll develop our full reduction function in two stages. Once we have
157 it working, we'll then consider a variant.
159 let rec reduce_try1 (t:term) : term =
160 if (is_redex t) then let t' = reduce_if_redex t
164 If the input is a redex, we ship it off to `reduce_if_redex` for
165 processing. But just in case the result of the one-step reduction is
166 itself a redex, we recursively apply `reduce_try1` to the result. The recursion
167 will continue until the result is no longer a redex. We're aiming at
168 allowing the evaluator to recognize that
170 I (I K) ~~> I K ~~> K
172 When trying to understand how recursive functions work, it can be
173 extremely helpful to examine an execution trace of inputs and
176 # #trace reduce_try1;;
177 reduce_try1 is now traced.
179 The first `#` there is OCaml's prompt. The text beginning `#trace ...` is what we typed. Now OCaml will report on all the input to, and results from, the `reduce_try1` function. Watch:
181 # reduce_try1 (App (I, App (I, K)));;
182 reduce_try1 <-- App (I, App (I, K))
183 reduce_try1 <-- App (I, K)
190 In the trace, "`<--`" shows the input argument to a call to
191 `reduce_try1`, and "`-->`" shows the output result.
193 Since the initial input (`I(IK)`) is a redex, the result after the
194 one-step reduction is `IK`. We recursively call `reduce_try1` on
195 this input. Since `IK` is itself a redex, the result after one-step
196 reduction is `K`. We recursively call `reduce_try1` on this input. Since
197 `K` is not a redex, the recursion bottoms out, and we return the
200 But this function doesn't do enough reduction. We want to recognize
201 the following reduction path:
205 But the reduction function as written above does not deliver this result:
207 # reduce_try1 (App (App (I, I), K));;
208 - : term = App (App (I, I), K)
210 The reason is that the top-level term is not a redex to start with,
211 so `reduce_try1` returns it without any evaluation.
213 What we want is to evaluate the subterms of a complex term. We'll do this by pattern matching our
214 top-level term to see when it _has_ subterms:
216 let rec reduce_try2 (t : term) : term = match t with
221 let t' = App (reduce_try2 a, reduce_try2 b) in
222 if (is_redex t') then let t'' = reduce_if_redex t'
226 Since we need access to the subterms, we do pattern matching on the
227 input. If the input is simple (the first three `match` cases), we
228 return it without further processing. But if the input is complex, we
229 first process the subexpressions, and only then see if we have a redex
232 To understand how this works, follow the trace
235 # reduce_try2 (App(App(I,I),K));;
236 reduce_try2 <-- App (App (I, I), K)
238 reduce_try2 <-- K ; first main recursive call
241 reduce_try2 <-- App (I, I) ; second main recursive call
250 reduce_try2 <-- K ; third
255 Ok, there's a lot going on here. Since the input is complex, the
256 first thing the function does is construct `t'`. In order to do this,
257 it must reduce the two main subexpressions, `II` and `K`.
259 There are three recursive calls to the `reduce` function, each of
260 which gets triggered during the processing of this example. They have
261 been marked in the trace.
263 The don't quite go in the order in which they appear in the code,
264 however! We see from the trace that it begins with the right-hand
265 expression, `K`. We didn't explicitly tell it to begin with the
266 right-hand subexpression, so control over evaluation order is starting
267 to spin out of our control. (We'll get it back later, don't worry.)
269 In any case, in the second main recursive call, we evaluate `II`. The
272 At this point, we have constructed `t' == App(I,K)`. Since that's a
273 redex, we ship it off to reduce_if_redex, getting the term `K` as a
274 result. The third recursive call checks that there is no more
275 reduction work to be done (there isn't), and that's our final result.
277 You can see in more detail what is going on by tracing both reduce
278 and reduce_if_redex, but that makes for some long traces.
280 So we've solved our first problem: `reduce` now recognizes that `IIK ~~>
283 Because the OCaml interpreter evaluates each subexpression in the
284 course of building `t'`, however, it will always evaluate the right
285 hand subexpression, whether it needs to or not. And sure enough,
287 # reduce_try2 (App(App(K,I),skomega));;
290 Running the evaluator with this input leads to an infinite loop, and
291 the only way to get out is to kill the interpreter with control-c.
293 Instead of performing the leftmost reduction first, and recognizing
294 that this term reduces to the normal form `I`, we get lost endlessly
295 trying to reduce Skomega.
297 ## Laziness is hard to overcome
299 To emphasize that our evaluation order here is at the mercy of the
300 evaluation order of OCaml, here is the exact same program translated
301 into Haskell. We'll put them side by side to emphasize the exact parallel.
305 ========================================================== =========================================================
307 type term = I | S | K | App of (term * term) data Term = I | S | K | App Term Term deriving (Eq, Show)
309 let skomega = App (App (App (S,I), I), App (App (S,I), I)) skomega = (App (App (App S I) I) (App (App S I) I))
311 reduce_if_redex :: Term -> Term
312 let reduce_if_redex (t:term):term = match t with reduce_if_redex t = case t of
313 | App(I,a) -> a App I a -> a
314 | App(App(K,a),b) -> a App (App K a) b -> a
315 | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) App (App (App S a) b) c -> App (App a c) (App b c)
318 is_redex :: Term -> Bool
319 let is_redex (t:term):bool = not (t = reduce_if_redex t) is_redex t = not (t == reduce_if_redex t)
321 reduce_try2 :: Term -> Term
322 let rec reduce_try2 (t : term) : term = match t with reduce_try2 t = case t of
326 | App (a, b) -> App a b ->
327 let t' = App (reduce_try2 a, reduce_try2 b) in let t' = App (reduce_try2 a) (reduce_try2 b) in
328 if (is_redex t') then let t'' = reduce_if_redex t' if (is_redex t') then reduce_try2 (reduce_if_redex t')
329 in reduce_try2 t'' else t'
333 There are some differences in the way types are made explicit, and in
334 the way terms are specified (`App(a,b)` for Ocaml versus `App a b` for
335 Haskell). But the two programs are essentially identical.
337 Yet the Haskell program finds the normal form for `KIΩ`:
339 *Main> reduce_try2 (App (App K I) skomega)
342 Woa! First of all, this is wierd. Haskell's evaluation strategy is
343 called "lazy". Apparently, Haskell is so lazy that even after we've
344 asked it to construct `t'` by evaluating `reduce_try2 a` and `reduce_try2 b`, it
345 doesn't bother computing `reduce_try2 b`. Instead, it waits to see if we
346 ever really need to use the result.
348 So the program as written does _not_ fully determine evaluation order
349 behavior. At this stage, we have defined an evaluation order that
350 still depends on the evaluation order of the underlying interpreter.
352 There are two questions we could ask:
354 * Can we adjust the OCaml evaluator to exhibit lazy behavior?
356 * Can we adjust the Haskell evaluator to exhibit eager behavior?
358 The answer to the first question is easy and interesting, and we'll
359 give it right away. The answer to the second question is also
360 interesting, but not easy. There are various tricks available in
361 Haskell we could use (such as the `seq` operator, or the `deepseq`
362 operator), but a fully general, satisifying resolution will have to
363 wait until we have Continuation Passing Style transforms.
365 The answer to the first question (Can we adjust the OCaml evaluator to
366 exhibit lazy behavior?) is quite simple:
368 let rec reduce_try3 (t : term) : term = match t with
373 let t' = App (reduce_try3 a, b) in
374 if (is_redex t') then let t'' = reduce_if_redex t'
378 There is only one small difference from `reduce_try2`: instead of setting `t'` to `App
379 (reduce_try3 a, reduce_try3 b)`, we omit one of the recursive calls, and have
380 `App (reduce_try3 a, b)`. That is, we don't evaluate the right-hand
381 subexpression at all. Ever! The only way to get evaluated is to
382 somehow get into functor position.
384 # reduce_try3 (App(App(K,I),skomega));;
386 # reduce_try3 skomega;;
389 The evaluator now has no trouble finding the normal form for `KIΩ`,
390 but evaluating skomega still gives an infinite loop.
392 We can now clarify the larger question at the heart of
395 *How can we can we specify the evaluation order of a computational
396 system in a way that is completely insensitive to the evaluation order
397 of the specification language?*
399 As a final note, we should mention that the evaluators given here are
400 absurdly inefficient computationally. Some computer scientists have
401 trouble even looking at code this inefficient, but the emphasis here
402 is on getting the concepts across as simply as possible.