# Differences

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

 expressing_regular_expressions_in_msol_over_strings [2007/05/06 21:01]vkuncak expressing_regular_expressions_in_msol_over_strings [2007/05/06 21:04] (current)vkuncak Both sides previous 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 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 ====== - - See 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 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 Line 12: 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\$