`ω := \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 <~~> &Omegea;(Ω 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#
- (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`?
- (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.)