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 c17-math-0001 with suitable properties, we can find c17-math-0002 the least element in the lattice such that c17-math-0003 equals c17-math-0004. 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 ...

Get Introduction to Lattice Theory with Computer Science Applications now with the O’Reilly learning platform.

O’Reilly members experience live online training, plus books, videos, and digital content from nearly 200 publishers.