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?