In the mathematical areas of order and lattice theory, the Knaster–Tarski theorem, named after Bronisław Knaster and Alfred Tarski, states the following: It was Tarski who stated the result in its most general form,[1] and so the theorem is often known as Tarski's fixed-point theorem.
Some time earlier, Knaster and Tarski established the result for the special case where L is the lattice of subsets of a set, the power set lattice.
[2] The theorem has important applications in formal semantics of programming languages and abstract interpretation, as well as in game theory.
For example, in theoretical computer science, least fixed points of monotonic functions are used to define program semantics, see Least fixed point § Denotational semantics for an example.
One then usually is looking for the smallest set that has the property of being a fixed point of the function f. Abstract interpretation makes ample use of the Knaster–Tarski theorem and the formulas giving the least and greatest fixpoints.
Weaker versions of the Knaster–Tarski theorem can be formulated for ordered sets, but involve more complicated assumptions.
For example:[citation needed] This can be applied to obtain various theorems on invariant sets, e.g. the Ok's theorem: In particular, using the Knaster-Tarski principle one can develop the theory of global attractors for noncontractive discontinuous (multivalued) iterated function systems.
For weakly contractive iterated function systems the Kantorovich theorem (known also as Tarski-Kantorovich fixpoint principle) suffices.
Other applications of fixed-point principles for ordered sets come from the theory of differential, integral and operator equations.
Then it has a least fixpoint there, giving us the least upper bound of W. We've shown that an arbitrary subset of P has a supremum, that is, P is a complete lattice.
Chang, Lyuu and Ti[7] present an algorithm for finding a Tarski fixed-point in a totally-ordered lattice, when the order-preserving function is given by a value oracle.
In contrast, for a general lattice (given as an oracle), they prove a lower bound of
Deng, Qi and Ye[8] present several algorithms for finding a Tarski fixed-point.
Their algorithms have the following runtime complexity (where d is the number of dimensions, and Ni is the number of elements in dimension i): The algorithms are based on binary search.
On the other hand, determining whether a given fixed point is unique is computationally hard: For d=2, for componentwise lattice and a value-oracle, the complexity of
[9] But for d>2, there are faster algorithms: Tarski's fixed-point theorem has applications to supermodular games.
Because the best-response functions are monotone, Tarski's fixed-point theorem can be used to prove the existence of a pure-strategy Nash equilibrium (PNE) in a supermodular game.
Echenique[14] presents an algorithm for finding all PNE in a supermodular game.
His algorithm is exponential in the worst case, but runs fast in practice.
Deng, Qi and Ye[8] show that a PNE can be computed efficiently by finding a Tarski fixed-point of an order-preserving mapping associated with the game.