Lists and List Comprehensions

  1. In Kapulet, what does [ [x, 2*x] | x from [1, 2, 3] ] evaluate to?

  2. What does [ 10*x + y | y from [4], x from [1, 2, 3] ] evalaute to?

  3. Using either Kapulet's or Haskell's list comprehension syntax, write an expression that transforms [3, 1, 0, 2] into [3, 3, 3, 1, 2, 2]. Here is a hint, if you need it.

  4. Last week you defined head in terms of fold_right. Your solution should be straightforwardly translatable into one that uses our proposed right-fold encoding of lists in the Lambda Calculus. Now define empty? in the Lambda Calculus. (It should require only small modifications to your solution for head.)

  5. If we encode lists in terms of their left-folds, instead, [a, b, c] would be encoded as \f z. f (f (f z a) b) c. The empty list [] would still be encoded as \f z. z. What should cons be, for this encoding?

  6. Continuing to encode lists in terms of their left-folds, what should last be, where last [a, b, c] should result in c. Let last [] result in whatever err is bound to.

  7. Continuing to encode lists in terms of their left-folds, how should we write head? This is challenging. Here is a solution, if you need help.

  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, if you need it.

    (The function you're trying to define here is like eqlist? in Chapter 5 of The Little Schemer, though you are only concerned with lists of numbers, whereas the function from The Little Schemer also works on lists containing symbolic atoms --- and in the final version from that Chapter, also on lists that contain other, embedded lists.)


  1. 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.)

  2. 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.) 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.)

  3. 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:

  1. Kxy
  2. KKxy
  3. KKKxy
  4. SKKxy
  5. SIII
  6. SII(SII)
  1. 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:

  1. \x x
  2. \x y. x
  3. \x y. y
  4. \x y. y x
  5. \x. x x
  6. \x y z. x (y z)
  1. For each of the above translations, how many Is 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

Evaluation strategies in Combinatory Logic

  1. Find a term in CL that behaves like Omega does in the Lambda Calculus. Call it Skomega.

  2. Are there evaluation strategies in CL corresponding to leftmost reduction and rightmost reduction in the Lambda Calculus? What counts as a redex in CL?

  3. 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?

  4. 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:

  1. (\x. x (\y. y x)) (v w)
  2. (\x. x (\x. y x)) (v w)
  3. (\x. x (\y. y x)) (v x)
  4. (\x. x (\y. y x)) (v y)
  5. (\x y. x y y) u v
  6. (\x y. y x) (u v) z w
  7. (\x y. x) (\u u)
  8. (\x y z. x z (y z)) (\u v. u)