exercises/assignment3.mdwn

   1 ** *Work In Progress* **
   2
   3 ## Comprehensions
   4
   5 1. In Kapulet, what does `[ [x, 2*x] | x from [1, 2, 3] ]` evaluate to?
   6
   7 2. What does `[ 10*x + y | y from [4], x from [1, 2, 3] ]` evalaute to?
   8
   9 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.
  10
  11
  12 ## Lists
  13
  14 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`.)
  15
  16 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?
  17
  18 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.
  19
  20 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.
  21
  22
  23 ## Numbers
  24
  25 8. 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. In last week's homework, you defined `succ` for numbers so encoded. Can you now define `pred` in the Lambca Calculus? 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.
  26
  27 9. Define `leq` for numbers (that is, &leq;) in the Lambda Calculus. Here is the expected behavior,
  28 where `one` abbreviates `succ zero`, and `two` abbreviates `succ (succ zero)`.
  29
  30         leq zero zero ~~> true
  31         leq zero one ~~> true
  32         leq zero two ~~> true
  33         leq one zero ~~> false
  34         leq one one ~~> true
  35         leq one two ~~> true
  36         leq two zero ~~> false
  37         leq two one ~~> false
  38         leq two two ~~> true
  39         ...
  40
  41     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.
  42
  43 ## Combinatory Logic
  44
  45 Reduce the following forms, if possible:
  46
  47 10. `Kxy`
  48 11. `KKxy`
  49 12. `KKKxy`
  50 13. `SKKxy`
  51 14. `SIII`
  52 15. `SII(SII)`
  53
  54 <!-- -->
  55
  56 16. Give Combinatory Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`.
  57
  58 Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic:
  59
  60 17. `\x x`
  61 18. `\x y. x`
  62 19. `\x y. y`
  63 20. `\x y. y x`
  64 21. `\x. x x`
  65 22. `\x y z. x (y z)`
  66
  67 <!-- -->
  68
  69 23. 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.
  70
  71 Evaluation strategies in Combinatory Logic
  72 ------------------------------------------
  73
  74 23. Find a term in CL that behaves like Omega does in the Lambda
  75 Calculus.  Call it Skomega.
  76
  77 24. Are there evaluation strategies in CL corresponding to leftmost
  78 reduction and rightmost reduction in the lambda calculus?
  79 What counts as a redex in CL?
  80
  81 25. Consider the CL term K I Skomega.  Does leftmost (alternatively,
  82 rightmost) evaluation give results similar to the behavior of K I
  83 Omega in the lambda calculus, or different?  What features of the
  84 lambda calculus and CL determine this answer?
  85
  86 26. What should count as a thunk in CL?  What is the equivalent
  87 constraint in CL to forbidding evaluation inside of a lambda abstract?
  88
  89
  90 More Lambda Practice
  91 --------------------
  92
  93 Reduce to beta-normal forms:
  94
  95 <OL start=24>
  96 <LI>`(\x. x (\y. y x)) (v w)`
  97 <LI>`(\x. x (\x. y x)) (v w)`
  98 <LI>`(\x. x (\y. y x)) (v x)`
  99 <LI>`(\x. x (\y. y x)) (v y)`
 100
 101 <LI>`(\x y. x y y) u v`
 102 <LI>`(\x y. y x) (u v) z w`
 103 <LI>`(\x y. x) (\u u)`
 104 <LI>`(\x y z. x z (y z)) (\u v. u)`
 105 </OL>
 106