X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=exercises%2F_assignment4.mdwn;h=7df06052a7d951fd663438b1b9cfbc5181238bed;hb=89121328344917225949cb675a6706cbcd0f83d9;hp=bb67eb4080156ef666e18ee2a97dc7724a5d3453;hpb=4b58f050598948e1345d1a5734257c656adb9002;p=lambda.git
diff --git a/exercises/_assignment4.mdwn b/exercises/_assignment4.mdwn
index bb67eb40..7df06052 100644
--- a/exercises/_assignment4.mdwn
+++ b/exercises/_assignment4.mdwn
@@ -2,10 +2,46 @@
## Basic fixed points ##
-1. Recall that `ω := \f.ff`, and `Ω := ω ω`.
-Is Ω a fixed point for ω? Find a fixed point for ω,
+1. Recall that ω := \f.ff
, and Ω :=
+ω ω
. Is Ω
a fixed point for
+ω
? Find a fixed point for ω
,
and prove that it is a fixed point.
+2. Consider Ω X
for an arbitrary term `X`.
+Ω is so busy reducing itself (the eternal solipsist) that it
+never gets around to noticing whether it has an argument, let alone
+doing anything with that argument. If so, how could Ω have a
+fixed point? That is, how could there be an `X` such that
+Ω X <~~> Ω(Ω X)
? To answer this
+question, begin by constructing YΩ
. Prove that
+YΩ
is a fixed point for Ω.
+
+3. Find two different terms that have the same fixed point. That is,
+find terms `F`, `G`, and `X` such that `F(X) <~~> F(F(X))` and `G(X)
+<~~> G(G(X))`. (If you need a hint, reread the notes on fixed
+points.)
+
+## Writing recursive functions ##
+
+4. Helping yourself to the functions given just below,
+write a recursive function caled `fac` that computes the factorial.
+The factorial `n! = n * (n - 1) * (n - 2) * ... * 3 * 2 * 1`.
+For instance, `fac 0 ~~> 1`, `fac 1 ~~> 1`, `fac 2 ~~> 2`, `fac 3 ~~>
+6`, and `fac 4 ~~> 24`.
+
+ let true = \then else. then in
+ let false = \then else. else in
+ let iszero = \n. n (\x. false) true in
+ let pred = \n f z. n (\u v. v (u f)) (K z) I in
+ let succ = \n f z. f (n f z) in
+ let add = \n m .n succ m in
+ let mult = \n m.n(add m)0 in
+ let Y = \h . (\f . h (f f)) (\f . h (f f)) in
+
+ let fac = ... in
+
+ fac 4
+
## Arithmetic infinity? ##
The next few questions involve reasoning about Church arithmetic and