Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
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] vkuncak |
||
|---|---|---|---|
| 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$ | ||