+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.
+
+
+## Numbers
+
+9. Recall our proposed encoding for the numbers, called "Church's encoding". As we explained last week, it's similar to our proposed encoding of lists in terms of their folds. Give a Lambda Calculus definition of `zero?` for numbers so encoded. (It should require only small modifications to your solution for `empty?`, above.)
+
+10. In last week's homework, you gave a Lambda Calculus definition of `succ` for Church-encoded numbers. Can you now define `pred`? Let `pred 0` result in whatever `err` is bound to. This is challenging. For some time theorists weren't sure it could be done. (Here is [some interesting commentary](http://okmij.org/ftp/Computation/lambda-calc.html#predecessor).) However, in this week's notes we examined one strategy for defining `tail` for our chosen encodings of lists, and given the similarities we explained between lists and numbers, perhaps that will give you some guidance in defining `pred` for numbers.
+
+ (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.)
+
+
+
+11. Define `leq` for numbers (that is, ≤) in the Lambda Calculus. Here is the expected behavior,
+where `one` abbreviates `succ zero`, and `two` abbreviates `succ (succ zero)`.
+
+ leq zero zero ~~> true
+ leq zero one ~~> true
+ leq zero two ~~> true
+ leq one zero ~~> false
+ leq one one ~~> true
+ leq one two ~~> true
+ leq two zero ~~> false
+ leq two one ~~> false
+ leq two two ~~> true
+ ...
+
+ You'll need to make use of the predecessor function, but it's not essential to understanding this problem that you have successfully implemented it yet. You can treat it as a black box.
+
+## Combinatory Logic
+
+Reduce the following forms, if possible:
+
+<ol start=12>
+<li><code>Kxy</code>
+<li><code>KKxy</code>
+<li><code>KKKxy</code>
+<li><code>SKKxy</code>
+<li><code>SIII</code>
+<li><code>SII(SII)</code>
+</ol>
+
+<!-- -->
+
+18. Give Combinatory Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. Provide combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`.
+
+Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic:
+
+<ol start=19>
+<li><code>\x x</code>
+<li><code>\x y. x</code>
+<li><code>\x y. y</code>
+<li><code>\x y. y x</code>
+<li><code>\x. x x</code>
+<li><code>\x y z. x (y z)</code>
+</ol>
+
+<!-- -->
+
+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.
+
+Evaluation strategies in Combinatory Logic
+------------------------------------------
+
+26. Find a term in CL that behaves like Omega does in the Lambda
+Calculus. Call it `Skomega`.
+
+27. Are there evaluation strategies in CL corresponding to leftmost
+reduction and rightmost reduction in the Lambda Calculus?
+What counts as a redex in CL?
+
+28. Consider the CL term `K I Skomega`. Does leftmost (alternatively,
+rightmost) evaluation give results similar to the behavior of `K I
+Omega` in the Lambda Calculus, or different? What features of the
+Lambda Calculus and CL determine this answer?
+
+29. What should count as a thunk in CL? What is the equivalent
+constraint in CL to forbidding evaluation inside of a lambda abstract?
+
+
+More Lambda Practice
+--------------------
+
+Reduce to beta-normal forms:
+
+<OL start=30>
+<LI><code>(\x. x (\y. y x)) (v w)</code>
+<LI><code>(\x. x (\x. y x)) (v w)</code>
+<LI><code>(\x. x (\y. y x)) (v x)</code>
+<LI><code>(\x. x (\y. y x)) (v y)</code>
+
+<LI><code>(\x y. x y y) u v</code>
+<LI><code>(\x y. y x) (u v) z w</code>
+<LI><code>(\x y. x) (\u u)</code>
+<LI><code>(\x y z. x z (y z)) (\u v. u)</code>
+</OL>