Introduction to Lattice Theory with Computer Science Applications

Chapter 17Fixed Point Theory

In this chapter, we introduce the notion of fixed points of a function defined over ordered sets. The theory of fixed points allows us to obtain extremal solutions of equations involving operations over lattices. For example, given any function with suitable properties, we can find the least element in the lattice such that equals . In computer science applications, we can use fixed point theory to define the meaning of recursion when functions are defined over lattices (or complete partial orders). We illustrate these notions by defining probabilistic version of formal languages.

We begin by defining complete partial orders because they are weaker than complete lattices but still allow computation of fixed points. We then give Knaster–Tarski fixed point theorem that shows existence of least and greatest fixed points for monotone functions. If the function is continuous (a stronger property than monotonicity), then we show how one can give an explicit construction of the least fixed point. Section 17.3 gives applications of these results.

17.1 Complete ...