24
I also have the impression that Descriptive Complexity is a less active area of research nowadays. Nevertheless, there are some topics in which people are still active:
Rank logics:
Rank Logic is Dead, Long Live Rank Logic! by Grädel and Pakusa
Symmetric Circuits for Rank Logic by Dawar and Wilsenach
Separating Rank Logic from Polynomial Time
by Lichter
...
13
Definitely still active in the area of Weisfeiler-Leman-style algorithms for isomorphism problems such as Graph Isomorphism. The connection with logic was first (I believe) made in Immerman-Lander and Cai-Fürer-Immerman. Very recently adapted to Group Isomorphism [Brachter-Schweitzer]. Certain logics are equivalent in their power to distinguish graphs (resp....
11
As you move to higher-order logics, each new order gives you quantification over exponentially larger objects than before, thus you can simulate exponentially longer computations. Other than that, it works pretty much the same as in the second-order case.
More precisely, define the iterated exponential function $2_d^x$ by
$$\begin{align*}2_0^x&=x,\\2_{d+...
8
FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per ...
8
There are recent exciting results concerning the search for a logic capturing PTIME.
The famous example by Cai, Fürer and Immerman showing that LFP+C does not capture
PTIME was based on a seemingly artificial class of graphs, though. Of course, it was constructed for the particular
task of demonstrating the restrictions of LFP+C. Only recently it was shown ...
6
Standard notions of reduction used in Descriptive Complexity are first-order reduction and the weaker first-order projection. Definitions of both these notions are found in Immerman's book on Descriptive Complexity.
6
The issue in play here is whether you use a self-terminating encoding (like your C example) or not. If you use a self-terminating encoding, then the subadditivity property does hold. If you don't (as in the common definition), then you need to expend bits on delimiting encodings.
Self-terminating encodings have other advantages, and even though real ...
6
There is a famous example of Cai, Fürer and Immerman, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}_{\infty\...
6
In fact, the circuit depends on the input structure, not only on the input structure size. We take a tree-decomposition of the graph with additional colours and turn it into a convolution tree. The evaluation of the formula on this tree is reduced to computing the value of the convolution tree. To compute the value of the tree, it is turned into an ...
5
This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment.
$PSPACE$ has the following (equivalent) descriptive characterizations:
$FO[2^{n^{O(1)}}]$, first-order logic with exponentially iterated quantifier blocks.
$SO[n^{O(1)}]$, second-order logic with polynomially iterated quantifier blocks.
$SO[TC]$, ...
4
Here's a more reality-concerned version of tigreen's answer from the point of a person who actually makes heavy use of (relational) databases: The whole point and complexity of their application is to structure them in a way they'd require as little amount of joins for each and every ever-needed query as possible and that's why they actually Do Work.
In ...
4
Here is another attempt at a more comprehensive answer. Your question already contains the formal definition of FO-rewritability, which at its core says that you can reduce a query answering problem:
The problem $D\cup\Sigma\models Q$ is being reduced to a problem $D\models Q_\Sigma$.
Several noteworthy things are happening here. The original problem is ...
4
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, ...
3
You have a non-deterministic algorithm deciding the problem.
If you want to think of it as a proof system for $EQUIV$, then
the proof of $(u,v) \in EQUIVE$ is just the string
representing the computation of your algorithm on $(u,v)$.
The proof checker just checks that
the given string is in fact an accepting computation of your algorithm on $(u,v)$.
Use ...
2
Lemma 1. Consider $L = (ab)^* + (ba)^*$:
There exists CFG with two variables which generates $L$
There exist no CFG with one variable which generates $L$
For proving (1) we may just consider the following CFG $$ S \rightarrow bAa \mid A , \, A \rightarrow abA \mid \varepsilon$$
The second proposition is a bit more tricky. Suppose that there exists CFG $G = ...
2
It does not extend.
Consider FO-LFP with just a binary predicate $<$, and the axioms for $<$ being a total order, with first and last positions, and every position has a successor. Moreover, we add an axiom saying that the last position can be reached from the first by iterating the successor function as a smallest fixpoint. This ensures that the ...
2
First question: A set $M$ is decidable if there is a Turing Machine which halts on all inputs and accepts all inputs $x$ with $x \in M$.
We try to encode $\bigwedge_{\phi \in X} \phi$ for arbitrary sets of $\mathsf{FO}[\tau]$-formulars $X$. Since, $\mathcal{P}(X)$ is uncountable there can be no code with finite alphabet. Hence, there can be no Turing ...
2
this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require.
To answer the requirement of positivity, the need comes from the fact that testing whether the formula captures a monotone operator or not is undecidable both ...
2
Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous:
A cut-free cyclic proof system for Kleene Algebra
Here we give a more traditional bona fide proof system for equivalence of regular expressions by allowing non-wellfounded reasoning in ...
2
For the case of Schaefer's dichotomy theorem, informally, the universal expressive power of Boolean CNF formulas built from non-Schaefer logical relations is behind the dichotomy. Every logical relation is definable by such formula using existential quantifier. This is stated formally in Schaefer's expressibility theorem (Theorem 2.5).
answered Oct 13 '15 at 7:57
Mohammad Al-Turkistany
20.4k4 gold badges57 silver badges144 bronze badges
2
Martin Grohe made substantial progress on this question recently. He gives a logic capturing polynomial time on classes of graphs embeddable in a fixed surface: https://dl.acm.org/citation.cfm?doid=2371656.2371662
Edit: the general case seems to be unresolved (but I am by no means an expert on this).
1
Professor Immerman kindly answered this by email:
The definition of FO(REGULAR) is the set of all decision problems that are reducible to some regular language via first-order reductions.
Additionally, since the word problem for $S_5$ (which is a regular language) is complete for $\mathsf{NC}^1$ under FO reductions, this means that FO(REGULAR) can be ...
1
As a complement to Janoma's answer above: it's 'very good'--- from the point of view of implementation --- because given a FO-rewritable language, we can use the powerful engines (for evaluating queries directly against a database without dependencies) that are available. That's basically reducing the problem to evaluation of SQL queries.
Only top voted, non community-wiki answers of a minimum length are eligible