# Differences

This shows you the differences between two versions of the page.

 expressing_regular_expressions_in_msol_over_strings [2007/05/06 20:59]vkuncak created expressing_regular_expressions_in_msol_over_strings [2007/05/06 21:04]vkuncak 2007/05/06 21:04 vkuncak 2007/05/06 21:01 vkuncak 2007/05/06 21:01 vkuncak 2007/05/06 20:59 vkuncak created Next revision Previous revision 2007/05/06 21:04 vkuncak 2007/05/06 21:01 vkuncak 2007/05/06 21:01 vkuncak 2007/05/06 20:59 vkuncak created Line 1: Line 1: ====== Expressing regular expressions in MSOL over strings ====== ====== Expressing regular expressions in MSOL over strings ====== - Idea: for each regular expression \$r\$ of alphabet ​with inputs \$v_1,​\ldots,​v_n\$ associate a formula \$F\$ with free variables \$v_1,​\ldots,​v_n,​p,​q\$ such that \$F\$ is valid precisely for whose sets of numbers for which + Idea: for each regular expression \$r\$ of a [[regular expressions for automata ​with parallel ​inputs|automaton for parallel inputs]] ​\$v_1,​\ldots,​v_n\$ associate a formula \$F\$ with free variables \$v_1,​\ldots,​v_n,​p,​q\$ such that \$F\$ is valid precisely for whose sets of numbers for which * \$p\$ and \$q\$ are singletons * \$p\$ and \$q\$ are singletons * the strings given by the parts of \$v_1,​\ldots,​v_n\$ that start at position \$p\$ and end at position \$q\$ satisfy regular expression \$F(r)\$ * the strings given by the parts of \$v_1,​\ldots,​v_n\$ that start at position \$p\$ and end at position \$q\$ satisfy regular expression \$F(r)\$ Line 10: Line 10: ... ...     ... ... ... ...     ... ... ... apn ... aqn ... ... apn ... aqn ... + + The construction is by induction on the structure of regular expressions and resembles the description of parsing the string given by a regular expression: + * base cases are easy + * union is disjunction + * concatenation existentially quantifies over middle position + * iteration in \$r^*\$ quantifies over a set of positions between \$p\$ and \$q\$ at which a string can be broken into strings that satisfy \$r\$