LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
msol_over_strings [2008/05/14 19:21]
vkuncak
msol_over_strings [2008/05/15 09:26]
vkuncak
Line 51: Line 51:
 \end{equation*} \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:​** **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 s(y,x))$
Line 74: Line 66:
   \exists C.\ 0 \notin i\ \land \forall i.\    \exists C.\ 0 \notin i\ \land \forall i.\ 
    ​\big(\begin{array}[t]{rcl}    ​\big(\begin{array}[t]{rcl}
-    ((i \in Z) &​\leftrightarrow&​ ((i \in X \oplus i \in Y) \oplus i \in C))\ \land\\ +    ((i \in Z) &​\leftrightarrow&​ ((i \in X\oplus ​(i \in Y) \oplus ​(i \in C))\ \land\\ 
-    ((i+1 \in C) &​\leftrightarrow&​ \mbox{twoOrMore}(i \in X,i \in Y,i \in C)\big)+    ((i+1 \in C) &​\leftrightarrow&​ \mbox{atLeastTwo}(i \in X,i \in Y,i \in C)\big)
    ​\end{array}    ​\end{array}
 \end{equation*} \end{equation*}
Line 81: Line 73:
 \begin{eqnarray*} \begin{eqnarray*}
   x \oplus y &=& (x \lor y) \land \lnot (x \land y) \\   x \oplus y &=& (x \lor y) \land \lnot (x \land y) \\
-  \mbox{twoOrMore}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z)+  \mbox{atLeastTwo}(x,y,z) &=& (x \land y) \lor (x \land z) \lor (y \land z)
 \end{eqnarray*} \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+1$.) 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$.)