Buchi's Theorem

A language is definable in second-order monadic logic if and only if it is regular.

Proof

Let L be a regular language with associated DFA D = (Q, q1, δ, F). We construct a formula Φ describing an accepting run of D on a string (Φ is true iff there is an accepting run of D on the string).

Let Q = {q1, q2,..., qn).

Φ can be described as: ∃C1∃C2...∃Cn: ∀x: ( should be in some state) ∧ ( can be in only 1 state) ∧ (zero(x) → start at q1) ∧ ( follow the right transitions) ∧ (last(x) → end at a final state)

• should be in some state: [C1(x) ∨ C2(x) ∨ ... ∨ Cn(x)]
• can be in only 1 state: for every pair of states qi, qj, add the following: [Ci(x) → ¬Cj(x)]. Connect these together with ∧.
• start at q1: C1(x)
• follow the right transitions: for every transition δ(qi, a) = qj, add the following: [(Ci(x) ∧ Ia(x)) → Cj(x+1)]. Connect these together with ∧.
• end at a final state: for every transition δ(qi, a) = qj such that qj∈F, add the following: [Ia(x) ∧ Ci(x)]. Connect these together with ∨.
zero(x) - x is the beginning of the string, (x+1), and last(x) - x is the end of the string, can be easily described in first-order logic.

If we have a formula with variables x, y, A, B, we can mark a string w with them. Each x and y can mark 1 position in w. A and B can mark sets of positions.

Let string w satisfy formula Φ with free variables x, y, A, B.

Assume a DFA MΦ decides (w, x, y, A, B) satisfies Φ.

• Build an NFA M'Φ that decides (w, y, A, B) satisfies ∃x:Φ. Non-deteministically guess which position is marked by x. Then run MΦ on the input with guessed x.
• Build an NFA M'Φ that decides (w, x, y, B) satisfies ∃A:Φ. For each position non-deterministically guess if it is marked by A. Then run MΦ on the input with guessed A's.
• Build a DFA M'Φ that decides (w, y, A, B) satisfies ∀x:Φ. Check each possible marking with x using MΦ.
• Build a DFA M'Φ that decides (w, x, y, B) satisfies ∀A:Φ. Check each possible marking with A's using MΦ.
Base case: Booleans, (x ≤ y), Ia(x), A(x) are all regular.

-- SvorotnI - 2012-04-22

Topic revision: r3 - 2012-04-23 - SvorotnI

 Home H401 Web P View Edit Account
Copyright © 2008-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UMass CS EdLab? Send feedback