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 [2007/05/27 13:44]
vaibhav.rajan 		msol_over_strings [2008/05/15 09:26]
vkuncak
Line 1: Line 1:
 ====== MSOL over Strings ====== ====== MSOL over Strings ======
- 
- 
- 
  
 ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings ===== ===== Syntax and Semantics of Weak Monadic Second-Order Logic over Strings =====
Line 29: Line 26:
   [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0 \land [\![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*} \end{eqnarray*}
- 
- 
- 
- 
- 
  
 ===== What can we express in MSOL over strings ===== ===== What can we express in MSOL over strings =====
Line 59: 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 82: 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 89: 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$.)