Immerman-Vardi theorem: Difference between revisions

From Polymath Wiki
Jump to navigationJump to search
New page: (More discussion needed!) : '''Theorem (Immerman-Vardi)'''. Over finite, ordered structures, the queries expressible in the logic FO(LFP) are precisely those that can be computed in polyn...
 
No edit summary
 
(One intermediate revision by one other user not shown)
Line 1: Line 1:
(More discussion needed!)
(More discussion needed!)


: '''Theorem (Immerman-Vardi)'''. Over finite, ordered structures, the queries expressible
: '''Theorem (Immerman-Vardi)'''. Over finite, ordered structures, the queries expressible in the logic FO(LFP) are precisely those that can be computed in polynomial time. Namely, FO(LFP) = P.
in the logic FO(LFP) are precisely those that can be computed in polynomial time. Namely, FO(LFP) = P.
 
In this context, an order relation could be as simple as a ''succ'' binary predicate, such that the transitive closure of ''succ'' imply a total order on the structure. A quick definition of FO(FLP) can be found in the [http://qwiki.stanford.edu/wiki/Complexity_Zoo:F#folfp complexity zoo]
 
* [I1986] N. Immerman, "[http://www.cs.umass.edu/~immerman/pub/query.pdf Relational queries computable in polynomial time]", Information and Control 68 (1986), 86-104
* [V1982] M. Vardi, Complexity of Relational Query Languages, 14th Symposium on Theory of Computation (1982), 137-146.

Latest revision as of 08:07, 10 August 2010

(More discussion needed!)

Theorem (Immerman-Vardi). Over finite, ordered structures, the queries expressible in the logic FO(LFP) are precisely those that can be computed in polynomial time. Namely, FO(LFP) = P.

In this context, an order relation could be as simple as a succ binary predicate, such that the transitive closure of succ imply a total order on the structure. A quick definition of FO(FLP) can be found in the complexity zoo