Knaster–Tarski Fixed Point Theorem in Generalized Two Mappings on Metric Spaces

Abstract

The theorem has applications in abstract interpretation, a form of static program analysis. A common theme in lambda calculus is to find fixed points of given lambda expressions. Every lambda expression has a fixed point, and a fixed-point combinator is a "function" which takes as input a lambda expression and produces as output a fixed point of that expression. An important fixed-point combinator is the Y combinator used to give recursive definitions. In denotational semantics of programming languages, a special case of the Knaster–Tarski theorem is used to establish the semantics of recursive definitions. While the fixed-point theorem is applied to the "same" function (from a logical point of view), the development of the theory is quite different. The same definition of recursive function can be given, in computability theory, by applying Kleene's recursion theorem. These results are not equivalent theorems; the Knaster–Tarski theorem is a much stronger result than what is used in denotational semantics. However, in light of the Church–Turing thesis their intuitive meaning is the same: a recursive function can be described as the least fixed point of a certain functional, mapping functions to functions. The above technique of iterating a function to find a fixed point can also be used in set theory; the fixed-point lemma for normal functions states that any continuous strictly increasing function from ordinals to ordinals has one (and indeed many) fixed points.