Tags:
, view all tags
Buchi's Theorem

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

Proof

Regular → Second-order monadic

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.

Second-order monadic Regular


-- SvorotnI - 2012-04-22

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r2 - 2012-04-22 - SvorotnI
 
  • Edit
  • Attach
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 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

mersin escort adana escort izmir escort gaziantep escort