## Recursion ##
## Basic fixed points ##
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
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#