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>
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8345661163330078, "perplexity": 672.4917611524396}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2013-20/segments/1368707184996/warc/CC-MAIN-20130516122624-00052-ip-10-60-113-184.ec2.internal.warc.gz"}