Game Development Reference
InDepth Information
queries, or propositional modal logic) by formulae defining
fixedpoints of
relational operators
. Notice that, in general, fixedpoints of
F
ψ
need not exist,
or there may exist many of them. We therefore consider special kinds of
fixedpoints, such as least and greatest, and later inflationary and deflationary
fixedpoints, and we impose additional conditions on the relational operators
to guarantee that these fixedpoints exist.
We shall now describe some basic facts of fixedpoint 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 fixedpoint
X
of
F
is called the
least fixedpoint
of
F
if
X
Y
for all fixedpoints
Y
of
F
. Similarly, if all fixedpoints of
F
are
subsets of a fixedpoint
X
, then
X
is the
greatest fixedpoint
of
F
.
⊆
Theorem 4.7
(KnasterTarski)
Every monotone operator F
:
P
(
B
)
→
P
(
B
)
has a least fixedpoint
lfp
(
F
)
and a greatest fixedpoint
gfp
(
F
)
. Further,
these fixedpoints 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 fixedpoint theory
or fixedpoint logics (see e.g., Gradel [2007]). Least fixedpoints 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 fixedpoint, 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 fixedpoint: X
∞
=
lfp
(
F
)
.
Search Nedrilad ::
Custom Search