## 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 . Prove that 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#
  1. (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`?
  2. (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.)