Existential quantification over regular predicates - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-18T07:06:55Z http://mathoverflow.net/feeds/question/100872 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/100872/existential-quantification-over-regular-predicates Existential quantification over regular predicates Alberto 2012-06-28T16:14:42Z 2013-05-31T11:00:01Z <p>A regular language over an alphabet $\Sigma$ is a subset of the set of all words over $\Sigma$ that can be accepted by some finite automaton. A regular language identifies a certain property of strings of $\Sigma^*$.</p> <p>One can then define a regular predicate over $\Sigma^*$</p> <p>as an n-ary relation on $\Sigma^*$ such that by suitably coding n-tuples of words as single words (see for example Blumensath and Gradel) one obtains a regular language (over a new alphabet). If $R(x,y)$ is a regular binary predicate, what can be the status of the unary predicate $\exists x.R(x,y)$? (again regular, decidable, r.e., or what else?)</p> http://mathoverflow.net/questions/100872/existential-quantification-over-regular-predicates/100948#100948 Answer by Alberto for Existential quantification over regular predicates Alberto 2012-06-29T15:56:26Z 2012-06-29T15:56:26Z <p>I think I found a reference for the answer. It should be in the following paper:</p> <p>S. Eilemberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by n-tape automata, Journal of Algebra, vol. 13, (1969), pp. 447-464. </p> <p>Unfortunately I cannot download it from the internet.</p> http://mathoverflow.net/questions/100872/existential-quantification-over-regular-predicates/132277#132277 Answer by Sam Nead for Existential quantification over regular predicates Sam Nead 2013-05-29T21:17:26Z 2013-05-31T11:00:01Z <p>I believe that this is Theorem 1.4.6 (predicate calculus) in the book "Word processing in groups". However, I find their discussion somewhat confusing -- I came here hoping for a better reference...</p> http://mathoverflow.net/questions/100872/existential-quantification-over-regular-predicates/132288#132288 Answer by The User for Existential quantification over regular predicates The User 2013-05-29T23:15:53Z 2013-05-30T01:01:58Z <p>That is a central point about automatic structures: By projection (“existential quantification”) you get another regular predicate, and regular predicates are also closed under intersection and complementation. Consequently, the first-order theories of automatic structures are decidable (because you can decide for a given automaton whether he accepts any word).</p> <p>The proof is quite simple: You want to project $x$ away—just simulate every possible input for $x$ in parallel using sets of states of the old automaton as states for the new automaton (it remains a finite state machine, since the power set of a finite set is finite).</p> <p>As conjectured above you can also prove it using the MSO translation, let me sketch it: You have regular predicate $R(x,y)$ defined using a MSO formula. This MSO formula uses relation symbols $X_{(a,b)}$ to refer to “the set of positions where $x$ has character $a$ and $y$ has character $b$”. For the projection add existential second-order quantifiers $\exists Q_1\ldots Q_n$ (where $\Sigma=\left\{1,\ldots,n\right\}$) and replace the occurencesof $X_{(a,b)}$ by $X_b\wedge Q_a$ and add an expression expressing that the sets $Q_a$ build a partition. This is not yet correct, because it does not consider different lengths of $x$ and $y$ and we have to deal with some trailing characters, but that is as easy. However–the whole MSO-based proof is much more complicated than constructing an automaton directly.</p> <p>Notice that both proofs can be transfered to $\omega$-automata and finite and infinite tree-automata.</p>