Additional reading Taski Fix Point
Tarski Fix Point Theorem
Tarski Fix Point Theorem can be applied on a larger range of functions but
on a smaller range of domains. Given a set
A and a partial order
R on
A, we call
A, R a complete lattice if for any subset
X of
A,
X
has a least upper bound and a greatest lower bound. Tarski fix point theorem
says, if
F: A -> A is a monotonic function w.r.t. the order
R, then the
greatest lower bound of set
{ a: A | F a ≤ a } is the least fix point of
F.
In comparison with Bourbaki-Witt fix point theorem, Tarski fix point theorem
does not require the function
F to be continuous but requires every subset
of
A to have a least upper bound (and a greatest lower bound), not only
those chains.
Soundness
Suppose
a0 = glb ( {a: A | F a ≤ a} ). Then, for any
a: A such that
F a ≤ a we know that
a0 ≤ a. Thus,
F a0 ≤ F a ≤ a. That means
F a0 is also a lower bound of
{a: A | F a ≤ a} . So,
F a0 ≤ a0
since
a0 is its greatest lower bound.
This conclusion is immediately followed by the fact:
F (F a0) ≤ F a0. So,
F a0 is an element of
{a: A | F a ≤ a} . Therefore,
a0 ≤ F a0.
Thus,
a0 = F a0.
Least Fix Point
Suppose
a1 is also a fix point of
F. Then,
a1 = F a1 and thus
a1
is also an element of
{a: A | F a ≤ a} . But
a0 is the greatest lower
bound of this set, therefore
a0 ≤ a1.