The Least Fixed-point

The least fixed-point: In the above example, we obtained a fixed-point h which we asserted to be the “least” in a sense that will now be made clear. In general,
given a recursive program, if there are multiple fixed-points, The desired meaning of recursive programs corresponds to the least fixed-point, and The fixed-point finding combinator Y is guaranteed to compute the least fixed-point [114].
To better understand these assertions, consider the following four
definitions of functions of type Z × Z → Z, where Z is the integers
(this example comes from [78]):
f1 = λ(x, y) . if x = y then y 1 else x 1
f2 = λ(x, y) . if x ≥ y then x 1 else y − 1
f3 = λ(x, y) . if x ≥ y and x− y is even then x 1 else ⊥
Now consider the recursive definition:
F(x, y) = if x = y then y 1 else F(x, F(x − 1, y 1)).
We can substitute f1, f2, or f3 in place of F and get a true equation! Exercise 6.8 asks you to demonstrate this. However, of these functions, f3 is the least defined function in the sense that whenever f3(x) is defined, fi(x) is defined for i = 1, 2, but not vice versa, and there is no other function (say f4) that is less defined than f3 and also serves as a solution to F.
To visualize concepts such as “less defined,” imagine as if we were plotting the graphs of these functions. Now, when a function is undefined for an x value, we introduce a “gap” in the graph. In this sense, the graph of the least fixed-point function is the “gappiest” of all; it is a solution, and is the most undefined of all solutions – it has the most number of “gaps.” These notions can be captured precisely in terms of least upper-bounds of pointed complete partial orders [107]. In our example, it can be shown that f3 is the least fixed-point for the recursion.

Fixed-points in Automata Theory: We will have many occasions to appeal to the least fixed-point idea in this book. Here are some examples:

Cross-coupled combinational gates attain stable states defined by fixed-points. For instance, two inverters in a loop become a flip-flop that stores a 0 or a 1. These are the two solutions of the recursive circuit-node equation x = not(not(x)).1
Three inverters in a loop form a ring oscillator. The reason, to a first approximation, is that they are all trying, in vain, to solve the recursive node equation x = not(not(not(x))); in addition, there is a 3-inverter delay around the loop.
Context-free grammar productions are recursive definitions of languages. The language defined by such recursive definitions can be determined through a least fixed-point iteration similar to what we did by starting with ⊥; for context-free grammars, the empty language ∅ serves as the “seed” from which to begin such iterations.
In the section pertaining to Binary Decision Diagrams, we will formulate a process of computing the set of reachable states as a fixedpoint computation.
In the section on nondeterministic automata, we will write recursive definitions for Eclosure and justify that such recursive definitions are well-defined (i.e., they are not nonsensical, similar to the recursion for function Bob, for which no solution exists).

It is also worth noting that while least fixed-points are most often of interest, in many domains such as temporal logic, the greatest fixedpoints are also of interest. The functional (higher order function) H from Section 6.1.1, namely
H = (λy.λx.if (x = 0) then 0 else x y(x − 1))
has an interesting property: it works as a “bottom refiner!” In other words, when fed the “everywhere undefined function” f0 (called the “bottom function”), it returns the next better approximation of the least fixed-point h in the form of f1. When fed f1, it returns the next better approximation f2, and so on. It may sound strange that the meaning of recursive programs is determined starting from the most uninteresting of functions, namely the ‘bottom’ or ⊥ function. However, this is the most natural approach to be taking, because

⊥ contains no information at all,
going through the fixed-point iteration starting from ⊥, pulls into subsequent approximants f1, f2, etc., only relevant information stemming from the structure of the recursion.

Later when we study state-space reachability analysis techniques in Section 11.3.2, and context-free grammars in Section 13.2.2, we will appeal to this “bottom-refining” property. We will be identifying a suitable “bottom” object in each such domain.