Game Development Reference
InDepth 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 fixedpoints
lfp
(
F
ϕ
) and
gfp
(
F
ϕ
) are
polynomialtime 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 firstorder operations are polynomialtime computable
we can conclude, by induction, that every LFPdefinable 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 Ptimecomplete, 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
fixedpoint logic captures polynomial time.
However, in the absence of a linear ordering, LFP fails to express all
Ptimeproperties. Indeed, there are quite trivial queries on unordered finite
structures that are not LFPdefinable. 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 fixedpoint logics). How
ever, many people conjecture that no logic whatsoever can capture Ptime
Search Nedrilad ::
Custom Search