Game Development Reference
In-Depth Information
4.4.2 Capturing polynomial time
Let ϕ be a formula such that, for any given structure
A
, the update operator
( A k )
( A k ) is monotone and computable in polynomial time
F ϕ :
P
→P
(with respect to
). Then also the fixed-points lfp ( F ϕ ) and gfp ( F ϕ ) are
polynomial-time computable since the inductive constructions of least and
greatest fixed points terminate after at most
|
A
|
k iterations of F ϕ . Together
with the fact that first-order operations are polynomial-time computable
we can conclude, by induction, that every LFP-definable property of finite
structures is computable in polynomial time.
|
A
|
Theorem 4.9 Let ψ be a sentence in LFP . It is decidable in polynomial time
whether a given finite structure
A
is a model of ψ. In short, LFP
Ptime .
Further, we have already seen that LFP can define properties that are
actually Ptime-complete, such as winning regions in reachability games.
This leads to the question of whether LFP can express all properties of finite
structures that are computable in polynomial time.
This is indeed the case when we consider ordered finite structures .Wesay
that a logic L captures a complexity class C on a domain
D
of finite
structures, if (1) for every fixed sentence ψ
L , the complexity of evaluating
ψ on structures from
is a problem in the complexity class C , and (2)
every property of structures in
D
that can be decided with complexity C
is definable in the logic L . For any finite vocabulary τ , we write Ord( τ )
for the class of all structures (A ,< ), where A is a finite τ -structure and <
is a linear order on (the universe of) A. It is one of the most influential
results of finite model theory that for every model class K⊆ Ord( τ ) that
is decidable in polynomial time, there exists a sentence ψ ∈ LFP such that
K = { A Ord( τ ):A | = ψ} .
D
Theorem 4.10 (Immerman and Vardi)
On ordered finite structures, least
fixed-point logic captures polynomial time.
However, in the absence of a linear ordering, LFP fails to express all
Ptime-properties. Indeed, there are quite trivial queries on unordered finite
structures that are not LFP-definable. A simple example is the question of
whether a given finite structure has an even number of elements.
The question of whether there exists a logic that captures Ptime on arbi-
trary finite structures, originally posed by Chandra and Harel [1982], is the
most important open problem of finite model theory. The most promising
candidates are suitable extensions of LFP (or other fixed-point logics). How-
ever, many people conjecture that no logic whatsoever can capture Ptime