LARA

Differences

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

Link to this comparison view

Both sides previous 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 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$