Game Development Reference
InDepth Information
As
X
∞
is a fixedpoint,
lfp
(
X
)
X
∞
. For the converse, we show
Proof
⊆
⊆
lfp
(
F
) for all
α
.As
lfp
(
F
)=
{
by induction that
X
α
Z
:
F
(
Z
)
⊆
Z
}
,it
su
ces to show that
X
α
is contained in all
Z
for which
F
(
Z
)
Z
.
For
α
= 0, this is trivial. By monotonicity and the induction hypothesis,
we have
X
α
+1
=
F
(
X
α
)
⊆
Z
. For limit ordinals
λ
with
X
α
⊆
F
(
Z
)
⊆
⊆
Z
for
all
α<λ
we also have
X
λ
=
α<λ
⊆
Z
.
The greatest fixedpoint can be constructed by a dual induction, starting
with
Y
0
=
B
, by setting
Y
α
+1
:=
F
(
Y
α
) and
Y
λ
=
α<λ
Y
α
for limit
ordinals. The
decreasing
sequence of these stages then eventually converges
to the greatest fixedpoint
Y
∞
=
gfp
(
F
).
The least and greatest fixedpoints are dual t
o each
other.
Fo
r every
monotone operator
F
, the dual operator
F
d
:
X
F
(
X
) (where
X
denotes
the complement of
X
) is also monotone, and we have that
→
lfp
(
F
)=
gfp
(
F
d
) and
gfp
(
F
)=
lfp
(
F
d
)
.
4.4.1 Least fixedpoint logic and reachability games
Least fixedpoint logic
(LFP) is defined by adding to the syntax of first
order logic the following
least fixedpoint formation rule
:If
ψ
(
R, x
)isa
formula of vocabulary
τ ∪{R}
with only positive occurrences of
R
,if
x
is a
t
uple of variables, and if
t
is a tuple of terms (such that the lengths of
x
and
t
match the arity of
R
), then also
[
lfp
Rx.ψ
](
t
) and [
gfp
Rx.ψ
](
t
)
are formulae of vocabulary
τ
. The free first

order variables of these formulae
are those in (free(
ψ
)
−{x
:
x
in
x}
)
∪
free(
t
).
Semantics.
Since
R
occurs only positive in
ψ
, the update operator
F
ψ
, defined
by
ψ
on any
τ
structure A (providing interpretations
f
or all free variables in
t
he formula) is monotone. We define that
A

=[
lfp
Rx.ψ
](
t
) if, and only if,
t
A
(the tuple of elements of
interpreting
t
) is contained in
lfp
(
F
ψ
). The
definition for greatest fixedpoints is analogous.
A
Obviously, LFP is a fragment of secondorder logic. Indeed, by the Tarski
Knaster Theorem,
[
lfp
Rx.ψ
(
R, x
)](
y
)
≡∀
R
((
∀
x
(
ψ
(
R, x
)
→
Rx
))
→
Ry
)
[
gfp
Rx.ψ
(
R, x
)](
y
)
≡∃
R
((
∀
x
(
Rx
→
ψ
(
R, x
))
∧
Ry
)
.
Perhaps the simplest example of a problem that is expressible in LFP, but
not in firstorder logic, is
reachability
: Given a graph
G
=(
V,E
) and a
Search Nedrilad ::
Custom Search