# How to convert regular expressions into predicate logic?

I've been given the problem to describe the language of, "The set of strings beginning with ab." with predicate logic using quantifiers. The issue I don't have a systematic approach to do this with.

I first defined a boolean predicate, "Pred" which just returns a boolean value if one variable is a predecessor of another.

$$Pred(y, x) = ( y < x ) \land \forall z: ( z \leq y) \land (z \ge x)$$

Another predicate is just to determine if the first letter is A is :

$$Initial(a) = \exists x: C_a(x) \land \forall y: x \leq y$$

Where $C_a(x)$ means that "the character at position x is the character a."

From here, I need to combine the two definitions I've created to come up with a language that describes the set of strings beginning with ab.

You need a small correction to your predecessor definition. For instance: $$\operatorname{Pred}(y,x) := (y < x) \wedge \forall z \,.\, (z \leq y) \vee (x \leq z) \enspace.$$

Instead of $\operatorname{Initial}(a)$, you may want to define $$\operatorname{Initial}(x) := \forall y \,.\, x \leq y \enspace.$$

From these two predicates you can build second, third, .... For the language of all words that start with $ab$, you could write

$$\forall x \,.\, \forall y \,.\, \operatorname{Initial}(x) \rightarrow \Big(C_a(x) \wedge \big(\operatorname{Pred}(x,y) \rightarrow C_b(y)\big)\Big) \enspace.$$

In general, a word language over a finite alphabet is first-order definable (with signature $<$) if and only if it is star-free. Hence you won't find a systematic procedure to translate an arbitrary regular expression into a first-order formula. If, however, you are given a star-free extended regular expression, then translation is algorithmic and not too hard.

First, "start-free expression" means that the expression doesn't contain any Kleene stars. Second, "extended" means that complementation is allowed. The translation proceeds recursively.

Let $\Sigma$ be the alphabet. The FOL formula for the empty language is $\bot$ (false). This means that the formula for $\Sigma^*$ is $\top$ (true). (Even though $\Sigma^*$ is not a star-free expression, the language it defines is star-free, because it can also be described as the complement of the empty language.)

A formula for the expression $a$, with $a \in \Sigma$, is $$\exists x \,.\, (\forall w \,.\, w = x) \wedge C_a(x) \enspace.$$

A formula for the empty string $\epsilon$ is $$\forall x \,.\, \bigwedge_{\sigma \in \Sigma} \neg C_\sigma(x) \enspace.$$

These are all the base cases. For the recursive step, union maps to disjunction, intersection maps to conjunction, and complementation maps to negation. Since there is no star, this only leaves concatenation, for which we introduce the relativizations of a formula $\varphi$ with respect to variable $z$:

$$[\varphi]_{<z} ~~~~ [\varphi]_{\geq z} \enspace,$$

which restrict the quantifiers in $\varphi$ to the natural numbers that are less than $z$, or greater than or equal to $z$, respectively. Then, if $L_i$ translates to $\varphi_i$, then $L_1 \cdot L_2$ translates to $$\exists z \,.\, [\varphi_1]_{<z} \wedge [\varphi_2]_{\geq z} \enspace.$$

As an example, if $\Sigma = \{a,b\}$ and we wanted the formula for $\epsilon a$, we'd start with \begin{align*} \varphi_1 &:= \forall x \,.\, \neg C_a(x) \wedge \neg C_b(x) \\ \varphi_2 &:= \exists y \,.\, (\forall w \,.\, w = y) \wedge C_a(y) \enspace. \end{align*} We would then compute \begin{align*} [\varphi_1]_{<z} &:= \forall x \,.\, x < z \rightarrow (\neg C_a(x) \wedge \neg C_b(x)) \\ [\varphi_2]_{\geq z} &:= \exists y \,.\, z \leq y \wedge (\forall w \,.\, z \leq w \rightarrow w = y) \wedge C_a(y) \enspace. \end{align*} Finally, \begin{align*} \exists z \,.\, [\varphi_1]_{<z} \wedge [\varphi_2]_{\geq z} &:= \exists z \,.\, \Big(\forall x \,.\, x < z \rightarrow (\neg C_a(x) \wedge \neg C_b(x))\Big) \,\wedge \\ &\enspace\quad \Big(\exists y \,.\, z \leq y \wedge (\forall w \,.\, z \leq w \rightarrow w = y) \wedge C_a(y)\Big) \enspace. \end{align*} This is rather horrible-looking--a bit like the regular expressions or MSO formulae one mechanically extracts from automata--but if we notice that the first "half" of the formula implies $z=0$, things work out OK and eventually we get $\varphi_2$ back.