Büchi–Elgot–Trakhtenbrot theorem

Short description: Formal language theorem

In formal language theory, the Büchi–Elgot–Trakhtenbrot theorem states that a language is regular if and only if it can be defined by a formula in monadic second-order logic (MSO). The theorem is due to Julius Richard Büchi, Calvin Elgot, and Boris Trakhtenbrot.

Since a language is regular if and only if it can be defined as the accepted language of a finite-state automaton, a more precise statement of the theorem is that for every MSO formula defining a formal language, we can find a finite-state automaton defining the same language, and for every finite-state automaton, we can find an MSO formula defining the same language.

Examples

Regular languages are usually described by regular expressions. For instance, $(ab{)}^{*}$ represents the regular language of words where the pattern $ab$ is repeated:

$ϵ,ab,abab,ababab,abababab,\dots$

The same language is represented by the following monadic second-order logic formula (in this case a first-order logic formula). The variables represent word indices (positions), and the predicate $S(x,y)$ denotes the successor relation $y=x+1$.

$\begin{array}{l}(\mathrm{\exists }x\mathrm{\forall }y\mathrm{\neg }S(y,x)\wedge a(x))\\ \wedge (\mathrm{\exists }x\mathrm{\forall }y\mathrm{\neg }S(x,y)\wedge b(x))\\ \wedge (\mathrm{\forall }x\mathrm{\forall }y(S(x,y)\wedge a(x))\to b(y))\\ \wedge (\mathrm{\forall }x\mathrm{\forall }y(S(x,y)\wedge b(x))\to a(y))\\ \end{array}$

In words:

• There is a position $x$ which is the beginning of the word and has letter $a$.
• There is a position $x$ which is the end of the word and has letter $b$.
• Any position following a letter $a$ must have letter $b$.
• Any position following a letter $b$ must have letter $a$.

A second example is the regular expression $(aa{)}^{*}$. This language cannot be expressed in first-order logic and needs the second-order quantification of MSO. We introduce an $\text{EVEN}$ predicate that is exactly true on positions that are even. The following MSO formula says that all letters are $a$, that $\text{EVEN}$ is true at every even index, and that $\text{EVEN}$ is true at the ending position.

$\begin{array}{l}(\mathrm{\forall }xa(x))\wedge \mathrm{\exists }\text{EVEN}\\ (\mathrm{\exists }x\mathrm{\forall }y\mathrm{\neg }S(y,x)\wedge \mathrm{\neg }\text{EVEN}(x))\\ \wedge (\mathrm{\exists }x\mathrm{\forall }y\mathrm{\neg }S(x,y)\wedge \text{EVEN}(x))\\ \wedge (\mathrm{\forall }x\mathrm{\forall }y(S(x,y)\wedge \text{EVEN}(x))\to \mathrm{\neg }\text{EVEN}(y))\\ \wedge (\mathrm{\forall }x\mathrm{\forall }y(S(x,y)\wedge \mathrm{\neg }\text{EVEN}(x))\to \text{EVEN}(y))\\ \end{array}$

Setup

Let $\mathrm{\Sigma }$ be a finite nonempty set, called the alphabet. A formal language is a subset of ${\mathrm{\Sigma }}^{*}$, the set of finite-length strings formed by elements of $\mathrm{\Sigma }$. A language is regular if and only if it is accepted by a finite-state automaton.

In order to define languages using logical formulas, we need the following logical formalism. Other than the first-order logic symbols, it also has the following predicates:

• The equality relation $=$.
• One monadic relation $Q_a$ per letter $a\in \mathrm{\Sigma }$, where $Q_a(x)$ means "location $x$ contains letter $a$".
• The successor relation $S(x,y)$, meaning "location $x$ is immediately followed by location $y$".
  • Since in MSO logic we can quantify over all monadic predicates, the successor relation can be used to define an ordering relation $x<y$ as the transitive closure of $S(x,y)$:$$\mathrm{\neg }x=y\wedge \mathrm{\forall }X(X(x)\wedge \mathrm{\forall }z,z^{\prime }(X(z)\wedge S(z,z^{\prime })\to X(z^{\prime }))\to X(y))$$This construction is similar to the induction principle in Peano arithmetic.

With this formalism, one can characterize a language by a single MSO formula $\sigma$. Specifically, $\sigma$ defines the set $L_{\sigma }:=\{w\in {\mathrm{\Sigma }}^{*}:M_w\models \sigma \}$. In this definition, to each word $w\in {\mathrm{\Sigma }}^{*}$, we define a finite model $M_w$ with the following conditions:

• The universe of $M_w$ is $\{1,2,\dots ,|w|\}$.
• For each $n\in \{1,2,\dots ,|w|\}$, we have $M_w\models Q_a(n)$ if and only if $w_n=a$.
• For each $n,m\in \{1,2,\dots ,|w|\}$, we have $M_w\models S(n,m)$ if and only if $m=n+1$.

Any such language $L_{\sigma }$ is said to be MSO-expressible.

Theorem statement

A language $L\subseteq {\mathrm{\Sigma }}^{*}$ is regular iff it is MSO-expressible.

Proof overview

Regular implies MSO-expressible

Given a regular language $L$, it is specified by a finite-state automaton with $k$ states. Then, one constructs a MSO formula of the form $\mathrm{\exists }{X}_1,\dots ,X_k,\varphi (X_1,\dots ,X_k)$. Here, each $X_i$ is supposed to be interpreted as the set of locations at which the automaton is at state $i$. The formula $\varphi (X_1,\dots ,X_k)$ then expresses the following:

• Any location belongs to exactly one of $X_1,\dots ,X_k$, and
• the state transition at each location follows the automaton's edge rules, and
• the last location is in one of the accepting states.

More concretely, we can construct the formula as a conjunction of the following:

• $\mathrm{\forall }x,\underset{i:1\le i\le n}{\bigvee }(X_i(x)\wedge \underset{j:j\ne i,1\le j\le n}{\bigwedge }\mathrm{\neg }{X}_j(x))$.
• $\mathrm{\forall }x,y,S(x,y)\to \underset{i:1\le i\le n,a\in \mathrm{\Sigma }}{\bigvee }{X}_i(x)\wedge Q_a(x)\wedge X_{A(i,a)}(y)$, where we use $A(i,a)$ to mean: the state you arrive at, if you start at state $i$ on the automaton and follow the edge for letter $a$.
  • In this part, we assume that the automaton is deterministic. This can be generalized easily to the nondeterministic case.
• $\mathrm{\forall }x(\mathrm{\neg }\mathrm{\exists }yS(x,y))\to \underset{a\in \text{accepting states}}{\bigvee }{Q}_a(x)$.

MSO-expressible implies regular

Conversely, to show that each MSO formula defines a language that is regular, it suffices to induct over the syntax of MSO formulas. This boils down to induction over $\mathrm{\neg },\wedge$, and existential quantification over monadic predicates. These correspond to complement, intersection, and projection (a restricted kind of homomorphism). The set of regular languages over $\mathrm{\Sigma }$ is closed under complement, intersection, and projection.

See also

• Trakhtenbrot's theorem
• Courcelle's theorem