= (λx.if (x = 0) then 0 else if (x = 1) then x 0 else x ⊥)
= (λx.if (x = 0) then 0 else if (x = 1) then 1 else ⊥)
which (calling it f2) is yet another function that defined for one more input value. In summary, substituting f0 for f, one gets f1, and substituting f1, one gets f2. Continuing this way, each fi turns into a function fi 1 that is defined for one more input value. While none of these functions satisfies the equation, in the limit of these functions is a total function that satisfies the equation, and hence is a fixed-point (compared with earlier examples, such as the cos function, which seemed to “stabilize” to a fixed-point in a few steps on a finite-precision calculator; in case of the fi series, we achieve the fixed-point only in the limit). This limit element happens to be the least fixed-point (in a sense precisely defined in the next section), and is written
μx.(if (x = 0) then 0 else x f(x − 1)).
Let this least fixed-point function be called h. It is easy to see that h is the following function:
h(n) = Σn i=0 i.
It is reassuring to see that the least fixed-point is indeed the function that computes the same “answers” as function Fred would compute if compiled and run on a machine. It turns out that in recursive programming, the “desired solution” is always the least fixed-point, while in other contexts (e.g., in reachability analysis of finite-state machines demonstrated in Chapter 9), that need not be true. The ‘solution’ point of view for recursion also explains recursive definitions of the form
function Bob(x) = Bob(x 1).
The only solution for function Bob is the everywhere undefined function λx. ⊥. To see this more vividly, one can try to de-Bob the recursion to get
Bob = Y (lambda y . lambda x . y(x 1)). Suppose H = (lambda y . lambda x . y(x 1)). Now, supplying a value such as 5 to Bob, and continuing as with function Fred, one obtains the following reduction sequence:
Bob 5 = (Y H) 5
= H (Y H) 5
= (lambda y . lambda x . y(x 1)) (Y H) 5
= (lambda x . (Y H)(x 1)) 5
= (Y H)(5 1)
= (Y H) 6
= ...
= (Y H) 7
= ...
= (non-convergent).
In other words, Bob turns out to be the totally undefined function, or “bottom function.”
