X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2Fassignment3.mdwn;h=f80fe71c355912c10431fde30ba34c20571ac691;hp=f593f4d7bdc89d9af36ac1a68f1336c0880ed9b8;hb=588916b85952d356b51cccea0fb38b8cc1582174;hpb=9794378606926302d83f08b63cc7021bbe9725c5 diff --git a/exercises/assignment3.mdwn b/exercises/assignment3.mdwn index f593f4d7..f80fe71c 100644 --- a/exercises/assignment3.mdwn +++ b/exercises/assignment3.mdwn @@ -1,17 +1,115 @@ -## Comprehensions +** *Work In Progress* ** -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]`. +## Lists and List Comprehensions -*Here is a hint* +1. In Kapulet, what does `[ [x, 2*x] | x from [1, 2, 3] ]` evaluate to? -Define a function `dup (n, x)` that creates a list of *n* copies of `x`. Then use list comprehensions to transform `[3, 1, 0, 2]` into `[[3, 3, 3], [1], [], [2, 2]]`. Then use `join` to "flatten" the result. +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|assignment3 hint1]], if you need it. +4. Last week you defined `head` in the Lambda Calculus, using our proposed encoding for lists. Now define `empty?` (It should require only small modifications to your solution for `head`.) -## Lists +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? -7. Continuing to encode lists in terms of their left-folds, how should we write `head`? This is challenging. +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. -*Here is a hint* +7. Continuing to encode lists in terms of their left-folds, how should we write `head`? This is challenging. [[Here is a solution|assignment3 hint2]], 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|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: + +
    +
  1. Kxy +
  2. KKxy +
  3. KKKxy +
  4. SKKxy +
  5. SIII +
  6. SII(SII) +
+ + + +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: + +
    +
  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) +
+ + + +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: + +
    +
  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) +