> I'm not sure which of the two solutions presented here is better. The one given in the hint traverses the list only once; whereas the one gotten by reversing the list and getting the last member of the result traverses the list twice. But the former strategy does more complicated stuff at each step of the traversal (both conceptually and more applications), so in the end it might be computationally "cheaper" to use the latter strategy.
+ > Here is yet a third solution, which is probably the most efficient:
+ > let box = \a. \v. v a in
+ > let left_head = \xs. xs (\b x. (K (b (K x)))) (box err) I in
+ > ...
8. 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. How would you implement such a list comparison? You can write it in Scheme or Kapulet using `letrec`, or if you want more of a challenge, in the Lambda Calculus using your preferred encoding for lists. If you write it in Scheme, don't rely on applying the built-in comparison operator `equal?` to the lists themselves. (Nor on the operator `eqv?`, which might not do what you expect.) You can however rely on the comparison operator `=` which accepts only number arguments. If you write it in the Lambda Calculus, you can use your implementation of `leq?`, requested below, to write an equality operator for Church-encoded numbers. [[Here is a hint|assignment3 hint3]], if you need it.
> let pred = \n. n shift (pair 0 err) snd in
> ...
- > Here is another solution, due to Martin Bunder and F. Urbanek:
+ > Here is another solution, that is attributed variously to Martin Bunder and F. Urbanek, or J. Velmans:
- > let pred = \n. \s z. n (\u v. v (u s)) (K z) I in
+ > let box = \a. \v. v a in
+ > let pred = \n. \s z. n (\b. box (b s)) (K z) I in
> ...
- > That can be hard to wrap your head around. If you trace it through, you'll see that:
+ > That can be hard to wrap your head around. If you trace this expression through, you'll see that:
- > * when `n == 0`, it reduces to `\s z. (\v. z) I`, or `\s z. z`
- > * when `n == 1`, it reduces to `\s z. (\v. v z) I`, or `\s z. z`
- > * when `n == 2`, it reduces to `\s z. (\v. v (s z)) I`, or `\s z. s z`
- > * when `n == 3`, it reduces to `\s z. (\v. v (s (s z))) I`, or `\s z. s (s z)`
+ > * when `n == 0`, it reduces to `\s z. (K z) I`, or `\s z. z`
+ > * when `n == 1`, it reduces to `\s z. (box z) I`, or `\s z. z`
+ > * when `n == 2`, it reduces to `\s z. (box (s z)) I`, or `\s z. s z`
+ > * when `n == 3`, it reduces to `\s z. (box (s (s z))) I`, or `\s z. s (s z)`
- > The technique used here is akin to that used in [[the hint for last week's `reverse`|assignment2_answers#cps-reverse]].
+ > `box a` is `\v. v a`; this stands to `pair a b` as one stands to two. Since boxes (like pairs) are really just functions, the technique used in this definition of `pred` is akin to that used in [[the hint for last week's `reverse`|assignment2_answers#cps-reverse]].
(Want a further challenge? Define `map2` in the Lambda Calculus, using our right-fold encoding for lists, where `map2 g [a, b, c] [d, e, f]` should evaluate to `[g a d, g b e, g c f]`. Doing this will require drawing on a number of different tools we've developed, including that same strategy for defining `tail`. Purely extra credit.)
> let leq? = \l r. zero? (sub l r) in
> ...
- > Here is another solution. Jim crafted this particular implementation, but like a great deal of the CS knowledge he's gained over the past eight years, Oleg Kiselyov pointed the way.
+ > Here is another solution. Jim crafted this particular implementation, but like a great deal of the CS knowledge he's gained over the past eight years, Oleg Kiselyov pointed the way. <!-- see "lambda-calc-opposites.txt" at http://okmij.org/ftp/Computation/lambda-calc.html#neg -->
> let leq? = (\base build consume. \l r. r consume (l build base) fst)
> ; where base is