Differences

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

--- msol_over_strings [2007/05/27 12:52]
vaibhav.rajan
+++ msol_over_strings [2007/05/27 13:44]
vaibhav.rajan
@@ Line 29: / Line 29: @@
   [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0 \land [\![F]\!](e[v \mapsto S])
 \end{eqnarray*}
@@ Line 56: / Line 59: @@
 \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_{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 81: / 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$.)