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, ( a b ) ∗ {\displaystyle (ab)^{*}} represents the regular language of words where the pattern a b {\displaystyle ab} is repeated:
ϵ , a b , a b a b , a b a b a b , a b a b a b a b , … {\displaystyle \epsilon ,ab,abab,ababab,abababab,\ldots }
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 ) {\displaystyle S(x,y)} denotes the successor relation y = x + 1 {\displaystyle y=x+1} .
( ∃ x ∀ y ¬ S ( y , x ) ∧ a ( x ) ) ∧ ( ∃ x ∀ y ¬ S ( x , y ) ∧ b ( x ) ) ∧ ( ∀ x ∀ y ( S ( x , y ) ∧ a ( x ) ) → b ( y ) ) ∧ ( ∀ x ∀ y ( S ( x , y ) ∧ b ( x ) ) → a ( y ) ) {\displaystyle {\begin{array}{l}(\exists x\;\forall y\;\lnot S(y,x)\land a(x))\\\land (\exists x\;\forall y\;\lnot S(x,y)\land b(x))\\\land (\forall x\forall y\;(S(x,y)\land a(x))\rightarrow b(y))\\\land (\forall x\forall y\;(S(x,y)\land b(x))\rightarrow a(y))\\\end{array}}}
In words:
There is a position x {\displaystyle x} which is the beginning of the word and has letter a {\displaystyle a} . There is a position x {\displaystyle x} which is the end of the word and has letter b {\displaystyle b} . Any position following a letter a {\displaystyle a} must have letter b {\displaystyle b} . Any position following a letter b {\displaystyle b} must have letter a {\displaystyle a} . A second example is the regular expression ( a a ) ∗ {\displaystyle (aa)^{*}} . This language cannot be expressed in first-order logic and needs the second-order quantification of MSO. We introduce an EVEN {\displaystyle {\text{EVEN}}} predicate that is exactly true on positions that are even. The following MSO formula says that all letters are a {\displaystyle a} , that EVEN {\displaystyle {\text{EVEN}}} is true at every even index, and that EVEN {\displaystyle {\text{EVEN}}} is true at the ending position.
( ∀ x a ( x ) ) ∧ ∃ EVEN ( ∃ x ∀ y ¬ S ( y , x ) ∧ ¬ EVEN ( x ) ) ∧ ( ∃ x ∀ y ¬ S ( x , y ) ∧ EVEN ( x ) ) ∧ ( ∀ x ∀ y ( S ( x , y ) ∧ EVEN ( x ) ) → ¬ EVEN ( y ) ) ∧ ( ∀ x ∀ y ( S ( x , y ) ∧ ¬ EVEN ( x ) ) → EVEN ( y ) ) {\displaystyle {\begin{array}{l}(\forall x\;a(x))\land \exists {\text{EVEN}}\\(\exists x\;\forall y\;\lnot S(y,x)\land \lnot {\text{EVEN}}(x))\\\land (\exists x\;\forall y\;\lnot S(x,y)\land {\text{EVEN}}(x))\\\land (\forall x\forall y\;(S(x,y)\land {\text{EVEN}}(x))\rightarrow \lnot {\text{EVEN}}(y))\\\land (\forall x\forall y\;(S(x,y)\land \lnot {\text{EVEN}}(x))\rightarrow {\text{EVEN}}(y))\\\end{array}}}
Setup Let Σ {\displaystyle \Sigma } be a finite nonempty set, called the alphabet. A formal language is a subset of Σ ∗ {\displaystyle \Sigma ^{*}} , the set of finite-length strings formed by elements of Σ {\displaystyle \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 = {\displaystyle =} . One monadic relation Q a {\displaystyle Q_{a}} per letter a ∈ Σ {\displaystyle a\in \Sigma } , where Q a ( x ) {\displaystyle Q_{a}(x)} means "location x {\displaystyle x} contains letter a {\displaystyle a} ". The successor relation S ( x , y ) {\displaystyle S(x,y)} , meaning "location x {\displaystyle x} is immediately followed by location y {\displaystyle 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 {\displaystyle x<y} as the transitive closure of S ( x , y ) {\displaystyle S(x,y)} : ¬ x = y ∧ ∀ X ( X ( x ) ∧ ∀ z , z ′ ( X ( z ) ∧ S ( z , z ′ ) → X ( z ′ ) ) → X ( y ) ) {\displaystyle \neg x=y\wedge \forall X(X(x)\wedge \forall z,z'(X(z)\wedge S(z,z')\to X(z'))\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 σ {\displaystyle \sigma } . Specifically, σ {\displaystyle \sigma } defines the set L σ := { w ∈ Σ ∗ : M w ⊨ σ } {\displaystyle L_{\sigma }:=\{w\in \Sigma ^{*}:M_{w}\models \sigma \}} . In this definition, to each word w ∈ Σ ∗ {\displaystyle w\in \Sigma ^{*}} , we define a finite model M w {\displaystyle M_{w}} with the following conditions:
The universe of M w {\displaystyle M_{w}} is { 1 , 2 , … , | w | } {\displaystyle \{1,2,\dots ,|w|\}} . For each n ∈ { 1 , 2 , … , | w | } {\displaystyle n\in \{1,2,\dots ,|w|\}} , we have M w ⊨ Q a ( n ) {\displaystyle M_{w}\models Q_{a}(n)} if and only if w n = a {\displaystyle w_{n}=a} . For each n , m ∈ { 1 , 2 , … , | w | } {\displaystyle n,m\in \{1,2,\dots ,|w|\}} , we have M w ⊨ S ( n , m ) {\displaystyle M_{w}\models S(n,m)} if and only if m = n + 1 {\displaystyle m=n+1} . Any such language L σ {\displaystyle L_{\sigma }} is said to be MSO-expressible.
Theorem statement A language L ⊆ Σ ∗ {\displaystyle L\subseteq \Sigma ^{*}} is regular iff it is MSO-expressible.
Proof overview
Regular implies MSO-expressible Given a regular language L {\displaystyle L} , it is specified by a finite-state automaton with k {\displaystyle k} states. Then, one constructs a MSO formula of the form ∃ X 1 , … , X k , ϕ ( X 1 , … , X k ) {\displaystyle \exists X_{1},\dots ,X_{k},\phi (X_{1},\dots ,X_{k})} . Here, each X i {\displaystyle X_{i}} is supposed to be interpreted as the set of locations at which the automaton is at state i {\displaystyle i} . The formula ϕ ( X 1 , … , X k ) {\displaystyle \phi (X_{1},\dots ,X_{k})} then expresses the following:
Any location belongs to exactly one of X 1 , … , X k {\displaystyle 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:
∀ x , ⋁ i : 1 ≤ i ≤ n ( X i ( x ) ∧ ⋀ j : j ≠ i , 1 ≤ j ≤ n ¬ X j ( x ) ) {\displaystyle \forall x,\bigvee _{i:1\leq i\leq n}\left(X_{i}(x)\wedge \bigwedge _{j:j\neq i,1\leq j\leq n}\neg X_{j}(x)\right)} .
∀ x , y , S ( x , y ) → ⋁ i : 1 ≤ i ≤ n , a ∈ Σ X i ( x ) ∧ Q a ( x ) ∧ X A ( i , a ) ( y ) {\displaystyle \forall x,y,S(x,y)\to \bigvee _{i:1\leq i\leq n,a\in \Sigma }X_{i}(x)\wedge Q_{a}(x)\wedge X_{A(i,a)}(y)} , where we use A ( i , a ) {\displaystyle A(i,a)} to mean: the state you arrive at, if you start at state i {\displaystyle i} on the automaton and follow the edge for letter a {\displaystyle a} . In this part, we assume that the automaton is deterministic. This can be generalized easily to the nondeterministic case.
∀ x ( ¬ ∃ y S ( x , y ) ) → ⋁ a ∈ accepting states Q a ( x ) {\displaystyle \forall x(\neg \exists yS(x,y))\to \bigvee _{a\in {\text{accepting states}}}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 ¬ , ∧ {\displaystyle \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 Σ {\displaystyle \Sigma } is closed under complement, intersection, and projection.
See also Trakhtenbrot's theorem Courcelle's theorem
References