XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=b174581d30a1ca0ce3ca8ba61ab5639b473dc0da;hp=150e88354cd7f8b56884ffe201e3afd1255693ba;hb=6131a5f57f675f9dcafcb3a4ec9d3613a0e29726;hpb=43a168d149dd549338cd3f8b59c85bef3ba4de20
diff git a/week4.mdwn b/week4.mdwn
index 150e8835..b174581d 100644
 a/week4.mdwn
+++ b/week4.mdwn
@@ 276,39 +276,39 @@ can just deliver that answer, and not branch into any further recursion. If
you've got the right evaluation strategy in place, everything will work out
fine.

An advantage of the v3 lists and v3 (aka "Church") numerals is that they
have a recursive capacity built into their skeleton. So for many natural
operations on them, you won't need to use a fixed point combinator. Why is
that an advantage? Well, if you use a fixed point combinator, then the terms
you get
won't be strongly normalizing: whether their reduction stops at a normal form
will depend on what evaluation order you use. Our online [[lambda evaluator]]
uses normalorder reduction, so it finds a normal form if there's one to be
had. But if you want to build lambda terms in, say, Scheme, and you wanted to
roll your own recursion as we've been doing, rather than relying on Scheme's
native `let rec` or `define`, then you can't use the fixedpoint combinators
`Y` or Θ
. Expressions using them will have nonterminating
reductions, with Scheme's eager/callbyvalue strategy. There are other
fixedpoint combinators you can use with Scheme (in the [week 3 notes](/week3/#index7h2) they
were Y′
and Θ′
. But even with
them, evaluation order still matters: for some (admittedly unusual)
evaluation strategies, expressions using them will also be nonterminating.

The fixedpoint combinators may be the conceptual stars. They are cool and
+But what if we wanted to use v3 lists instead?
+
+> Why would we want to do that? The advantage of the v3 lists and v3 (aka
+"Church") numerals is that they have their recursive capacity built into their
+very bones. So for many natural operations on them, you won't need to use a fixed
+point combinator.
+
+> Why is that an advantage? Well, if you use a fixed point combinator, then
+the terms you get won't be strongly normalizing: whether their reduction stops
+at a normal form will depend on what evaluation order you use. Our online
+[[lambda evaluator]] uses normalorder reduction, so it finds a normal form if
+there's one to be had. But if you want to build lambda terms in, say, Scheme,
+and you wanted to roll your own recursion as we've been doing, rather than
+relying on Scheme's native `let rec` or `define`, then you can't use the
+fixedpoint combinators `Y` or Θ
. Expressions using them
+will have nonterminating reductions, with Scheme's eager/callbyvalue
+strategy. There are other fixedpoint combinators you can use with Scheme (in
+the [week 3 notes](/week3/#index7h2) they were Y′
and
+Θ′
. But even with them, evaluation order still
+matters: for some (admittedly unusual) evaluation strategies, expressions using
+them will also be nonterminating.
+
+> The fixedpoint combinators may be the conceptual stars. They are cool and
mathematically elegant. But for efficiency and implementation elegance, it's
best to know how to do as much as you can without them. (Also, that knowledge
could carry over to settings where the fixed point combinators are in
principle unavailable.)
+could carry over to settings where the fixed point combinators are in principle
+unavailable.)
This is why the v3 lists and numbers are so lovely..

+So again, what if we're using v3 lists? What options would we have then for
+aborting a search or list traversal before it runs to completion?
But what if you're using v3 lists? What options would you have then for
aborting a search?

Well, suppose we're searching through the list `[5;4;3;2;1]` to see if it
+Suppose we're searching through the list `[5;4;3;2;1]` to see if it
contains the number `3`. The expression which represents this search would have
something like the following form: