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/10 18:15] vkuncak |
msol_over_strings [2007/05/27 12:52] vaibhav.rajan |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== MSOL over Strings ====== | ====== MSOL over Strings ====== | ||
| + | |||
| Line 26: | Line 27: | ||
| [\![F_1 \lor F_2]\!]e &=& [\![F_1]\!]e\ \lor\ [\![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]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0. [\![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 40: | Line 43: | ||
| * Intersection: $(A = B \cap C) = (A \subseteq B \land A \subseteq C) \land (\forall A_1. A_1 \subseteq B \land A_1 \subseteq C \rightarrow A_1 \subseteq A)$ | * Intersection: $(A = B \cap C) = (A \subseteq B \land A \subseteq C) \land (\forall A_1. A_1 \subseteq B \land A_1 \subseteq C \rightarrow A_1 \subseteq A)$ | ||
| * Union: $(A = B \cup C) = (B \subseteq A \land C \subseteq A) \land (\forall A_1. B \subseteq A_1 \land C \subseteq A_1 \rightarrow A \subseteq A_1)$ | * Union: $(A = B \cup C) = (B \subseteq A \land C \subseteq A) \land (\forall A_1. B \subseteq A_1 \land C \subseteq A_1 \rightarrow A \subseteq A_1)$ | ||
| - | * Set difference: $(A = B \setminus C) = (A \cup C = B \land A \cap C = \emptyset)$ | + | * Set difference: $(A = B \setminus C) = (A \cup (B \cap C) = B \land A \cap C = \emptyset)$ |
| (or just use element-wise definitions with singletons) | (or just use element-wise definitions with singletons) | ||
| * If $k$ is a fixed constant, properties $\mbox{card}(A) \geq k$, $\mbox{card}(A)\leq k$, $\mbox{card}(A)=k$ | * If $k$ is a fixed constant, properties $\mbox{card}(A) \geq k$, $\mbox{card}(A)\leq k$, $\mbox{card}(A)=k$ | ||
| Line 46: | Line 49: | ||
| **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*} | ||
| **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))$ | ||
| - | * Addition by constant: $(x = y + c) = (\exists y_1,\ldots,y_{c-1}. s(y,y_1) \land s(y_1,y_2) \land \ldots \land s(y_{k-1},x))$ | + | * Addition by constant: $(x = y + c) = (\exists y_1,\ldots,y_{c-1}. s(y,y_1) \land s(y_1,y_2) \land \ldots \land s(y_{c-1},x))$ |
| * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|s(x,y))\}^*$ | * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|s(x,y))\}^*$ | ||
| * Reachability in $k$-increments, that is, $\exists k \geq 0. y=x + c\cdot k$: $\mbox{Reach}_c(u,v) = ((u,v) \in \{(x,y)\mid y=x+c\})$ | * Reachability in $k$-increments, that is, $\exists k \geq 0. y=x + c\cdot k$: $\mbox{Reach}_c(u,v) = ((u,v) \in \{(x,y)\mid y=x+c\})$ | ||