Differences

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

--- msol_over_strings [2007/05/10 18:15]
vkuncak
+++ msol_over_strings [2008/05/15 09:26] (current)
vkuncak
@@ Line 1: / Line 1: @@
 ====== MSOL over Strings ======
 ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings =====
@@ Line 26: / Line 24: @@
   [\![F_1 \lor F_2]\!]e &=& [\![F_1]\!]e\ \lor\ [\![F_2]\!]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*}
@@ Line 40: / Line 38: @@
   * 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)$
-  * 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)
   * If $k$ is a fixed constant, properties $\mbox{card}(A) \geq k$, $\mbox{card}(A)\leq k$, $\mbox{card}(A)=k$
@@ Line 46: / Line 44: @@
 **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*}
-  \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*}
 Then $(u,v) \in \{(x,y) \mid F(x,y)\}^*$ is defined by
 \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*}
 **Using transitive closure and successors:**
   * 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))\}^*$
-  * 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\}^*)$
   * Congruence modulo $c$: $(x \equiv y)(\mbox{mod}\ c) = \mbox{Reach}_c(x,y) \lor \mbox{Reach}_c(y,x)$
@@ Line 68: / Line 66: @@
   \exists C.\ 0 \notin i\ \land \forall i.\
    \big(\begin{array}[t]{rcl}
-    ((i \in Z) &\leftrightarrow& ((i \in X \oplus i \in Y) \oplus i \in C))\ \land\\
+    ((i \in Z) &\leftrightarrow& ((i \in X) \oplus (i \in Y) \oplus (i \in C))\ \land\\
-    ((i+1 \in C) &\leftrightarrow& \mbox{twoOrMore}(i \in X,i \in Y,i \in C)\big)
+    ((i+1 \in C) &\leftrightarrow& \mbox{atLeastTwo}(i \in X,i \in Y,i \in C)\big)
    \end{array}
 \end{equation*}
@@ Line 75: / Line 73: @@
 \begin{eqnarray*}
   x \oplus y &=& (x \lor y) \land \lnot (x \land y) \\
-  \mbox{twoOrMore}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z)
+  \mbox{atLeastTwo}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z)
 \end{eqnarray*}
-This way we can represent entire Presburger arithmetic in MSOL over strings.  Moreover, we have more expressive power because $X \subseteq Y$ means that the one bits of $N(X)$ are included in the bits of $N(Y)$, that is, the bitwise or of $N(X)$ and $N(Y)$ is equal to $N(Y)$.  In fact, if we add the relation of bit inclusion into Presburger arithmetic, we obtain precisely the expressive power of MSOL when sets are treated as binary representations of integers (Indeed, taking the minimal syntax of MSOL from the beginning, the bit inclusion gives us the subset, whereas the successor relation $s(x,y)$ is expressible using $y=x+x$.)
+This way we can represent entire Presburger arithmetic in MSOL over strings.  Moreover, we have more expressive power because $X \subseteq Y$ means that the one bits of $N(X)$ are included in the bits of $N(Y)$, that is, the bitwise or of $N(X)$ and $N(Y)$ is equal to $N(Y)$.  In fact, if we add the relation of bit inclusion into Presburger arithmetic, we obtain precisely the expressive power of MSOL when sets are treated as binary representations of integers (Indeed, taking the minimal syntax of MSOL from the beginning, the bit inclusion gives us the subset, whereas the successor relation $s(x,y)$ is expressible using $y=x+1$.)