order properties of an evaluator to depend on the evaluation order
properties of the programming language in which the evaluator is
written. We would like to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
+evaluation is insensitive to the evaluator language. That is, the goal is to
find an order-insensitive way to reason about evaluation order. We
will not fully succeed in this first attempt, but we will make good
progress.
This type definition says that a term in CL is either one of the three
simple expressions (`I`, `K`, or `S`), or else a pair of CL
expressions. `App` stands for Functional Application. With this type
-definition, we can encode skomega, as well as other terms whose
+definition, we can encode Skomega, as well as other terms whose
reduction behavior we want to try to control.
Using pattern matching, it is easy to code the one-step reduction
The definition of `reduce_one_step` explicitly says that it expects
its input argument `t` to have type `term`, and the second `:term`
-says that the type of the output it delivers as a result will be of
+says that the type of the output the function delivers as a result will also be of
type `term`.
The type constructor `App` obscures things a bit, but it's still
possible to see how the one-step reduction function is just the
-reduction rules for CL. The OCaml interpreter shows us that the
-function faithfully recognizes that `KSI ~~> S`, and `skomega ~~>
+reduction rules for CL. The OCaml interpreter responses given above show us that the
+function faithfully recognizes that `KSI ~~> S`, and that `Skomega ~~>
I(SII)(I(SII))`.
We can now say precisely what it means to be a redex in CL.
Because we need to process subparts, and because the result after
processing a subpart may require further processing, the recursive
structure of our evaluation function has to be somewhat subtle. To
-truly understand, you will need to do some sophisticated thinking
+truly understand, we will need to do some sophisticated thinking
about how recursion works.
We'll develop our full reduction function in two stages. Once we have
I (I K) ~~> I K ~~> K
When trying to understand how recursive functions work, it can be
-extremely helpful to examining an execution trace of inputs and
+extremely helpful to examine an execution trace of inputs and
outputs.
# #trace reduce_stage1;;
# reduce_stage1 (App (App (I, I), K));;
- : term = App (App (I, I), K)
-Because the top-level term is not a redex to start with,
-`reduce_stage1` returns it without any evaluation. What we want is to
+The reason is that the top-level term is not a redex to start with,
+so `reduce_stage1` returns it without any evaluation.
+
+What we want is to
evaluate the subparts of a complex term. We'll do this by evaluating
the subparts of the top-level expression.
input. 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
+at the top level.
+
+To understand how this works, follow the trace
carefully:
# reduce (App(App(I,I),K));;
You can see in more detail what is going on by tracing both reduce
and reduce_one_step, but that makes for some long traces.
-So we've solved our first problem: reduce recognizes that `IIK ~~>
+So we've solved our first problem: `reduce` now recognizes that `IIK ~~>
K`, as desired.
Because the OCaml interpreter evaluates each subexpression in the
Instead of performing the leftmost reduction first, and recognizing
that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
+trying to reduce Skomega.
## Laziness is hard to overcome