author Chris Wed, 18 Feb 2015 19:55:13 +0000 (14:55 -0500) committer Chris Wed, 18 Feb 2015 19:55:13 +0000 (14:55 -0500)
 exercises/_assignment4.mdwn [new file with mode: 0644] patch | blob exercises/_assignment4_answers.mdwn [new file with mode: 0644] patch | blob

diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn
new file mode 100644 (file)
index 0000000..bb67eb4
--- /dev/null
@@ -0,0 +1,110 @@
+## Recursion ##
+
+## Basic fixed points ##
+
+1. Recall that `&omega; := \f.ff`, and `&Omega; := &omega; &omega;`.
+Is &Omega; a fixed point for &omega;?  Find a fixed point for &omega;,
+and prove that it is a fixed point.
+
+## Arithmetic infinity? ##
+
+The next few questions involve reasoning about Church arithmetic and
+infinity.  Let's choose some arithmetic functions:
+
+    succ = \nfz.f(nfz)
+    add = \m n. m succ n in
+    mult = \m n. m (add n) 0 in
+    exp = \m n . m (mult n) 1 in
+
+There is a pleasing pattern here: addition is defined in terms of
+the successor function, multiplication is defined in terms of
+addition, and exponentiation is defined in terms of multiplication.
+
+1. Find a fixed point `X` for the succ function.  Prove it's a fixed
+point, i.e., demonstrate that `succ X <~~> succ (succ X)`.
+
+We've had surprising success embedding normal arithmetic in the lambda
+calculus, modeling the natural numbers, addition, multiplication, and
+so on.  But one thing that some versions of arithmetic supply is a
+notion of infinity, which we'll write as `inf`.  This object usually
+satisfies the following constraints, for any (finite) natural number `n`:
+
+    n + inf == inf
+    n * inf == inf
+    n ^ inf == inf
+    n leq inf == True
+
+2. Prove that `add 1 X <~~> X`, where `X` is the fixed
+point you found in (1).  What about `add 2 X <~~> X`?
+
+Comment: a fixed point for the succ function is an object such that it
+is unchanged after adding 1 to it.  It make a certain amount of sense
+to use this object to model arithmetic infinity.  For instance,
+depending on implementation details, it might happen that `leq n X` is
+true for all (finite) natural numbers `n`.  However, the fixed point
+you found for succ is unlikely to be a fixed point for `mult n` or for
+`exp n`.
+
+
+#Mutually-recursive functions#
+
+<OL start=5>
+<LI>(Challenging.) One way to define the function `even` is to have it hand off
+part of the work to another function `odd`:
+
+       let even = \x. iszero x
+                                       ; if x == 0 then result is
+                                       true
+                                       ; else result turns on whether x's pred is odd
+                                       (odd (pred x))
+
+At the same tme, though, it's natural to define `odd` in such a way that it
+hands off part of the work to `even`:
+
+       let odd = \x. iszero x
+                                       ; if x == 0 then result is
+                                       false
+                                       ; else result turns on whether x's pred is even
+                                       (even (pred x))
+
+Such a definition of `even` and `odd` is called **mutually recursive**. If you
+trace through the evaluation of some sample numerical arguments, you can see
+that eventually we'll always reach a base step. So the recursion should be
+perfectly well-grounded:
+
+       even 3
+       ~~> iszero 3 true (odd (pred 3))
+       ~~> odd 2
+       ~~> iszero 2 false (even (pred 2))
+       ~~> even 1
+       ~~> iszero 1 true (odd (pred 1))
+       ~~> odd 0
+       ~~> iszero 0 false (even (pred 0))
+       ~~> false
+
+But we don't yet know how to implement this kind of recursion in the lambda
+calculus.
+
+The fixed point operators we've been working with so far worked like this:
+
+       let X = Y T in
+       X <~~> T X
+
+Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
+a *pair* of functions `T1` and `T2`, as follows:
+
+       let X1 = Y1 T1 T2 in
+       let X2 = Y2 T1 T2 in
+       X1 <~~> T1 X1 X2 and
+       X2 <~~> T2 X1 X2
+
+If we gave you such a `Y1` and `Y2`, how would you implement the above
+definitions of `even` and `odd`?
+
+
+<LI>(More challenging.) Using our derivation of Y from the [Week3
+notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave
+in the way described.
+
+(See [[hints/Assignment 4 hint 3]] if you need some hints.)
+
new file mode 100644 (file)
index 0000000..ac1ab6e
--- /dev/null
@@ -0,0 +1,27 @@
+1. Find a fixed point `X` for the succ function:
+
+    H := \f.succ(ff)
+    X := HH
+      == (\f.succ(ff)) H
+      ~~> succ(HH)
+
+So `succ(HH) <~~> succ(succ(HH))`.
+
+2. Prove that `add 1 X <~~> X`:
+
+    add 1 X == (\mn.m succ n) 1 X
+            ~~> 1 succ X
+            == (\fz.fz) succ X
+            ~~> succ X
+