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 ## Arithmetic infinity? ##
  11
  12 The next few questions involve reasoning about Church arithmetic and
  13 infinity.  Let's choose some arithmetic functions:
  14
  15     succ = \nfz.f(nfz)
  16     add = \m n. m succ n in
  17     mult = \m n. m (add n) 0 in
  18     exp = \m n . m (mult n) 1 in
  19
  20 There is a pleasing pattern here: addition is defined in terms of
  21 the successor function, multiplication is defined in terms of
  22 addition, and exponentiation is defined in terms of multiplication.
  23
  24 1. Find a fixed point `X` for the succ function.  Prove it's a fixed
  25 point, i.e., demonstrate that `succ X <~~> succ (succ X)`.
  26
  27 We've had surprising success embedding normal arithmetic in the lambda
  28 calculus, modeling the natural numbers, addition, multiplication, and
  29 so on.  But one thing that some versions of arithmetic supply is a
  30 notion of infinity, which we'll write as `inf`.  This object usually
  31 satisfies the following constraints, for any (finite) natural number `n`:
  32
  33     n + inf == inf
  34     n * inf == inf
  35     n ^ inf == inf
  36     n leq inf == True
  37
  38 2. Prove that `add 1 X <~~> X`, where `X` is the fixed
  39 point you found in (1).  What about `add 2 X <~~> X`?
  40
  41 Comment: a fixed point for the succ function is an object such that it
  42 is unchanged after adding 1 to it.  It make a certain amount of sense
  43 to use this object to model arithmetic infinity.  For instance,
  44 depending on implementation details, it might happen that `leq n X` is
  45 true for all (finite) natural numbers `n`.  However, the fixed point
  46 you found for succ is unlikely to be a fixed point for `mult n` or for
  47 `exp n`.
  48
  49
  50 #Mutually-recursive functions#
  51
  52 <OL start=5>
  53 <LI>(Challenging.) One way to define the function `even` is to have it hand off
  54 part of the work to another function `odd`:
  55
  56         let even = \x. iszero x
  57                                         ; if x == 0 then result is
  58                                         true
  59                                         ; else result turns on whether x's pred is odd
  60                                         (odd (pred x))
  61
  62 At the same tme, though, it's natural to define `odd` in such a way that it
  63 hands off part of the work to `even`:
  64
  65         let odd = \x. iszero x
  66                                         ; if x == 0 then result is
  67                                         false
  68                                         ; else result turns on whether x's pred is even
  69                                         (even (pred x))
  70
  71 Such a definition of `even` and `odd` is called **mutually recursive**. If you
  72 trace through the evaluation of some sample numerical arguments, you can see
  73 that eventually we'll always reach a base step. So the recursion should be
  74 perfectly well-grounded:
  75
  76         even 3
  77         ~~> iszero 3 true (odd (pred 3))
  78         ~~> odd 2
  79         ~~> iszero 2 false (even (pred 2))
  80         ~~> even 1
  81         ~~> iszero 1 true (odd (pred 1))
  82         ~~> odd 0
  83         ~~> iszero 0 false (even (pred 0))
  84         ~~> false
  85
  86 But we don't yet know how to implement this kind of recursion in the lambda
  87 calculus.
  88
  89 The fixed point operators we've been working with so far worked like this:
  90
  91         let X = Y T in
  92         X <~~> T X
  93
  94 Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
  95 a *pair* of functions `T1` and `T2`, as follows:
  96
  97         let X1 = Y1 T1 T2 in
  98         let X2 = Y2 T1 T2 in
  99         X1 <~~> T1 X1 X2 and
 100         X2 <~~> T2 X1 X2
 101
 102 If we gave you such a `Y1` and `Y2`, how would you implement the above
 103 definitions of `even` and `odd`?
 104
 105
 106 <LI>(More challenging.) Using our derivation of Y from the [Week3
 107 notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave
 108 in the way described.
 109
 110 (See [[hints/Assignment 4 hint 3]] if you need some hints.)
 111