Existential quantification over regular predicates - MathOverflow

Existential quantification over regular predicates

2012-06-28T16:14:42Z

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^*$.

One can then define a regular predicate over $\Sigma^*$

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?)

Answer by Alberto for Existential quantification over regular predicates

2012-06-29T15:56:26Z

I think I found a reference for the answer. It should be in the following paper:

S. Eilemberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by n-tape automata, Journal of Algebra, vol. 13, (1969), pp. 447-464.

Unfortunately I cannot download it from the internet.

Answer by Sam Nead for Existential quantification over regular predicates

2013-05-29T21:17:26Z

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...

Answer by The User for Existential quantification over regular predicates

2013-05-29T23:15:53Z

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).

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).

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.

Notice that both proofs can be transfered to $\omega$-automata and finite and infinite tree-automata.