Game Development Reference
In-Depth Information
As X is a fixed-point, 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 fixed-point 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 fixed-point Y = gfp ( F ).
The least and greatest fixed-points 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 fixed-point logic and reachability games
Least fixed-point logic (LFP) is defined by adding to the syntax of first-
order logic the following least fixed-point 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 fixed-points is analogous.
A
Obviously, LFP is a fragment of second-order 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 first-order logic, is reachability : Given a graph G =( V,E ) and a