Differences

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

--- msol_over_strings [2007/05/06 19:03]
vkuncak created
+++ msol_over_strings [2007/05/27 13:27]
vaibhav.rajan
@@ Line 1: / Line 1: @@
+====== MSOL 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 =====
 **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 44: @@
   * 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 50: @@
 **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\})$