17
$\begingroup$

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).

Improve this question
$\endgroup$
7
  • $\begingroup$ If I am not mistaken, $\mu$-calculus is indeed equivalent to MSO over strings. $\endgroup$
    – Sylvain
    Jan 27, 2012 at 22:11
  • $\begingroup$ @Sylvain, any reference? I don't know anything about $\mu$-calculus. $\endgroup$
    – Janoma
    Jan 27, 2012 at 22:15
  • 1
    $\begingroup$ It appears to be proven in dx.doi.org/10.1109/LICS.1988.5137 for the infinite tree, and in dx.doi.org/10.1007/3-540-61604-7_60 for the equivalence with the bisimulation-invariant fragment of MSO over arbitrary structures. $\endgroup$
    – Sylvain
    Jan 27, 2012 at 22:27
  • $\begingroup$ 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. $\endgroup$
    – Janoma
    Jan 27, 2012 at 23:19
  • $\begingroup$ 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$.) $\endgroup$
    – Sylvain
    Jan 28, 2012 at 0:47

3 Answers 3

Reset to default
12
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Janoma
    Jan 30, 2012 at 22:45
10
$\begingroup$

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.

Improve this answer
$\endgroup$
7
$\begingroup$

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).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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