# Reasoning about evaluation order in Combinatory Logic
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term contains more than one
-redex, we have to choose which one to reduce, and this choice can make
-a difference. For instance, in the term `((\x.I)(ωω)`, if we reduce
-the leftmost redex first, the term reduces to the normal form `I` in
-one step. But if we reduce the left most redex instead (namely,
-`(ωω)`), we do not arrive at a normal form, and are in danger of
-entering an infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference. For instance,
+in the term `((\x.I)(ωω))`, if we reduce the leftmost redex first, the
+term reduces to the normal form `I` in one step. But if we reduce the
+left most redex instead (namely, `(ωω)`), we do not arrive at a normal
+form, and are in danger of entering an infinite loop.
+
+Thanks to the recent introduction of sum types (disjoint union), we are now
in a position to gain a deeper understanding of evaluation order by
writing a program that experiments with different evaluation order
strategies.
progress.
The first evaluator we will develop will evaluate terms in Combinatory
-Logic. This significantly simplifies the program, since we won't need
+Logic. This significantly simplifies the discussion, since we won't need
to worry about variables or substitution. As we develop and extend
our evaluator in future weeks, we'll switch to lambdas, but for now,
working with the simplicity of Combinatory Logic will make the
rules:
Ia ~~> a
- Kab ~~> b
+ Kab ~~> a
Sabc ~~> ac(bc)
where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
how to embed the untyped lambda calculus in CL, so it's no
-surprise that the evaluation order issues arise in CL. To illustrate,
+surprise that evaluation order issues arise in CL. To illustrate,
we'll use the following definition:
skomega = SII(SII)
~~> I(SII)(I(SII))
~~> SII(SII)
-Instead of the lambda term `Ω`, we'll use the CL term skomega. We'll
-use the same symbol, `Ω`, though: in a lambda term, `Ω` refers to
-omega, but in a CL term, `Ω` refers to skomega as defined here.
+We'll use the same symbol, `Ω`, though: in a lambda term, `Ω` refers
+to omega, but in a CL term, `Ω` refers to skomega as defined here.
If we consider the term
KIΩ == KI(SII(SII))
-we can choose to reduce the leftmost redex by firing the reduction
+we can choose to reduce the leftmost redex by applying the reduction
rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule for the leftmost `S`, in which case we do not get a
-normal form, and we're headed towards an infinite loop.
+one step; or we can choose to reduce the skomega part, by applying the
+reduction rule `S`, in which case we do not get a normal form, and
+we're headed towards an infinite loop.
With sum types, we can define terms in CL in OCaml as follows:
In order to fully reduce a term, we need to be able to reduce redexes
that are not at the top level of the term.
- (II)I ~~> IK ~~> K
+ (II)K ~~> IK ~~> K
That is, we want to be able to first evaluate the redex `II` that is
a proper subpart of the larger term, to produce a new intermediate term
Because the top-level term is not a redex, `reduce1` returns it
without any evaluation. What we want is to evaluate the subparts of a
-complex term.
+complex term. We'll do this by mapping the reduction function onto
+the parts of a complex term.
let rec reduce2 (t:term):term = match t with
I -> I
if (is_redex t') then reduce2 (reduce_one_step t')
else t'
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it (the first three
-match cases). If the input is complex, we first process the
-subexpressions, and only then see if we have a redex. To understand
-how this works, follow the trace carefully:
+Since what we need is access to the subterms, we do pattern matching
+on the input term. If the input is simple (the first three `match`
+cases), we return it without further processing. But if the input is
+complex, we first process the subexpressions, and only then see if we
+have a redex at the top level. To understand how this works, follow
+the trace carefully:
# reduce2 (FA(FA(I,I),K));;
reduce2 <-- FA (FA (I, I), K)
reduce2 --> I
reduce2 <-- I
reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
+ reduce2 <-- I
+ reduce2 --> I
reduce2 --> I
- reduce2 <-- K ; fourth
+ reduce2 <-- K ; third
reduce2 --> K
reduce2 --> K
- : term = K
Ok, there's a lot going on here. Since the input is complex, the
first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
+it must reduce the two main subexpressions, `II` and `K`.
+
+There are three recursive calls to the reduce2 function, each of
+which gets triggered during the processing of this example. They have
+been marked in the trace.
+
+The don't quite go in the order in which they appear in the code,
+however! We see from the trace that it begins with the right-hand
+expression, `K`. We didn't explicitly tell it to begin with the
+right-hand subexpression, so control over evaluation order is starting
+to spin out of our control. (We'll get it back later, don't worry.)
In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
+result is `I`.
At this point, we have constructed `t' == FA(I,K)`. Since that's a
redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
+result. The third recursive call checks that there is no more
reduction work to be done (there isn't), and that's our final result.
You can see in more detail what is going on by tracing both reduce2
*How can we can we specify the evaluation order of a computational
system in a way that is completely insensitive to the evaluation order
of the specification language?*
+
+[By the way, the evaluators given here are absurdly inefficient computationally.
+Some computer scientists have trouble even looking at code this inefficient, but
+the emphasis here is on getting the concepts across as simply as possible.]