Questions tagged [descriptive-complexity]
Descriptive complexity classifies problems based on how hard it is to express the problem in some logical formalism.
53
questions
1
vote
0
answers
74
views
Complexity class name for the class of languages that are $\Sigma^1_1$-definable over finite domains
Let ${\cal L}=\{Y_1,..., Y_k, X\}$ be a finite relational language such that $X$ is a unary relation name. Let $\phi(X,\bar{Y})\in{\cal L}$ be a first-order formula (the formula can have the equality ...
- 322
5
votes
1
answer
93
views
Nonterminal descriptional complexity of regular languages
Recently I became interested in grammar complexity of regular language. Prior to searching for literature, I tried to investigate it on my own, proving two lemmas from comment below.
I am aware of an ...
- 411
29
votes
3
answers
3k
views
Is Descriptive Complexity dead?
I recently started reading about Descriptive Complexity, the branch of Complexity Theory studying the logic languages needed to express complexity classes. The main milestone in the area seems to be ...
- 429
4
votes
1
answer
179
views
What is FO(REGULAR)? (The descriptive complexity equivalent of NC1)
According to Immerman's Descriptive Complexity diagram, there is a logic called $\mathsf{FO(REGULAR)}$ which captures $\mathsf{NC}^1$. However, I can't find the reference where this logic is defined. ...
- 842
0
votes
0
answers
98
views
Does Descriptive Complexity techniques have the naturalisation barrier?
I wished to know if the proof attempts at separation of complexity classes via the methods outlined by Descriptive Complexity theorists naturalise?
By naturalise I'm talking about the Idea of Natural ...
- 21
8
votes
1
answer
229
views
Second order logic = PH. Do even higher order logics correspond to anything on complexity side of things?
In the context of descriptive complexity PH is the class of languages expressible by statements of second-order logic. What classes of languages do higher order logics correspond to?
- 291
11
votes
0
answers
193
views
Descriptive Complexity characterzation of BPP
We know of descriptive complexity characterizations of classes such as P, and NP, which use First Order logic, and operators. Does BPP have a characterization under descriptive complexity, too(any ...
- 1,101
4
votes
1
answer
182
views
Reductions in Descriptive Complexity
Reducing one problem to another are well known in various settings, such as many-one, randomized, truth-table, logspace or a whole slew of other reductions. Descriptive complexity can alternately ...
- 1,101
2
votes
0
answers
67
views
Inexpressibility of Second order
In finite model theory, Ehrenfeucht-Fraïssé games gives us tools to prove inexpressibility results for FOL. Pebble games do the same for infinitary logic with finitely many variables.
Do we have such ...
- 121
10
votes
1
answer
272
views
P and Descriptive Complexity
In the Complexity Zoo, it says [1] that, in descriptive complexity, $P$ can be defined by three different kind of formulae, $FO(LFP)$ which is also $FO(n^{O(1)})$, and also as $SO(HORN)$.
However, ...
user17918
1
vote
0
answers
137
views
Proof of SAT is complete for NP via first-order reductions
So I have been reading this: https://people.cs.umass.edu/~immerman/book/ch7.pdf
I do not understand the proof of theorem 7.16, which says that SAT is complete for NP via first-order reductions. My ...
- 21
3
votes
1
answer
165
views
Descriptive model theory classification of Counting hierarchy
Descriptive model theory uses logic to characterize complexity classes
How to model
Counting Hierarchy
PSPACE
in descriptive model theory?
- 12.5k
6
votes
1
answer
407
views
Where does the "intuitive" understanding of Kolmogorov complexity fails
Often, the Kolmogorov complexity of some string $x$ is defined as the length of the shortest program producing $x$, for example on wikipedia.
So to give this more formal meaning, define
$$
K'(x) := ...
- 1,947
3
votes
2
answers
137
views
Construct proof systems for common algorithmic task, like equivalence of regular expressions
A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto.
For $y \in L$ ...
- 1,947
0
votes
0
answers
156
views
Questions about the definition of the Quantum Turing Machine
I am trying to have a better understanding of the definition of the Quantum Turing Machine.
My questions:
If the output of a quantum program is the eigenvalue of the ground state of a Hamiltonian ...
- 697
10
votes
0
answers
214
views
reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary
$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda ...
- 4,319
11
votes
1
answer
249
views
What do dichotomy theorems feed on?
It is well known that certain classes of NP-problems have dichotomy theorems, which guarantee that every task in the class is either NP-complete or is in P. The best known such result is
Schaefer's ...
- 10.8k
1
vote
0
answers
145
views
Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP
In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
- 21
5
votes
1
answer
200
views
Expressiveness of Infinitary Logic
I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. ...
- 513
7
votes
3
answers
296
views
Completeness of the extension of first order logic with least fixed point order operator
Is there any result about the extension of first order logic with least fixed point operator, being complete (as logic in general on infinite structures too) or not? In other words does the Goedel ...
2
votes
1
answer
87
views
Infinitary Counting Logics: 1-sorted vs. 2-sorted framework
There are two ways to extend infinitary logic with counting:
Grädel's way (cf. p. 11):
We extend $L_{\infty\omega}$ by introducing a counting existential quantifier:
$$ \mathcal{A} \models \exists^{...
- 513
6
votes
1
answer
255
views
Is infinitary logic a logic in the sense of Gurevich?
Gurevich provides an exact definition of what Logic capturing PTIME is.
An abstract logic $L$ consists of
a set of $L[\tau]$-sentences for each vocabulary $\tau$,
and a mapping that maps a property $...
- 513
9
votes
1
answer
406
views
What is wrong with this $\mathsf{L} \subseteq \mathsf{L}-$uniform $\mathsf{NC}^1$ argument?
The following is not believed to be true:
$\mathsf{L} \subseteq \mathsf{L}-\mbox{uniform } \mathsf{NC}^1$
Can you help me see where the argument breaks down?
The directed reachability problem is ...
- 2,279
4
votes
2
answers
781
views
Context-free Grammar for a Context-free Language Intersecting a Regular Language (get the Maximum Number of Rules)
It is well known that the intersection of $L \cap R$ of a context-free Language $L$ and a regular Language $R$ is context-free. Each proof I have seen constructs a automaton (a PDA) that accepts $L$ ...
- 301
2
votes
1
answer
325
views
What is a commutative transitive closure operator?
When reading about descriptive complexity theory, I have read about a "commutative transitive closure operator". I understand transitive closure operators, but what is a commutative transitive closure ...
- 41
9
votes
2
answers
1k
views
How can we express "$P=PSPACE$" as a first-order formula? [closed]
How can we express "$P=PSPACE$" as a first-order formula?
Which level of the arithmetic hierarchy contains this formula (and what is the currently known minimum level of the hierarchy that contains it)...
- 101
1
vote
1
answer
351
views
Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$
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 \...
- 513
4
votes
1
answer
178
views
Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$
I'm reading a paper which shows the result:
$(1)$ There is a $p$-optimal proof system for $\operatorname{TAUT}$. $\Leftrightarrow$
$(2)$ $L_{\leq}$ is a $P$-bounded logic for $P$.
Both $(1)$ and $(...
- 513
10
votes
3
answers
5k
views
Understanding least-fixed point logic
To better understand a paper I'm trying to get a brief understanding of least-fixed point logic. There are a few points where I am stuck.
If $G = (V,E)$ is a graph and
$$ \Phi(P) = \{(a,b) \mid G \...
- 513
9
votes
2
answers
301
views
Intuition behind proof systems
I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution:
$\Sigma = \{0,1\}$ ... We ...
- 513
21
votes
0
answers
270
views
Descriptive complexity characterization of TimeSpace classes
Are there descriptive complexity characterizations for TimeSpace complexity classes like $\mathsf{SC^i}= \mathsf{DTimeSpace}(n^{O(1)},O(\lg^i n))$?
- 21.3k
9
votes
1
answer
395
views
FO-uniform AC0 with some predicate
My question is about finite model theory/descriptive complexity, so $FO(R)$ will mean "first order over finite binary words, using predicates Rs and a unary predicate P true on the position of the 1 ...
- 1,521
14
votes
0
answers
306
views
Proof assistant formalizations of Finite Model Theory
I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
- 2,874
10
votes
2
answers
231
views
When does an FO property kill off NL-hardness?
Context: We consider only digraphs. Let CYCLE be the language of graphs with a cycle; it is an NL-complete problem. Let HASEDGE be the language of graphs with at least one edge. Then trivially, $\...
- 3,916
5
votes
0
answers
198
views
Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties
Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)?
Motivation
As you ...
- 21.3k
7
votes
1
answer
176
views
Using MSOL for solving BIDS problem
From "Linear Time Solvable Optimization Problems on Graphs of Bounded Clique Width" (B. Courcelle et al) we know that any problem that can be written on MSOL (Monadic Second Order Logic) has a linear ...
- 531
19
votes
5
answers
1k
views
Why do relational databases work at all, given the theoretical exponential complexity of answer finding (in the size of the query)?
It seems to be known that to find an answer to a query $Q$ over a relational database $D$, one needs time $|D|^{|Q|}$, and one cannot get rid of the exponent $|Q|$.
As $D$ can be very large, we wonder ...
7
votes
3
answers
1k
views
What is First-Order Rewritable (and FO-Query)?
I just wonder what FO Rewritable is, put an example to make it clearer for me. Also, I heard that a language that is FO Rewritable is very good, in what sense?
It is said as follow:
A class C of ...
- 223
13
votes
2
answers
516
views
MSOL optimization problems on graphs of bounded cliquewidth, with cardinality predicates
CMSOL is Counting Monadic Second Order Logic, i.e. a logic of graphs where the domain is the set of vertices and edges, there are predicates for vertex-vertex adjacency and edge-vertex incidence, ...
- 5,225
5
votes
1
answer
323
views
What is the parameterized complexity of following model checking problem?
Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$
Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$
Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$
where $tw(G)$ is the treewidth of $...
- 901
2
votes
3
answers
152
views
Searching for matching queries
Suppose you have a large set of queries (could be in SQL form, but conceivably the same problem exists for search engine query strings or Lucene expressions, etc...) stored and you want to know which ...
- 123
10
votes
1
answer
440
views
Could a descriptive complexity version of Rice's theorem be used to separate AC0 and PSPACE?
In this question, it was mentioned that there are descriptive complexity versions of Rice's theorem. I found a proof of the following theorem:
Given a complexity class C, nontrivial properties of ...
- 5,088
9
votes
1
answer
169
views
Is testing two SO-Horn queries for equivalence decidable?
It follows from Rice's theorem that you cannot determine whether or not two Turing machines decide the same language. My question is: Does this also apply in descriptive complexity settings, ...
- 5,088
22
votes
2
answers
933
views
Are there descriptive complexity representations of quantum complexity classes?
The title more or less says it all, but I guess I could add a bit of background and some specific examples I'm interested in.
Descriptive complexity theorists, such as Immerman and Fagin, have ...
- 5,088
8
votes
1
answer
369
views
SAT in finite model theory without order
It is well known in finite model theory that without an order on the input, the expressivity is very limited. For example it is known that $FO(<,\textit{PFP})$ is equal to PSPACE, and $FO(\textit{...
- 1,521
10
votes
1
answer
487
views
Finite One-Way Permutation with Infinite Domain
Let $\pi \colon \{0,1\}^* \to \{0,1\}^*$ be a permutation. Note that while $\pi$ acts on an infinite domain, its description might be finite. By description, I mean a program that describes $\pi$'s ...
- 16.4k
20
votes
0
answers
499
views
Model-checking for three-variable logics and restricted structures
Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem
$MC(L,C)...
- 18.8k
6
votes
1
answer
162
views
Non-interesting numbers via resource-bounded properties?
There is an old joke about the smallest non-interesting number being interesting in itself (I have heard it attributed to Richard Hamming). This is then used to justify the argument that every number ...
- 18.8k
12
votes
3
answers
281
views
Is there a natural restriction of VO logic which captures P or NP?
The paper
Lauri Hella and José María Turull-Torres,
Computing queries with higher-order logics,
TCS 355 197–214,
2006.
doi: 10.1016/j.tcs.2006.01.009
proposes logic VO, variable-order logic. This ...
- 18.8k
11
votes
1
answer
625
views
Ehrenfeucht-Fraïssé games (Ajtai-Fagin in fact) for regular languages.
Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127. As $\exists$MSO on words is equivalent to regular languages, the ...
- 3,916