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