Differences

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

--- msol_over_strings [2007/05/06 19:04]
vkuncak
+++ msol_over_strings [2008/05/14 19:21]
vkuncak
@@ Line 22: / Line 22: @@
   [\![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*}
@@ Line 30: / Line 30: @@
 **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)$
   * Set is empty: $(S=\emptyset) = \forall S_1. S \subseteq S_1$
@@ Line 38: / 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 44: / 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*}
+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 84: @@
 \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$.)