> 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
Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic:
-
-Let's say that for any lambda term T, [T] is the equivalent Combinatory Logic term. Then we define the [.] mapping as follows.
-
- 1. [a] = a
- 2. [(\aX)] = @a[X]
- 3. [(XY)] = ([X][Y])
-
-Wait, what is that @a ... business? Well, that's another operation on (a variable and) a CL expression, that we can define like this:
-
- 4. @aa = I
- 5. @aX = KX if a is not in X
- 6. @a(Xa) = X if a is not in X
- 7. @a(XY) = S(@aX)(@aY)
-
-
-
-
<ol start=19>
<li><code>[\x x] = @x x = I</code>
<li><code>[\x y. x] = @x [\y. x] = @x. (@y x) = @x (Kx) = S (@x K) (@x x) = S (KK) I</code>; in general expressions of this form <code>S(K<i>M</i>)I</code> will behave just like <code><i>M</i></code> for any expression <code><i>M</i></code>
25. For each of the above translations, how many `I`s are there? Give a rule for describing what each `I` corresponds to in the original lambda term.
+ This generalization depends on you omitting the translation rule:
+
+ 6. @a(Xa) = X if a is not in X
+
+ > With that shortcut rule omitted, then there turn out to be one `I` in the result corresponding to each occurrence of a bound variable in the original term.
+
Evaluation strategies in Combinatory Logic
------------------------------------------
<OL start=30>
<LI><code>(\x. x (\y. y x)) (v w) ~~> v w (\y. y (v w))</code>
<LI><code>(\x. x (\x. y x)) (v w) ~~> v w (\x. y x)</code>
-<LI><code>(\x. x (\y. y x)) (v x) ~~> v w (\y. y (v x))</code>
-<LI><code>(\x. x (\y. y x)) (v y) ~~> v w (\u. u (v y))</code>
+<LI><code>(\x. x (\y. y x)) (v x) ~~> v x (\y. y (v x))</code>
+<LI><code>(\x. x (\y. y x)) (v y) ~~> v y (\u. u (v y))</code>
<LI><code>(\x y. x y y) u v ~~> u v v</code>
<LI><code>(\x y. y x) (u v) z w ~~> z (u v) w</code>