## 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.
## 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#