exercises/_assignment4.mdwn

   1 ## Recursion ##
   2
   3 ## Basic fixed points ##
   4
   5 1. Recall that <code>&omega; := \f.ff</code>, and <code>&Omega; :=
   6 &omega; &omega;</code>.  Is <code>&Omega;</code> a fixed point for
   7 <code>&omega;</code>?  Find a fixed point for <code>&omega;</code>,
   8 and prove that it is a fixed point.
   9
  10 2. Consider <code>&Omega; X</code> for an arbitrary term `X`.
  11 &Omega; is so busy reducing itself (the eternal solipsist) that it
  12 never gets around to noticing whether it has an argument, let alone
  13 doing anything with that argument.  If so, how could &Omega; have a
  14 fixed point?  That is, how could there be an `X` such that
  15 <code>&Omega; X <~~> &Omega;(&Omega; X)</code>?  To answer this
  16 question, begin by constructing <code>Y&Omega;</code>.  Prove that
  17 <code>Y&Omega;</code> is a fixed point for &Omega;.
  18
  19 3. Find two different terms that have the same fixed point.  That is,
  20 find terms `F`, `G`, and `X` such that `F(X) <~~> F(F(X))` and `G(X)
  21 <~~> G(G(X))`.  (If you need a hint, reread the notes on fixed
  22 points.)
  23
  24 ## Writing recursive functions ##
  25
  26 4. Helping yourself to the functions given just below,
  27 write a recursive function caled `fac` that computes the factorial.
  28 The factorial `n! = n * (n - 1) * (n - 2) * ... * 3 * 2 * 1`.
  29 For instance, `fac 0 ~~> 1`, `fac 1 ~~> 1`, `fac 2 ~~> 2`, `fac 3 ~~>
  30 6`, and `fac 4 ~~> 24`.
  31
  32      let true = \then else. then in
  33      let false = \then else. else in
  34      let iszero = \n. n (\x. false) true in
  35      let pred = \n f z. n (\u v. v (u f)) (K z) I in
  36      let succ = \n f z. f (n f z) in
  37      let add = \n m .n succ m in
  38      let mult = \n m.n(add m)0 in
  39      let Y = \h . (\f . h (f f)) (\f . h (f f)) in
  40
  41      let fac = ... in
  42
  43      fac 4
  44
  45 ## Arithmetic infinity? ##
  46
  47 The next few questions involve reasoning about Church arithmetic and
  48 infinity.  Let's choose some arithmetic functions:
  49
  50     succ = \nfz.f(nfz)
  51     add = \m n. m succ n in
  52     mult = \m n. m (add n) 0 in
  53     exp = \m n . m (mult n) 1 in
  54
  55 There is a pleasing pattern here: addition is defined in terms of
  56 the successor function, multiplication is defined in terms of
  57 addition, and exponentiation is defined in terms of multiplication.
  58
  59 1. Find a fixed point `X` for the succ function.  Prove it's a fixed
  60 point, i.e., demonstrate that `succ X <~~> succ (succ X)`.
  61
  62 We've had surprising success embedding normal arithmetic in the lambda
  63 calculus, modeling the natural numbers, addition, multiplication, and
  64 so on.  But one thing that some versions of arithmetic supply is a
  65 notion of infinity, which we'll write as `inf`.  This object usually
  66 satisfies the following constraints, for any (finite) natural number `n`:
  67
  68     n + inf == inf
  69     n * inf == inf
  70     n ^ inf == inf
  71     n leq inf == True
  72
  73 2. Prove that `add 1 X <~~> X`, where `X` is the fixed
  74 point you found in (1).  What about `add 2 X <~~> X`?
  75
  76 Comment: a fixed point for the succ function is an object such that it
  77 is unchanged after adding 1 to it.  It make a certain amount of sense
  78 to use this object to model arithmetic infinity.  For instance,
  79 depending on implementation details, it might happen that `leq n X` is
  80 true for all (finite) natural numbers `n`.  However, the fixed point
  81 you found for succ is unlikely to be a fixed point for `mult n` or for
  82 `exp n`.
  83
  84
  85 #Mutually-recursive functions#
  86
  87 <OL start=5>
  88 <LI>(Challenging.) One way to define the function `even` is to have it hand off
  89 part of the work to another function `odd`:
  90
  91         let even = \x. iszero x
  92                                         ; if x == 0 then result is
  93                                         true
  94                                         ; else result turns on whether x's pred is odd
  95                                         (odd (pred x))
  96
  97 At the same tme, though, it's natural to define `odd` in such a way that it
  98 hands off part of the work to `even`:
  99
 100         let odd = \x. iszero x
 101                                         ; if x == 0 then result is
 102                                         false
 103                                         ; else result turns on whether x's pred is even
 104                                         (even (pred x))
 105
 106 Such a definition of `even` and `odd` is called **mutually recursive**. If you
 107 trace through the evaluation of some sample numerical arguments, you can see
 108 that eventually we'll always reach a base step. So the recursion should be
 109 perfectly well-grounded:
 110
 111         even 3
 112         ~~> iszero 3 true (odd (pred 3))
 113         ~~> odd 2
 114         ~~> iszero 2 false (even (pred 2))
 115         ~~> even 1
 116         ~~> iszero 1 true (odd (pred 1))
 117         ~~> odd 0
 118         ~~> iszero 0 false (even (pred 0))
 119         ~~> false
 120
 121 But we don't yet know how to implement this kind of recursion in the lambda
 122 calculus.
 123
 124 The fixed point operators we've been working with so far worked like this:
 125
 126         let X = Y T in
 127         X <~~> T X
 128
 129 Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
 130 a *pair* of functions `T1` and `T2`, as follows:
 131
 132         let X1 = Y1 T1 T2 in
 133         let X2 = Y2 T1 T2 in
 134         X1 <~~> T1 X1 X2 and
 135         X2 <~~> T2 X1 X2
 136
 137 If we gave you such a `Y1` and `Y2`, how would you implement the above
 138 definitions of `even` and `odd`?
 139
 140
 141 <LI>(More challenging.) Using our derivation of Y from the [Week3
 142 notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave
 143 in the way described.
 144
 145 (See [[hints/Assignment 4 hint 3]] if you need some hints.)
 146