A: Right:
<pre><code>let Y = \T. (\x. T (x x)) (\x. T (x x)) in
-Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
+Y Y
+≡ \T. (\x. T (x x)) (\x. T (x x)) Y
~~> (\x. Y (x x)) (\x. Y (x x))
~~> Y ((\x. Y (x x)) (\x. Y (x x)))
~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
-~~> Y (Y (Y (...(Y (Y Y))...)))</code></pre>
+~~> Y (Y (Y (...(Y (Y Y))...)))
+</code></pre>
#Q: Ouch! Stop hurting my brain.#
<pre><code>let succ = \n s z. s (n s z) in
let X = (\x. succ (x x)) (\x. succ (x x)) in
succ X
-≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x)) ))
-≡ succ (succ X)
+≡ succ (succ X)
</code></pre>
You should see the close similarity with `Y Y` here.
<pre><code>[same definitions]
succ X
-≡ (\n s z. s (n s z)) X
-~~> \s z. s (X s z)
+≡ (\n s z. s (n s z)) X
+~~> \s z. s (X s z)
<~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+≡ (\n s z. s (n s z)) (\s z. s (X s z))
+~~> \s z. s ((\s z. s (X s z)) s z)
+~~> \s z. s (s (X s z))
</code></pre>
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
<pre><code>let prefact = \f n. iszero n 1 (mul n (f (pred n))) in
let fact = Y prefact in
fact 2
-≡ [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
+≡ [(\f. (\x. f (x x)) (\x. f (x x))) prefact] 2
~~> [(\x. prefact (x x)) (\x. prefact (x x))] 2
~~> [prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 2
~~> [prefact (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
-≡ [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
+≡ [ (\f n. iszero n 1 (mul n (f (pred n)))) (prefact ((\x. prefact (x x)) (\x. prefact (x x))))] 2
~~> [\n. iszero n 1 (mul n ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred n)))] 2
~~> iszero 2 1 (mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 2)))
~~> mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 1)
...
~~> mul 2 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 0))
-≡ mul 2 (mul 1 (iszero 0 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0))))
+≡ mul 2 (mul 1 (iszero 0 1 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0)))))
~~> mul 2 (mul 1 1)
~~> mul 2 1
~~> 2
we can stop. If we haven't found `5` already, we know it's not in the rest of the
list either.
-This is an improvement, but it's still a "linear" search through the list.
+*Comment*: This is an improvement, but it's still a "linear" search through the list.
There are even more efficient methods, which employ "binary" searching. They'd
represent the set in such a way that you could quickly determine whether some
element fell in one half, call it the left half, of the structure that
for whichever quarter you were directed to next. And so on. Until you either
found the element or exhausted the structure and could then conclude that the
element in question was not part of the set. These sorts of structures are done
-using **binary trees** (see below).
+using [binary trees](/implementing_trees).
#Aborting a search through a list#
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 normal-order 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 fixed-point combinators
+`Y` or <code>Θ</code>. Expressions using them will have non-terminating
+reductions, with Scheme's eager/call-by-value strategy. There are other
+fixed-point combinators you can use with Scheme (in the [week 3 notes](/week3/#index7h2) they
+were <code>Y′</code> and <code>Θ′</code>. But even with
+them, evaluation order still matters: for some (admittedly unusual)
+evaluation strategies, expressions using them will also be non-terminating.
+
+The fixed-point 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.)
+
+This is why the v3 lists and numbers are so lovely..
+
+--
+
But what if you're using v3 lists? What options would you have then for
aborting a search?