Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $<_1,<_2$ on $A$

$$(\mathcal{A},<_1) \models_{LFP} \varphi \Leftrightarrow (\mathcal{A},<_2) \models_{LFP} \varphi.$$

The logic $L_\leq$ is defined such that the modelling-relation is

$$ \mathcal{A} \models_{L_\leq} \varphi \Leftrightarrow \varphi \textrm{ is $\leq |A|$-invariant and } (\mathcal{A},<)\models_{LFP}\varphi \textrm{ for some} <.$$

A logic $L$ is efficiently $\operatorname{P}$-bounded for $\operatorname{P}$ if

  • for each $Q \in \operatorname{P}$ there is a $\varphi \in L$ which axiomatizes $Q$
  • for each $\varphi \in L$ there is polynomial $p$ such that the modelling relation $\mathcal{A} \models_L \varphi$ can be decided by an algorithm in $\leq p(\|\mathcal{A}\|)$ steps

A known result is that LFP is an efficiently $\operatorname{P}$-bound logic for $\operatorname{P}$ on the class of ordered structures. A paper states that one can easily deduce from the result that $L_\leq$ is a logic for $\operatorname{P}$. Any ideas how?

share|improve this question
2  
It seems to me that you are probably misreading the paper (Chen and Flum 2010 or 2011? it is always a good idea to include a link to the paper when asking a question about it). It is not known if there is a logic capturing invariant polynomial time queries, the result is a conditional result. –  Kaveh Nov 21 '12 at 16:24
1  
Btw, your post is really difficult to parse, e.g. "$P$-bound for $P$" and "$Q \in P$". Please use fonts similar to those used in the paper to make the post more readable. –  Kaveh Nov 21 '12 at 16:28
    
I'm refering to ChenFlum2010 p. 325 bottom. Doesn't the paper state that LFP is a logic capturing $\operatorname{P}$ for the class of unordered structures? –  joachim Nov 21 '12 at 18:53
1  
The linked paper and its revision don't have page 325. This is a major open problem in descriptive complexity as far as I know, their result is conditional. –  Kaveh Nov 22 '12 at 5:09
    
I'm sorry. I had different version of the paper. The reference is on page 5 in the upper half. Immerman, Vardi is used as a source. –  joachim Nov 22 '12 at 18:58

1 Answer 1

up vote 4 down vote accepted

People informally use the phrase "a logic for P" for the notion of a logic that captures P, which corresponds to Chen and Flum's definition of a "P-bounded logic for P". Essentially, this means that the logic defines exactly the polynomial-time properties of relational structures and formulae can be evaluated in polynomial time.1 Specifically, it's no use if your logic defines exactly the polytime properties but it takes exponential time to figure out whether a formula's true.

I think the confusion has arisen because Chen and Flum use the phrase "a logic for P" to mean just any logic that defines exactly the polytime properties of structures, without the requirement that formulae can be evaluated in polytime. The logic $L_\leq$ is a logic for P in this specific sense. Every polytime property is definable by a formula $\phi\in L_\leq$ but the semantics of the logic requires testing whether $\phi$ is $|A|$-invariant and there is no known way to do that in polynomial time.

$L_\leq$ defines all polytime properties because, by the result of Immerman and Vardi cited by Chen and Flum, LFP captures P on the class of ordered structures. More specifically, any ordering of the structure's universe lets you use tuples in $A^k$ to represent $k$-digit numbers in base $|A|$, which you can use as both for timestamps and to say "the $i$th character on the tape is $c$. You can then use a fixed-point formula that says, "If the configuration at time $t$ is $C_t$, then the configuration at time $t+1$ is $C_{t+1}$. The resulting formula doesn't depend on which ordering is chosen, so it's order-invariant, as required. Choosing a different ordering is just permuting the meaning of the digits in your base $|A|$ numbers.

Note that order-invariance in general is not decidable, which is why Chen and Flum restrict to order-invariance only on structures up to the size of the one we're evaluating the formula on. That's decidable but not known to be in P. (But the formulas constructed above are, in fact, order-invariant across all structures.)


1 More formally, for every formula $\phi$, there is a deterministic algorithm and a constant $k$ such that the algorithm decides whether $\cal{A}\vDash\phi$ in time at most $|A|^k$.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.