/.ikiwiki
/recentchanges
-/.*.swp
+.*.swp
#Version 4 lists: Efficiently extracting tails#
-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. However, one disadvantage
+Version 3 lists and Church numerals are lovely, because they have their recursive capacity built into their very bones. However, one disadvantage
to them is that it's relatively inefficient to extract a list's tail, or get a
number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will
basically be performing some operation that builds up the tail afresh: at
let false = \x y. y in
let and = \l r. l (r true false) false in
- ; version 1 lists
let make_pair = \f s g. g f s in
- let fst = true in
- let snd = false in
+ let get_fst = true in
+ let get_snd = false in
let empty = make_pair true junk in
- let isempty = \x. x fst in
+ let isempty = \x. x get_fst in
let make_list = \h t. make_pair false (make_pair h t) in
- let head = \l. isempty l err (l snd fst) in
- let tail = \l. isempty l err (l snd snd) in
-
+ let head = \l. isempty l err (l get_snd get_fst) in
+ let tail = \l. isempty l err (l get_snd get_snd) in
+
; a list of numbers to experiment on
let mylist = make_list 1 (make_list 2 (make_list 3 empty)) in
-
- ; a fixed-point combinator for defining recursive functions
- let Y = \f. (\h. f (h h)) (\h. f (h h)) in
-
+
; church numerals
let iszero = \n. n (\x. false) true in
let succ = \n s z. s (n s z) in
- let mult = \m n s. m (n s) in
- let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in
- let pred = \n. iszero n 0 (length (tail (n (\p. make_list junk p) empty)))
- in
+ let mul = \m n s. m (n s) in
+ let pred = (\shift n. n shift (make\_pair 0 0) get\_snd) (\p. p (\x y. make\_pair (succ x) x)) in
let leq = \m n. iszero(n pred m) in
let eq = \m n. and (leq m n)(leq n m) in
-
+
+ ; a fixed-point combinator for defining recursive functions
+ let Y = \f. (\h. f (h h)) (\h. f (h h)) in
+ let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in
+
eq 2 2 yes no
trees.
<OL start=6>
-<LI>Write a function that sums the number of leaves in a tree.
+<LI>Write a function that sums the values at the leaves in a tree.
Expected behavior:
-Assignment 4
-------------
-
#Reversing a list#
-How would you define an operation to reverse a list? (Don't peek at the
+<OL>
+<LI>How would you define an operation to reverse a list? (Don't peek at the
[[lambda_library]]! Try to figure it out on your own.) Choose whichever
implementation of list you like. Even then, there are various strategies you
can use.
+(See [[hints/Assignment 4 hint 1]] if you need some hints.)
+</OL>
+
#Comparing lists for equality#
-<!--
-let list_equal =
- \left right. left
- ; here's our f
- (\hd sofar.
- ; deconstruct our sofar-pair
- sofar (\might_be_equal right_tail.
- ; our new sofar
- make_pair
- (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
- (tail right_tail)
- ))
- ; here's our z
- ; we pass along the fold a pair
- ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
- ; when left is empty, the lists are equal if right is empty
- (make_pair
- (not (isempty right))
- (reverse right)
- )
- ; when fold is finished, check sofar-pair
- (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
--->
+
+<OL start=2>
+<LI>Suppose you have two lists of integers, `left` and `right`. You want to determine whether those lists are equal: that is, whether they have all the same members in the same order. (Equality for the lists we're working with is *extensional*, or parasitic on the equality of their members, and the list structure. Later in the course we'll see lists which aren't extensional in this way.)
+
+How would you implement such a list comparison?
+
+(See [[hints/Assignment 4 hint 2]] if you need some hints.)
+</OL>
+
#Enumerating the fringe of a leaf-labeled tree#
-[[Implementing trees]]
+First, read this: [[Implementing trees]]
+
+<OL start=3>
+<LI>blah
+
+(See [[hints/Assignment 4 hint 3]] if you need some hints.)
+</OL>
+
+
+#Mutually-recursive functions#
+
+<OL start=4>
+<LI>(Challenging.) One way to define the function `even` is to have it hand off part of the work to another function `odd`:
+
+ let even = \x. iszero x
+ ; if x == 0 then result is
+ true
+ ; else result turns on whether x's pred is odd
+ (odd (pred x))
+
+At the same tme, though, it's natural to define `odd` in such a way that it hands off part of the work to `even`:
+
+ let odd = \x. iszero x
+ ; if x == 0 then result is
+ false
+ ; else result turns on whether x's pred is even
+ (even (pred x))
+
+Such a definition of `even` and `odd` is called **mutually recursive**. If you trace through the evaluation of some sample numerical arguments, you can see that eventually we'll always reach a base step. So the recursion should be perfectly well-grounded:
+
+ even 3
+ ~~> iszero 3 true (odd (pred 3))
+ ~~> odd 2
+ ~~> iszero 2 false (even (pred 2))
+ ~~> even 1
+ ~~> iszero 1 true (odd (pred 1))
+ ~~> odd 0
+ ~~> iszero 0 false (even (pred 0))
+ ~~> false
+
+But we don't yet know how to implement this kind of recursion in the lambda calculus.
+
+The fixed point operators we've been working with so far worked like this:
+
+ let X = Y T in
+ X <~~> T X
+
+Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on a *pair* of functions `T1` and `T2`, as follows:
+
+ let X1 = Y1 T1 T2 in
+ let X2 = Y2 T1 T2 in
+ X1 <~~> T1 X1 X2 and
+ X2 <~~> T2 X1 X2
+
+If we gave you such a `Y1` and `Y2`, how would you implement the above definitions of `even` and `odd`?
+
+
+<LI>(More challenging.) Using our derivation of Y from the [[Week2]] notes as a model, construct a pair `Y1` and `Y2` that behave in the way described.
+(See [[hints/Assignment 4 hint 4]] if you need some hints.)
+</OL>
let false = \x y. y in
let and = \l r. l (r true false) false in
let or = \l r. l true r in
-let make_pair = \f s g. g f s in
-let get_fst = true in
-let get_snd = false in
-let empty = make_pair true junk in
-let isempty = \x. x get_fst in
-let make_list = \h t. make_pair false (make_pair h t) in
-let head = \l. isempty l err (l get_snd get_fst) in
-let tail = \l. isempty l err (l get_snd get_snd) in
+;
+let make\_pair = \f s g. g f s in
+let get\_fst = true in
+let get\_snd = false in
+let empty = make\_pair true junk in
+let isempty = \x. x get\_fst in
+let make\_list = \h t. make\_pair false (make\_pair h t) in
+let head = \l. isempty l err (l get\_snd get\_fst) in
+let tail = \l. isempty l err (l get\_snd get\_snd) in
;
; a list of numbers to experiment on
-let mylist = make_list 1 (make_list 2 (make_list 3 empty)) in
+let mylist = make\_list 1 (make\_list 2 (make\_list 3 empty)) in
;
; church numerals
let iszero = \n. n (\x. false) true in
let succ = \n s z. s (n s z) in
let mul = \m n s. m (n s) in
-let pred = (\shift n. n shift (make_pair 0 0) get_snd) (\p. p (\x y. make_pair (succ x) x)) in
+let pred = (\shift n. n shift (make\_pair 0 0) get\_snd) (\p. p (\x y. make\_pair (succ x) x)) in
let leq = \m n. iszero(n pred m) in
let eq = \m n. and (leq m n)(leq n m) in
;
let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in
;
; synonyms
-let makePair = make_pair in
-let fst = get_fst in
-let snd = get_snd in
+let makePair = make\_pair in
+let fst = get\_fst in
+let snd = get\_snd in
let nil = empty in
let isNil = isempty in
-let makeList = make_list in
+let makeList = make\_list in
let isZero = iszero in
let mult = mul in
;
;
length (tail mylist)
</textarea>
+
<input id="PARSE" value="Normalize" type="button">
<input id="ETA" type="checkbox">do eta-reductions too
<noscript><p>You may not see it because you have JavaScript turned off. Uffff!</p></noscript>
--- /dev/null
+Hints for reverse.
+
+* If left and right are two v3 lists, what is the result of:
+
+ left make_list right
+
+* What is `reverse []`? What is `reverse [c]`? What is `reverse [b;c]`? How is it related to `reverse [c]`?
+
+* How is `reverse [a;b;c]` related to `reverse [b;c]`?
+
+* Getting any ideas?
+
+
+Another strategy.
+
+* Our version 3 lists are _right_-folds. That is, `[a;b;c]` is implemented as:
+
+ \f z. f a (f b (f c z))
+
+ which is the result of first combining the base value `z` with the rightmost element of the list, using `f`, then combining the result of that with the next element to the left, and so on.
+
+ A _left_-fold on the same list would be:
+
+ \f z. f (f (f z a) b) c
+
+ which is the result of first combining the base value `z` with the leftmost element of the list, then combining the result of that with the next element to the right, and so on.
+
+ It's conventional for `f` to take the accumulated value so far as its second argument when doing a right-fold, and for it to take it as its first argument when doing a left-fold. However, this convention could be ignored. We could also call this the left-fold of `[a;b;c]`:
+
+ \f z. f c (f b (f a z))
+
+* Getting any ideas?
+
+* Our `make_list` function for taking an existing, right-fold-based list, and a new element, and returning a new right-fold-based list, looks like this:
+
+ let make_list = \hd tl. \f z. f hd (tl f z)
+
+ How would you write a `make_left_list` function, that takes an existing, left-fold-based list, like `\f z. f c (f b z)`, and a new element, `a`, and returned the new, left-fold based list:
+
+ \f z. f c (f b (f a z))
+
+
--- /dev/null
+Hints for list\_equal.
+
+<!--
+let list_equal =
+ \left right. left
+ ; here's our f
+ (\hd sofar.
+ ; deconstruct our sofar-pair
+ sofar (\might_be_equal right_tail.
+ ; our new sofar
+ make_pair
+ (and (and might_be_equal (not (isempty right_tail))) (eq? hd (head right_tail)))
+ (tail right_tail)
+ ))
+ ; here's our z
+ ; we pass along the fold a pair
+ ; (might_for_all_i_know_still_be_equal?, tail_of_reversed_right)
+ ; when left is empty, the lists are equal if right is empty
+ (make_pair
+ true ; for all we know so far, they might still be equal
+ (reverse right)
+ )
+ ; when fold is finished, check sofar-pair
+ (\might_be_equal right_tail. and might_be_equal (isempty right_tail))
+-->
--- /dev/null
+Hints for enumerating a tree's fringe.
+
--- /dev/null
+Hints for Y1,Y2.
+
However, when using trees as a computational tool, one usually does have
latitude about how to structure a larger tree---in the same way that we had the
-freedom to implement our sets with lists whose members were just appended in
-the order we built the set up, or instead with lists whose members were ordered
-numerically.
+freedom to implement our [sets](/week4/#index9h1) with lists whose members were
+just appended in the order we built the set up, or instead with lists whose
+members were ordered numerically.
When building a new tree, one strategy for where to put the new element and
where to put the existing tree would be to always lean towards a certain side.
* We'll shortly be posting another assignment, assignment 4, which will be
"due" on the Sunday before our next seminar. That is, on Sunday Oct 17.
-(There's no seminar this coming Monday.)
+(There's no seminar on Monday Oct 11.)
The assignments will tend to be quite challenging. Again, you should by
all means talk amongst yourselves, and to us, about strategies and
(13 Sept) Lecture notes for [[Week1]]; [[Assignment1]].
-Topics: Applications; Basics of Lambda Calculus; Comparing Different Languages
+> Topics: [[Applications]], including [[Damn]]; Basics of Lambda Calculus; Comparing Different Languages
(20 Sept) Lecture notes for [[Week2]]; [[Assignment2]].
-Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; Lists and Numbers
+> Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; [[Lists and Numbers]]
(27 Sept) Lecture notes for [[Week3]]; [[Assignment3]];
an evaluator with the definitions used for homework 3
preloaded is available at [[assignment 3 evaluator]].
-Topics: Recursion with Fixed Point Combinators
+> Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators
-(4 Oct) Lecture notes for Week 4
+(4 Oct) Lecture notes for [[Week4]]; Assignment4
-<!-- Introducing the notion of a "continuation", which technique we'll now already have used a few times
--->
+> Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]]
+
+
+(18 Oct) Lecture notes for Week 5
+
+> Topics: Types, Polymorphism
[[Upcoming topics]]
+[Advanced Lambda Calculus Topics](/advanced lambda)
+
##[[Offsite Reading]]##
This wiki is powered by [[ikiwiki]].
-[[Test]]
; pairs
let make_pair = \x y f. f x y in
- let get_1st = \x y. x in ; aka true
- let get_2nd = \x y. y in ; aka false
+ let get_fst = \x y. x in ; aka true
+ let get_snd = \x y. y in ; aka false
; triples
let make_triple = \x y z f. f x y z in
let isempty = \lst. lst (\h sofar. false) true in
let head = \lst. lst (\h sofar. h) junk in
let tail_empty = empty in
- let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_2nd)
+ let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd)
; where shift is
(\h p. p (\t y. make_pair (make_list h t) t)) in
let length = \lst. lst (\h sofar. succ sofar) 0 in
let empty = make_pair true junk in
let make_list = \h t. make_pair false (make_pair h t) in
- let isempty = \lst. lst get_1st in
- let head = \lst. isempty lst err (lst get_2nd get_1st) in
+ let isempty = \lst. lst get_fst in
+ let head = \lst. isempty lst err (lst get_snd get_fst) in
let tail_empty = empty in
- let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in
+ let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in
; more math with Church numerals
; three strategies for predecessor
let pred_zero = zero in
- let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
+ let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd)
; where shift is
(\p. p (\x y. make_pair (succ x) x)) in ; or
; from Oleg; observe that for any Church numeral n: n I ~~> I
; more efficient comparisons, Oleg's gt provided some simplifications
- let leq = (\base build consume. \m n. n consume (m build base) get_1st)
+ let leq = (\base build consume. \m n. n consume (m build base) get_fst)
; where base is
(make_pair true junk)
; and build is
(\p. make_pair false p)
; and consume is
- (\p. p get_1st p (p get_2nd)) in
+ (\p. p get_fst p (p get_snd)) in
let lt = \m n. not (leq n m) in
- let eq = (\base build consume. \m n. n consume (m build base) get_1st)
+ let eq = (\base build consume. \m n. n consume (m build base) get_fst)
; 2nd element of a pair will now be of the form (K sthg) or I
; we supply the pair being consumed itself as an argument
; getting back either sthg or the pair we just consumed
; and build is
(\p. make_pair false (K p))
; and consume is
- (\p. p get_2nd p) in
+ (\p. p get_snd p) in
; -n is a fixedpoint of \x. add (add n x) x
(make_triple (succ cur) false (succ sofar)) ; continue
)) in
; or
- let sub = (\base build consume. \m n. n consume (m build base) get_1st)
+ let sub = (\base build consume. \m n. n consume (m build base) get_fst)
; where base is
(make_pair zero I) ; see second defn of eq for explanation of 2nd element
; and build is
(\p. p (\x y. make_pair (succ x) (K p)))
; and consume is
- (\p. p get_2nd p) in
+ (\p. p get_snd p) in
let min = \m n. sub m (sub m n) in
; and mtail is
(\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
in
- let div = \n d. divmod n d get_1st in
- let mod = \n d. divmod n d get_2nd in
+ let div = \n d. divmod n d get_fst in
+ let mod = \n d. divmod n d get_snd in
; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
<!--
; my original efficient comparisons
- let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
+ let leq = (\base build consume. \m n. n consume (m build base) get_fst (\x. false) true)
; where base is
(make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
; and build is
(\p. p (\x y. make_pair (succ x) (K p))) ; supplying the made pair as an arg to its 2nd term returns p (the previous pair)
; and consume is
- (\p. p get_2nd p) in
+ (\p. p get_snd p) in
let lt = \m n. not (leq n m) in
let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
; where base is
; and build is
(\p. p (\x y. make_pair (succ x) (K p)))
; and consume is
- (\p. p get_2nd p) in ; or
+ (\p. p get_snd p) in ; or
-->
<!--
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
-≡ (\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))
+≡ (\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.
-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
+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 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.)
+
+
+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?
+
+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:
is computed by. Conceptually, it will be easiest if we think of the reduction
happening in the order displayed above.
-Well, once we've found a match between our sought number `3` and some member of
+Once we've found a match between our sought number `3` and some member of
the list, we'd like to avoid any further unnecessary computations and just
deliver the answer `true` as "quickly" or directly as possible to the larger
computation in which the search was embedded.
understanding of the v2 lists will give you a helpful model.
In broad outline, a single stage of the search would look like before, except
-now f would receive two extra, "handler" arguments.
+now `f` would receive two extra, "handler" arguments.
f 3 <result of folding f and z over [2; 1]> <handler to continue folding leftwards> <handler to abort the traversal>
of the list multiplied to, because that would affect the answer you passed
along to the continue-leftwards handler.
-A **version 5** list encodes the kind of fold operation we're envisaging here, in
-the same way that v3 (and [v4](/advanced/#index1h1)) lists encoded the simpler fold operation.
-Roughly, the list `[5;4;3;2;1]` would look like this:
+A **version 5** list encodes the kind of fold operation we're envisaging here,
+in the same way that v3 (and [v4](/advanced_lambda/#index1h1)) lists encoded
+the simpler fold operation. Roughly, the list `[5;4;3;2;1]` would look like
+this:
\f z continue_leftwards_handler abort_handler.
discusses it in much more
detail](http://okmij.org/ftp/Streams.html#enumerator-stream).
-*Comments*:
-
-1. The technique deployed here, and in the v2 lists, and in our implementations
- of pairs and booleans, is known as **continuation-passing style** programming.
-
-2. We're still building the list as a right fold, so in a sense the
- application of `f` to the leftmost element `5` is "outermost". However,
- this "outermost" application is getting lifted, and passed as a *handler*
- to the next right application. Which is in turn getting lifted, and
- passed to its next right application, and so on. So if you
- trace the evaluation of the `extract_head` function to the list `[5;4;3;2;1]`,
- you'll see `1` gets passed as a "this is the head sofar" answer to its
- `continue_handler`; then that answer is discarded and `2` is
- passed as a "this is the head sofar" answer to *its* `continue_handler`,
- and so on. All those steps have to be evaluated to finally get the result
- that `5` is the outer/leftmost head of the list. That's not an efficient way
- to get the leftmost head.
-
- We could improve this by building lists as left folds when implementing them
- as continuation-passing style folds. We'd just replace above:
-
- let make_list = \h t. \f z continue_handler abort_handler.
- f h z (\z. t f z continue_handler abort_handler) abort_handler
-
- now `extract_head` should return the leftmost head directly, using its `abort_handler`:
-
- let extract_head = \lst larger_computation. lst
- (\hd sofar continue_handler abort_handler. abort_handler hd)
- junk
- larger_computation
- larger_computation
-
-3. To extract tails efficiently, too, it'd be nice to fuse the apparatus developed
- in these v5 lists with the ideas from [v4](/advanced/#index1h1) lists.
- But that also is left as an exercise.
+> *Comments*:
+
+> 1. The technique deployed here, and in the v2 lists, and in our
+> implementations of pairs and booleans, is known as
+> **continuation-passing style** programming.
+
+> 2. We're still building the list as a right fold, so in a sense the
+> application of `f` to the leftmost element `5` is "outermost". However,
+> this "outermost" application is getting lifted, and passed as a *handler*
+> to the next right application. Which is in turn getting lifted, and
+> passed to its next right application, and so on. So if you
+> trace the evaluation of the `extract_head` function to the list `[5;4;3;2;1]`,
+> you'll see `1` gets passed as a "this is the head sofar" answer to its
+> `continue_handler`; then that answer is discarded and `2` is
+> passed as a "this is the head sofar" answer to *its* `continue_handler`,
+> and so on. All those steps have to be evaluated to finally get the result
+> that `5` is the outer/leftmost head of the list. That's not an efficient way
+> to get the leftmost head.
+>
+> We could improve this by building lists as left folds when implementing them
+> as continuation-passing style folds. We'd just replace above:
+>
+> let make_list = \h t. \f z continue_handler abort_handler.
+> f h z (\z. t f z continue_handler abort_handler) abort_handler
+>
+> now `extract_head` should return the leftmost head directly, using its
+> `abort_handler`:
+>
+> let extract_head = \lst larger_computation. lst
+> (\hd sofar continue_handler abort_handler. abort_handler hd)
+> junk
+> larger_computation
+> larger_computation
+>
+> 3. To extract tails efficiently, too, it'd be nice to fuse the apparatus
+> developed in these v5 lists with the ideas from
+> [v4](/advanced_lambda/#index1h1) lists. But that is left as an exercise.
+
##The simply-typed lambda calculus##
-The uptyped lambda calculus is pure computation. It is much more
+The untyped lambda calculus is pure computation. It is much more
common, however, for practical programming languages to be typed.
Likewise, systems used to investigate philosophical or linguistic
issues are almost always typed. Types will help us reason about our