Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
msol_over_strings [2007/05/27 13:44] vaibhav.rajan |
msol_over_strings [2008/05/14 19:23] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== MSOL over Strings ====== | ====== MSOL over Strings ====== | ||
| - | |||
| - | |||
| - | |||
| ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings ===== | ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings ===== | ||
| Line 29: | Line 26: | ||
| [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0 \land [\![F]\!](e[v \mapsto S]) | [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0 \land [\![F]\!](e[v \mapsto S]) | ||
| \end{eqnarray*} | \end{eqnarray*} | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| ===== What can we express in MSOL over strings ===== | ===== What can we express in MSOL over strings ===== | ||
| Line 59: | Line 51: | ||
| \end{equation*} | \end{equation*} | ||
| - | This does not give the smallest set containing both $u$ and $v$. The reflexive transitive closure, T is: | ||
| - | \begin{equation*} | ||
| - | (F \subseteq T )\land (\forall x. x \in S \rightarrow (x,x) \in T ) \land ((\exists k.(u,k) \in T \land (k,v) \in T) \rightarrow ((u,v) \in T)) | ||
| - | \end{equation*} | ||
| - | The underlying smallest set S containing $u$ and $v$ is given by: | ||
| - | \begin{equation*} | ||
| - | S = \{x | \exists k. ((k, x) \in T \lor (x,k) \in T) \} | ||
| - | \end{equation*} | ||
| **Using transitive closure and successors:** | **Using transitive closure and successors:** | ||
| * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land s(y,x))$ | * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land s(y,x))$ | ||