6
$\begingroup$

A language $L \subseteq \Sigma^*$ can be described by a regular expression iff it can be defined by a formula in monadic second order with words as structure $(\{0, \dots, n-1\}, <, (P_a)_{a \in \Sigma})$. The proof I know is an indirection construction over automata, i.e. we show that DFAs and regular expressions / formulas are equivalently powerful.

However, I am interested in a direct transformation process to make analysis of complexity properties easier. If I remember correctly, there is a construction based on the inductive nature of regular expressions and formulas, but I cannot find it. Just a link to a paper presenting these two algorithms (reg.exp. to MSO and back) would suffice for me.

Improve this question
$\endgroup$
2
  • $\begingroup$ Union is easy. Concatenation should be based on relativization (formula is true when restricted to certain positions), and star seems transitive closure. But you are asking for explicit references on the corresponding descriptive complexities. Did not find those, sorry. $\endgroup$
    – Hendrik Jan
    Oct 5, 2015 at 13:16
  • $\begingroup$ No, I am not asking for complexities. I am asking for for a detailed description of the constructions. $\endgroup$
    – Andreas T
    Oct 5, 2015 at 13:30

1 Answer 1

Reset to default
6
$\begingroup$

The direction from regular expressions to MSO is easy, as MSO is versatile. For a regular expressions $R$ let us construct formulae $\varphi_R$.

$\varphi_{\emptyset} := \bot$

$\varphi_{\varepsilon} := \forall x\bot$

$\varphi_a := \exists x(P_a x \wedge \forall y(x=y))$

$\varphi_{R_1 | R_2} := \varphi_{R_1} \vee \varphi_{R_2}$.

$\varphi_{R_1R_2} := \exists X(\forall y\forall z((Xy \wedge \neg Xz)\to y<z) \wedge [\varphi_{R_1}]_{Xx} \wedge [\varphi_{R_2}]_{\neg Xx})$

$\varphi_{R*} := \exists X(\forall y\forall z((\forall x((\neg x<y \wedge \neg z<x)\to(Xx\leftrightarrow Xy))) \wedge \forall x((x<y\wedge(Xx\leftrightarrow Xy))\to\exists x'(x<x'\wedge x'<y\wedge\neg(Xx'\leftrightarrow Xy))) \wedge \forall x((z<x\wedge(Xx\leftrightarrow Xy))\to\exists x'(z<x'\wedge x'<x\wedge\neg(Xx'\leftrightarrow Xy)))) \to [\varphi_R]_{\neg x<y \wedge \neg z<x})$

Here, $[\varphi]_{\psi(x)}$ denotes the relativization of the formula $\varphi$ to the formula $\psi$.

As you can see, the translation is linear.

In the other direction, I suggest to transform MSO to regular expressions in two steps, with NFAs in between. I know this is not what you are asking for. For complexity analysis it should suffice, however: The translation from MSO to NFAs is known not to have any elementary lower bound. And a direct translation to regular expressions cannot be any better, because of the linear translation from regular expressions to NFAs.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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