LARA

Differences

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

Link to this comparison view

Next revision
Previous revision
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] (current)
vkuncak
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$