Descriptive complexity is the study of the relative difficulty of formal languages based on the

syntactic resources needed to create logical formulas defining them.

We've defined first-order logic, where variables represent positions in the input string, the

atomic formulas are "Ia(x)" (position x holds an a), x = y, and x ≤ y, we have boolean

connectives, and we have first order forall and exists quantifiers.

-- BarrinG - 2012-02-27


Theorem

A language is first-order definable iff it is star-free regular.

Proof

Star-free → first-order

We show that the following elements of a star-free expression can be expressed in first-order logic:

∅ (empty set): ∃x: x≠x

a (letter in Σ): ∃x:∀y: (y=x) ∧ Ia(x)

‾ (complement): If ΦX is the first-order formula for a star-free expression X, then ΦX is the formula for expression X

∪ (union): If ΦX and ΦY are the first-order formulas for star-free expressions X and Y, then ΦX∨ΦY is the formula for expression X∪Y

• (concatenation): Let ΦX and ΦY be the first-order formulas for star-free expressions X and Y. Informally, the formula for XY would be the following:

∃z: (w1w2...wz satisfies ΦX) ∧ (wz+1...wn satisfies ΦY), where w1w2...wn is a string over Σ.

The first part (call it Φ≤z) can be constructed from ΦX in the following way: replace each "∃x" with "∃x: (x≤z) ∧" and each "∀x" with "∀x: (x≤z) →". Analogously we construct the second part.

-- SvorotnI - 2012-03-25


Buchi's Theorem says that a language is definable in second-order monadic logic iff it is regular. (See the page with the theorem for the proof.)

-- SvorotnI - 2012-03-12


Topic revision: r5 - 2012-04-22 - SvorotnI
 
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 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