Game Development Reference
In-Depth Information
queries, or propositional modal logic) by formulae defining fixed-points of
relational operators . Notice that, in general, fixed-points of F ψ need not exist,
or there may exist many of them. We therefore consider special kinds of
fixed-points, such as least and greatest, and later inflationary and deflationary
fixed-points, and we impose additional conditions on the relational operators
to guarantee that these fixed-points exist.
We shall now describe some basic facts of fixed-point theory for powerset
lattices (
P
( B ) ,
), where B is an arbitrary (finite or infinite) set. An operator
F :
P
( B )
→P
( B )is monotone , if it preserves inclusion, i.e., F ( X )
F ( Y )
whenever X
Y . A fixed-point X of F is called the least fixed-point of F
if X
Y for all fixed-points Y of F . Similarly, if all fixed-points of F are
subsets of a fixed-point X , then X is the greatest fixed-point of F .
Theorem 4.7 (Knaster-Tarski)
Every monotone operator F :
P
( B )
P
( B ) has a least fixed-point lfp ( F ) and a greatest fixed-point gfp ( F ) . Further,
these fixed-points may be written in the form
lfp ( F )=
=
{
X : F ( X )= X
}
{
X : F ( X )
X
}
gfp ( F )=
=
{
X : F ( X )= X
}
{
X : F ( X )
X
}
.
A proof can be found in any standard exposition on fixed-point theory
or fixed-point logics (see e.g., Gradel [2007]). Least fixed-points can also be
constructed inductively. We call an operator F :
( B ) inductive if
the sequence of its stages X α (where α ranges over the ordinals), defined by
X 0 :=
P
( B )
→P
,
X α +1 := F ( X α ) , and
X λ :=
α<λ
X α for limit ordinals λ,
is increasing, i.e., if X β
X α for all β<α . Obviously, monotone operators
are inductive. The sequence of stages of an inductive operator eventually
reaches a fixed-point, which we denote by X . The least ordinal β for which
X β = X β +1 = X is called the closure ordinal of F .
Exercise 4.2 Prove that the cardinality of the closure ordinal of every
inductive operator F :
( B ) is bounded by the cardinality of B .
However, the closure ordinal itself can be larger than
P
( B )
→P
|
B
|
. Prove this by an
example.
Theorem 4.8 For monotone operators, the inductively constructed fixed-
point coincides with the least fixed-point: X = lfp ( F ) .