18

Context: relations between logic and automata

Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that existential MSO ($\exists\text{MSO}$ or EMSO) over strings is enough to capture regular languages. This might be a bit surprising, since, over general structures, MSO is strictly more expressive than $\exists\text{MSO}$.

My (original) question: a minimal logic for regular languages?

Is there a logic which, over general structures, is strictly less expressive than $\exists\text{MSO}$, but that still captures the class of regular languages when considered over strings?

In particular, I'd like to know what fragment of the regular languages is captured by FO over strings when extended with a least-fixed point operator (FO+LFP). It seems like a natural candidate for what I'm looking for (if it is not $\exists\text{MSO}$).

A first answer

As per @makoto-kanazawa's answer, both FO(LFP) and FO(TC) capture more than regular languages, where TC is an operator of transitive closure of binary relations. It remains to be seen whether TC can be replaced by another operator or set of operators in such a way that the extension captures exactly the class of regular languages, and no others.

First-order logic alone, as we know, is not enough, since it captures star-free languages, a proper subclass of the regular languages. As a classical example, the language Parity$\;\;=(aa)^*$ cannot be expressed using a FO sentence.

Updated question

Here is a new wording of my question, which remains unanswered.

What is the minimal extension of first-order logic such that FO + this extension, when taken over strings, captures exactly the class of regular languages?

Here, an extension is minimal if it is the least expressive (when taken over general structures) among all extensions that capture the class of regular languages (when taken over strings).

Community
  • 1
Janoma
  • 1,406
  • 11
  • 27
  • If I am not mistaken, $\mu$-calculus is indeed equivalent to MSO over strings. – Sylvain Jan 27 '12 at 22:11
  • @Sylvain, any reference? I don't know anything about $\mu$-calculus. – Janoma Jan 27 '12 at 22:15
  • 1
    It appears to be proven in http://dx.doi.org/10.1109/LICS.1988.5137 for the infinite tree, and in http://dx.doi.org/10.1007/3-540-61604-7_60 for the equivalence with the bisimulation-invariant fragment of MSO over arbitrary structures. – Sylvain Jan 27 '12 at 22:27
  • I'm taking a look at the second paper, though I'm afraid many concepts are new to me. In particular, I didn't know about bisimulation-invariant transition systems. It appears to be that DFA are particular cases of a transition system, but I don't know if they are bisimulation-invariant. If they are, that would answer part of my question (there could be yet another less expressive logic for regular languages); if they are not, I think nothing can be said, for there could still be an equivalence when considering strings only. – Janoma Jan 27 '12 at 23:19
  • Two finite words, seen as transition systems, are bisimilar iff they are isomorphic. (In the notations of the second paper, a word $a_1\cdots a_n$ in $\Sigma^\ast$ with $\Sigma=2^{\mathit{Prop}}$ can be seen as a transition system $\langle{1,\dots,n},1,{(i,i+1)\mid i<n},{i\mid p\in a_i}_{p\in\mathit{Prop}}\rangle$.) – Sylvain Jan 28 '12 at 00:47
  • It's not clear to me what would make an extension minimal. For instance, you could imagine that ext1 and ext2 coincide on strings but might capture incomparable classes of general structures. Also, why should you restrict yourself to full FO+ext? As the case of the $\mu$-calculus indicates, bisimulation-invariant logics are sufficient for strings, for instance one might venture that PDL (propositional dynamic logic) would be enough. – Sylvain Feb 13 '12 at 18:35
  • @Sylvain Yep, it could be the case that two extensions coincide over strings but are not comparable over general structures. The reason I want to know about a minimal extension of FO is because I'm interested in the "gap" between FO and SO over different structures, make some kind of hierarchy. I don't have it clear myself, it is something I have to talk about with my future advisor if I ever start a PhD in TCS (possible question about career advice there as well). – Janoma Feb 13 '12 at 18:46

3 Answers3

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 binary relations) is equivalent to MSO on strings. In the same exercise, $\{ a^n b^n \mid n \geq 1 \}$ is used as an example to show FO(TC^2) is more expressive than MSO on strings. All FO(TC) formulas are clearly equivalent to FO(LFP) formulas.

Makoto Kanazawa
  • 191
  • 3
  • Excellent. I don't know what you mean by TC^1 and TC^2, is that a typo? As far as I know, in the book you mention the notation used is FO(TC) for the extension of FO with transitive closure and FO(DTC) for the extension of FO with deterministic transitive closure, which is defined differently. I haven't found the exercise you mention, though. It remains to see whether there is an operator less expressive than TC that still allows to capture regular languages. I will update my question accordingly. – Janoma Jan 30 '12 at 22:45
10

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.

Moreover, this is optimal in the sense that a regular language will only be definable if the quantifiers for every group dividing its syntactic monoid are available.

Ben Standeven
  • 261
  • 2
  • 4
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) (first-order logic with monadic transitive closure) in ten Cate and Segoufin's 2010 paper. It proves, among other things, FO(MTC) is strictly less expressive than MSO on finite trees.

Bargury and Makowsky's 1992 paper shows that deterministic monadic transitive closure—FO(DTC$^1$) in Ebbinghaus and Flum's notation—suffices to define regular string languages (see Theorem 5 in this paper).

Makoto Kanazawa
  • 191
  • 3