Differences

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

--- sav08:weak_monadic_logic_of_one_successor [2008/05/15 09:38]
vkuncak
+++ sav08:weak_monadic_logic_of_one_successor [2008/05/15 10:35]
vkuncak
@@ Line 27: / Line 27: @@
 The meaning of formulas is given by standard [[First-order logic semantics]].
-Note in particular that quantification is restricted to finite sets.
+Note in particular that quantification is restricted to finite sets (elements of $D$).
-===== 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.
+===== Expressive Power =====
+=== 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 \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)$
@@ Line 44: / Line 47: @@
   * If $k$ is a fixed constant, properties $\mbox{card}(A) \geq k$, $\mbox{card}(A)\leq k$, $\mbox{card}(A)=k$
-**Transitive closure of a relation.** If $F(x,y)$ is a formula on singletons, we define reflexive transitive closure as follows.  Define shorthand
+=== 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,F) = (\forall x,y. One(x) \land One(y) \land x \in S \land F(x,y) \rightarrow y \in S)
@@ Line 54: / Line 59: @@
 **Using transitive closure and successors:**
-  * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land s(y,x))$
+  * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land succ(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))$
+  * Addition by constant: $(x = y + c) = (\exists y_1,\ldots,y_{c-1}. succ(y,y_1) \land succ(y_1,y_2) \land \ldots \land succ(y_{c-1},x))$
-  * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|s(x,y))\}^*$
+  * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|succ(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\}^*)$
   * Congruence modulo $c$: $(x \equiv y)(\mbox{mod}\ c) = \mbox{Reach}_c(x,y) \lor \mbox{Reach}_c(y,x)$
-**Representing integers**.  Note that although we interpret elements as sets of integers, we cannot even talk about addition of two arbitrary integers $x=y+z$, only addition with a constant.  Also, although we can say $\mbox{Reach}_c(x,y)$ we cannot say in how many steps we reach $y$ from $x$.  However, if we view sets of integers digits of a binary representation of another integer, then we can express much more.  If $S$ is a finite set, let $N(S)$ represent the number whose digits are $S$, that is:
+=== Representing integers ===
+Note that although we interpret elements as sets of integers, we cannot even talk about addition of two arbitrary integers $x=y+z$, only addition with a constant.  Also, although we can say $\mbox{Reach}_c(x,y)$ we cannot say in how many steps we reach $y$ from $x$.  However, if we view sets of integers digits of a binary representation of another integer, then we can express much more.  If $S$ is a finite set, let $N(S)$ represent the number whose digits are $S$, that is:
 \begin{equation*}
   N(S) = \sum_{i \in S} 2^i
@@ Line 66: / Line 73: @@
 Then we can define addition $N(Z) = N(X) + N(Y)$ by saying that there exists a set of carry bits $C$ such that the rules for binary addition hold:
 \begin{equation*}
-  \exists C.\ 0 \notin i\ \land \forall i.\
+  \exists C.\ 0 \notin C\ \land \forall i.\
    \big(\begin{array}[t]{rcl}
     ((i \in Z) &\leftrightarrow& ((i \in X) \oplus (i \in Y) \oplus (i \in C))\ \land\\
@@ Line 79: / Line 86: @@
 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$.)
+=== Definable Relations ===
+We can define relations on $\mathbb{N}$ in two different ways.
+Relations on singleton sets:
+\[
+   r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \}
+\]
+Relations on binary representations:
+\[
+   r^b_F = \{(p,q) \mid F(N(p),N(q)) \}
+\]
+Addition is not definable as some $r^s_F$, but it is definable as $r^b_F$.