David Molnar asked a good question: (in my words) what does it mean to have a logic for a complexity class over ordered structures and over all (i.e. both ordered and unordered) structures? To answer this question, I will have to define what it means for a logic to capture a complexity class. As always, I assume that you have read preliminaries 1 and 2, which can be accessed from the sidebar. [Please let me know if your browser has any problem displaying the symbols.]
We will first recall the definition of "expressibility" of a property in a logic. Suppose we are given a σ-property (or boolean query) Q over a class C of σ-structures, i.e., Q is just a subset of C. Then, Q is said to be expressible in a logic L over C if there exists an L-sentence f such that, for any A ∈ C, A ∈ Q iff A |= f. When C is not mentioned, C is assumed to be the class of all finite σ-structures.
Observe that one can think of boolean queries as an analogue of the notion of languages, in the sense of formal language theory, or, more loosely, "computational problems". For example, consider the problem of testing hamiltonianicity of a graph. We can think of this problem as a boolean query H over the graph vocabulary such that a (finite) graph is in H iff it is hamiltonian. As a matter of fact, it is possible to encode any σ-structure as a (binary) string, and a string as a τ-structure for some vocabulary τ. Therefore, we can view any σ-boolean query as a language, and vice versa. So, we may redefine any complexity class K to be the set of all σ-properties that are computable in K, where σ ranges over all relational vocabularies. Hence, PTIME is the set of boolean queries that are computable in polynomial-time. For convenience, given a class C of structures, we also define KC to be the set of properties Q that are computable in K, when we restrict the input to Q to be all structures in C that have the same vocabulary as Q. When C is not mentioned, we assume C to be the set of all finite structures.
We are now ready to define the most important definition in descriptive complexity. A logic L is said to capture a complexity class K over a class C of finite structures if for any Q ∈ C: Q ∈ KC iff Q is expressible in L over C. Again, when C is not mentioned, it is assumed to be the set of all finite structures.
We know that existential second-order logic (ESO) captures NP. This is Fagin's result, which was discussed in Lance's blog recently. On the other hand, it is open whether there exists a logic that captures PTIME. We know, however, that there exists a logic (FO+LFP: first-order logic + least fixed point operator) that captures PTIME over all ordered structures. [Ordered structures mean that, we assume a binary relation in the structure to be interpreted as a total linear ordering on the universe.] This result was proven independently by Neil Immerman and Moshe Vardi in the 80's. You might be wondering whether FO+LFP captures PTIME. The answer is no: even testing whether a graph has an even number of elements cannot be done in FO+LFP without the help of an "external" linear order. The question whether there exists a logic for PTIME was first raised by Chandra and Harel in the 70's. Also, as I mentioned in a previous post, Yuri Gurevich conjectured that there is no logic for P (and this will imply that P ≠ NP). On a related note, it is also open whether there is a logic for any important complexity class below NP such as PTIME, L, NL, etc.
A relevant question is the following: why do we want to have a logic that capture complexity classes over all finite structures (not just over ordered structures)? The answer is technical: linear orderings make an inexpressibility proof more complicated by an order of magnitude!
3 comments:
Is there some natural relaxation of a linear ordering that is considered by logicians? Naively, I might try to define an ordering for which "not too many" elements are incomparable. If there exist such relaxations, do there exist any such that we know a logic for P with such a relaxed ordering?
David Molnar:
1. Answer to your first question: not that I know of. [I assume you ask this question for the hope that we can get increasingly "stronger" results so that a logic for PTIME will be finally obtained. See item 3 for another direction people have tried.]
2. Answer to your second question: I can give you one possible (although trivial) relaxation of a linear order: the "immediate successor" relation. I think FO+LFP still captures PTIME over all finite structures with external successor relations. This is because you can define a linear order using an external successor relation + fixed point operator. [Notice that without fixed point operator, FO cannot define a linear ordering even though you are given an external successor relation.]
3. On the other hand, some people have tried to find a logic that captures PTIME over "restricted classes of finite structures with no external linear orders". Martin Grohe has a beautiful result that says that the logic FO+LFP+(some counting quantifier) captures PTIME over the class of all finite structures, both ordered and unordered, of bounded treewidth. To the best of my knowledge, this is the strongest possible result we have gotten in this particular direction.
4. At the end of the day, one has to ask what we mean by a "logic". It seems that there are quite a few, not necessarily equivalent, definitions of the term logic. Alan Nash, Jeff Remmel, and Victor Vianu have recently published a nice paper on this issue. As far as I remember, their thesis is that each definition may lead to a different answer to whether there is a logic for PTIME.
Kenny: you can indeed think of the least fixed point operator as some sort of "built-in" partial order with limited capability (i.e. you can only pick "the least fixed point").
On a related note, there is a fixed point operator that gives you a "minimal fixed point" (not necessarily least). Finite model theorists (and I guess, also database theorists) call this operator "inflationary fixed point operator". Both FO+LFP and FO+IFP capture PTIME over ordered structures.
Post a Comment