projects
/
lambda.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
8dc497d
)
(no commit message)
author
chris
<chris@web>
Sat, 14 Mar 2015 17:39:05 +0000
(13:39 -0400)
committer
Linux User
<ikiwiki@localhost.members.linode.com>
Sat, 14 Mar 2015 17:39:05 +0000
(13:39 -0400)
topics/_week7_eval_cl.mdwn
patch
|
blob
|
history
diff --git
a/topics/_week7_eval_cl.mdwn
b/topics/_week7_eval_cl.mdwn
index
4d1b3e7
..
8349a40
100644
(file)
--- a/
topics/_week7_eval_cl.mdwn
+++ b/
topics/_week7_eval_cl.mdwn
@@
-29,7
+29,7
@@
One thing we'll see is that it is all too easy for the evaluation
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
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. Th
at is, th
e 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.
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.
@@
-84,7
+84,7
@@
With sum types, we can define CL terms in OCaml as follows:
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
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
s
komega, as well as other terms whose
+definition, we can encode
S
komega, 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
reduction behavior we want to try to control.
Using pattern matching, it is easy to code the one-step reduction
@@
-103,13
+103,13
@@
rules for CL:
The definition of `reduce_one_step` explicitly says that it expects
its input argument `t` to have type `term`, and the second `:term`
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
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
`s
komega ~~>
+reduction rules for CL. The OCaml interpreter
responses given above show
us that the
+function faithfully recognizes that `KSI ~~> S`, and
that `S
komega ~~>
I(SII)(I(SII))`.
We can now say precisely what it means to be a redex in CL.
I(SII)(I(SII))`.
We can now say precisely what it means to be a redex in CL.
@@
-143,7
+143,7
@@
that are not at the top level of the term.
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
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
about how recursion works.
We'll develop our full reduction function in two stages. Once we have
@@
-162,7
+162,7
@@
allowing the evaluator to recognize that
I (I K) ~~> I K ~~> K
When trying to understand how recursive functions work, it can be
I (I K) ~~> I K ~~> K
When trying to understand how recursive functions work, it can be
-extremely helpful to examin
ing
an execution trace of inputs and
+extremely helpful to examin
e
an execution trace of inputs and
outputs.
# #trace reduce_stage1;;
outputs.
# #trace reduce_stage1;;
@@
-196,8
+196,10
@@
But the reduction function as written above does not deliver this result:
# reduce_stage1 (App (App (I, I), K));;
- : term = App (App (I, I), K)
# 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.
evaluate the subparts of a complex term. We'll do this by evaluating
the subparts of the top-level expression.
@@
-214,7
+216,9
@@
Since we need access to the subterms, we do pattern matching on the
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
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));;
carefully:
# reduce (App(App(I,I),K));;
@@
-262,7
+266,7
@@
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 reduce
and reduce_one_step, but that makes for some long traces.
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
K`, as desired.
Because the OCaml interpreter evaluates each subexpression in the
@@
-277,7
+281,7
@@
the only way to get out is to kill the interpreter with control-c.
Instead of performing the leftmost reduction first, and recognizing
that this term reduces to the normal form `I`, we get lost endlessly
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
s
komega.
+trying to reduce
S
komega.
## Laziness is hard to overcome
## Laziness is hard to overcome