Game Development Reference
In-Depth Information
where ϕ does not hold. Rather than redesigning the system, he tries to just
throw away all bad elements of
A
, i.e., he relativises
A
to the substructure
A | ϕ induced by
{
a :
A |
= ϕ ( a )
}
. Unfortunately, it need not be the case that
A | ϕ |
( x ). Indeed, the removal of some elements may have the effect
that others no longer satisfy ϕ . But the lazy engineer can of course iterate
this relativisation procedure and define a (possibly transfinite) sequence of
substructures
=
λ = β<λ A
β , with
0 =
β +1 =
β
β
A
A
A
,
A
A
| ϕ and
A
for limit
A which satisfies
ordinals λ . This sequence reaches a fixed-point
( x )-
but it may be empty.
This process of iterated relativisation is definable by a fixed-point induction
in
Z be the syntactic relativisation of ϕ to a new set variable Z ,
obtained by replacing inductively all subformulae ∃yα by ∃y ( Zy ∧ α ) and
∀yα by ∀y ( Zy → α ). Iterated relativisation means repeated application of
the operator
A
. Let ϕ
|
F : Z →{a : A | Z | = ϕ ( a ) } = {a : A | = Za∧ ϕ| Z ( a ) }
starting with Z = A (the universe of
A
). Note that F is deflationary but not
necessarily monotone.
In logics with inflationary and deflationary fixed points (the universe of)
A is uniformly definable in
A
by a formula of the form [ dfp Zx.ϕ
| Z ]( x ).
A is also LFP-definable.
However, the only known way to provide such a definition is by going through
the proof of Kreutzer's Theorem (see Kreutzer [2004]). There seems to be no
simple direct definition based on least and greatest fixed-points only.
Since IFP and LFP have the same expressive power,
4.6.2 Parity games with backtracking
Backtracking games are essentially parity games with the addition that,
under certain conditions, players can jump back to an earlier position in the
play. This kind of move is called backtracking. A backtracking move from
position v to an earlier position u is only possible if v belongs to a given set
B of backtrack positions, if u and v have the same priority and if no position
of smaller priority has occurred between u and v . With such a move, the
player who backtracks not only resets the play back to u , she also commits
herself to a backtracking distance d , which is the number of positions of
priority Ω( v ) that have been seen between u and v . After this move, the play
ends when d further positions of priority Ω( v ) have been seen, unless this
priority is “released” by a lower priority.
For finite plays we have the winning condition that a player wins if her
opponent cannot move. For infinite plays, the winner is determined according