12
FO(LFP) captures PTIME on ordered structures, and strings are ordered structures. So the languages definable by FO(LFP) include all regular languages and much much more.
http://dx.doi.org/10.1016/S0019-9958(86)80029-8
Ebbinghaus and Flum's textbook contains an exercise that asks to show FO(TC^1) (first-order logic extended with transitive closures of ...
11
Here is one possibility, but other people might use different words. I will use first-order logic as a running example.
Language
The language is a collection of expressions, which are syntactic entities, i.e., finite configurations without any a priori meaning. A language is described by the grammar, which determines which finite configurations are valid ...
9
Consider the boolean algebra formed from the powerset of a finite set $S$, ordered by set inclusion. Now, consider the operator $P$ defined by
$$
P(X) = \lnot X
$$
Clearly $P$ is a non-positive operator.
Show that there are no fixed points $\mu P$ such that $P(\mu P) = \mu P$. As a result, you can conclude that $\mu X.\;P(X)$ cannot be well-defined.
...
9
If you are having trouble with the concept of least fixed point, I would recommend spending some time getting a background in more general order theory.
Davey and Priestley, Introduction to Lattices and Order is a good intro.
To see why the transitive closure is the least fixed point, imagine building up the closure from an empty set, applying the logical ...
8
You can express that $s$ is connected to $t\ne s$ in $G=(V,E)$ by the $\exists\mathrm{MSO}_2$ formula
“there exists $E'\subseteq E$ such that in the graph $(V,E')$, $s$ and $t$ have degree $1$, and all other vertices have degree $0$ or $2$.”
Note that the formula after the initial $\exists E'$ quantifier is first-order.
A graph of degree $\le2$ is a ...
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 ...
8
As far as I understand, linear logic can only express statements about structures that have quite restrictive form. I would ideally like to see a reference to, or a sketch of, a logic that can express properties of arbitrary sets of relational structures, while still avoiding fixed points. If I am wrong about the expressive power of linear logic then a ...
8
This answer is a bit late, but it is known that one can obtain all and only the regular languages by adjoining a generalized group quantifier for each finite group (or equivalently for each finite simple group). Eg, see "Regular Languages Definable by Lindstrom Quantifiers" by Zoltan Esiky and Kim G. Larsen, at http://www.brics.dk/RS/03/28/BRICS-RS-03-28.pdf....
7
It's Exercise 8.6.3 on page 221 of the second edition of Ebbinghaus and Flum's textbook, Finite Model Theory. The notation FO(TC$^r$) is explained there. FO(TC$^r$) can form the transitive closure of a $2r$-ary relation, regarded as a binary relation on $r$-tuples.
I found some more references you might be interested in.
FO(TC$^1$) is called FO(MTC) (...
7
Parity cannot be expressed in MSOL (see for instance http://www.cs.technion.ac.il/~janos/COURSES/236331-15/Lec-1.pdf), but connectedness Yes. Using instead $C_2$MSOL, one can express the existence of an eulerian cycle by using the equivalent characterisation : connected and every vertex has degree even.
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
The main conferences where automata are among the main topics are ICALP, LICS, STACS, CSL, MFCS, FSTTCS.
If you feel your paper is not strong enough for these conferences (which accept about a quarter of the papers that are sent each year), you can send to conferences which are a little less exigeant.
The ICALP submission deadline is soon (in a week), ...
5
Let your original state machine $M(k)$ have $n$ states and transition relation $t(s,s')$, where each transition $t(s,s')$ updates the global variables $x_1,...,x_k$ by applying function
$(x'_1,...,x'_k) = f_{t(s,s')} (x_1,...,x_k)$.
Then $M(k)$ is equivalent to a standard FSM with $n(2r+1)^k$ states, where each state encodes a tuple $(s,...
5
You could start with the survey article by Peter Hinman, Recursion on Abstract Structures, Chapter 11 of the Handbook on Computability Theory (editor E. R. Griffor). If you follow the references there you'll find a wealth of material.
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]$, ...
5
I am not completely sure what you are looking for, but the following might
be interesting to you:
The idea that restricting numerical predicates in FO-formula corresponds to uniformity conditions is explicitly investigated, for example, in the paper
"FO(<)-uniformity" by Behle and Lange.
The survey "Arithmetic, first-order logic, and counting ...
5
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 ...
3
Part of the answer is in your question: if your language is FO-rewritable, query answering is in $\textrm{AC}_0$ in data complexity, which is almost as good as it gets. However, keep in mind that you have to pay the cost of computing $Q_\Sigma$, which might be expensive, though you have to do it only once.
Other good thing is that, for a FO-rewritable ...
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
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 ...
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
