Immerman-Vardi theorem: Difference between revisions

From Polymath Wiki
Jump to navigationJump to search
Setting up another stub
No edit summary
 
Line 2: Line 2:


: '''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.
: '''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 [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
* [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.
* [V1982] M. Vardi, Complexity of Relational Query Languages, 14th Symposium on Theory of Computation (1982), 137-146.

Latest revision as of 07: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