Differences

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

--- msol_over_strings [2007/05/08 20:32]
vaibhav.rajan
+++ msol_over_strings [2007/05/27 13:44]
vaibhav.rajan
@@ Line 1: / Line 1: @@
 ====== MSOL over Strings ======
 ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings =====
@@ Line 22: / Line 25: @@
   [\![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\}) \\ \
-  [\![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) \\ \
-  [\![\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 \land [\![F]\!](e[v \mapsto S])
 \end{eqnarray*}
 ===== What can we express in MSOL over strings =====
@@ Line 38: / Line 46: @@
   * 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 44: / Line 52: @@
 **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*}
+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:**
   * 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 76: / Line 92: @@
 \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$.)