3 ## Basic fixed points ##
5 1. Recall that `ω := \f.ff`, and `Ω := ω ω`.
6 Is Ω a fixed point for ω? Find a fixed point for ω,
7 and prove that it is a fixed point.
9 ## Arithmetic infinity? ##
11 The next few questions involve reasoning about Church arithmetic and
12 infinity. Let's choose some arithmetic functions:
15 add = \m n. m succ n in
16 mult = \m n. m (add n) 0 in
17 exp = \m n . m (mult n) 1 in
19 There is a pleasing pattern here: addition is defined in terms of
20 the successor function, multiplication is defined in terms of
21 addition, and exponentiation is defined in terms of multiplication.
23 1. Find a fixed point `X` for the succ function. Prove it's a fixed
24 point, i.e., demonstrate that `succ X <~~> succ (succ X)`.
26 We've had surprising success embedding normal arithmetic in the lambda
27 calculus, modeling the natural numbers, addition, multiplication, and
28 so on. But one thing that some versions of arithmetic supply is a
29 notion of infinity, which we'll write as `inf`. This object usually
30 satisfies the following constraints, for any (finite) natural number `n`:
37 2. Prove that `add 1 X <~~> X`, where `X` is the fixed
38 point you found in (1). What about `add 2 X <~~> X`?
40 Comment: a fixed point for the succ function is an object such that it
41 is unchanged after adding 1 to it. It make a certain amount of sense
42 to use this object to model arithmetic infinity. For instance,
43 depending on implementation details, it might happen that `leq n X` is
44 true for all (finite) natural numbers `n`. However, the fixed point
45 you found for succ is unlikely to be a fixed point for `mult n` or for
49 #Mutually-recursive functions#
52 <LI>(Challenging.) One way to define the function `even` is to have it hand off
53 part of the work to another function `odd`:
55 let even = \x. iszero x
56 ; if x == 0 then result is
58 ; else result turns on whether x's pred is odd
61 At the same tme, though, it's natural to define `odd` in such a way that it
62 hands off part of the work to `even`:
64 let odd = \x. iszero x
65 ; if x == 0 then result is
67 ; else result turns on whether x's pred is even
70 Such a definition of `even` and `odd` is called **mutually recursive**. If you
71 trace through the evaluation of some sample numerical arguments, you can see
72 that eventually we'll always reach a base step. So the recursion should be
73 perfectly well-grounded:
76 ~~> iszero 3 true (odd (pred 3))
78 ~~> iszero 2 false (even (pred 2))
80 ~~> iszero 1 true (odd (pred 1))
82 ~~> iszero 0 false (even (pred 0))
85 But we don't yet know how to implement this kind of recursion in the lambda
88 The fixed point operators we've been working with so far worked like this:
93 Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on
94 a *pair* of functions `T1` and `T2`, as follows:
101 If we gave you such a `Y1` and `Y2`, how would you implement the above
102 definitions of `even` and `odd`?
105 <LI>(More challenging.) Using our derivation of Y from the [Week3
106 notes](/week3/#index4h2) as a model, construct a pair `Y1` and `Y2` that behave
107 in the way described.
109 (See [[hints/Assignment 4 hint 3]] if you need some hints.)