Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
msol_over_strings [2007/05/06 19:04] vkuncak |
msol_over_strings [2007/05/10 18:15] 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 22: | Line 24: | ||
[\![v_1 \subseteq v_2]\!]e &=& (e(v_1) \subseteq e(v_2)) \\ \ | [\![v_1 \subseteq v_2]\!]e &=& (e(v_1) \subseteq e(v_2)) \\ \ | ||
[\![s(v_1,v_2)]\!]e &=& (\exists k \in N_0. e(v_1) = \{k\} \land e(v_2)=\{k+1\}) \\ \ | [\![s(v_1,v_2)]\!]e &=& (\exists k \in N_0. e(v_1) = \{k\} \land e(v_2)=\{k+1\}) \\ \ | ||
- | [\![F_1 \lor F_2]\!]e &=& [\![F_1]\!]e\ \land\ [\![F_2]\!]e \\ \ | + | [\![F_1 \lor F_2]\!]e &=& [\![F_1]\!]e\ \lor\ [\![F_2]\!]e \\ \ |
[\![\lnot F]\!]e &=& \lnot ([\![F]\!]e) \\ \ | [\![\lnot F]\!]e &=& \lnot ([\![F]\!]e) \\ \ | ||
- | [\![\exists v. F]\!] &=& \exists S \subseteq N_0. [\![F]\!](e[v \mapsto S]) | + | [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0. [\![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 ===== | ||
**Set operations**. The ideas is that quantification over sets with $\subseteq$ gives us the full Boolean algebra of sets. | **Set operations**. The ideas is that quantification over sets with $\subseteq$ gives us the full Boolean algebra of sets. | ||
- | * Two sets are equal: $(S_1 = S_2) = (S_1 \subeteq S_2) \land (S_2 \subseteq S_1)$ | + | * Two sets are equal: $(S_1 = S_2) = (S_1 \subseteq S_2) \land (S_2 \subseteq S_1)$ |
* Strict subset: $(S_1 \subset S_2) = (S_1 \subseteq S_2) \land \lnot (S_2 \subseteq S_1)$ | * Strict subset: $(S_1 \subset S_2) = (S_1 \subseteq S_2) \land \lnot (S_2 \subseteq S_1)$ | ||
* Set is empty: $(S=\emptyset) = \forall S_1. S \subseteq S_1$ | * Set is empty: $(S=\emptyset) = \forall S_1. S \subseteq S_1$ | ||
Line 44: | Line 47: | ||
**Transitive closure of a relation.** If $F(x,y)$ is a formula on singletons, we define reflexive transitive closure as follows. Define shorthand | **Transitive closure of a relation.** If $F(x,y)$ is a formula on singletons, we define reflexive transitive closure as follows. Define shorthand | ||
\begin{equation*} | \begin{equation*} | ||
- | \mbox{Closed}(S,R) = (\forall x,y. One(x) \land One(y) \land x \in S \land F(x,y) \rightarrow y \in S) | + | \mbox{Closed}(S,F) = (\forall x,y. One(x) \land One(y) \land x \in S \land F(x,y) \rightarrow y \in S) |
\end{equation*} | \end{equation*} | ||
Then $(u,v) \in \{(x,y) \mid F(x,y)\}^*$ is defined by | Then $(u,v) \in \{(x,y) \mid F(x,y)\}^*$ is defined by | ||
\begin{equation*} | \begin{equation*} | ||
- | \forall S. u \in S \land \mbox{Closed}(S,R) \rightarrow v \in S | + | \forall S. u \in S \land \mbox{Closed}(S,F) \rightarrow v \in S |
\end{equation*} | \end{equation*} | ||