Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
msol_over_strings [2007/05/27 12:52] vaibhav.rajan |
msol_over_strings [2007/05/27 13:34] vaibhav.rajan |
||
---|---|---|---|
Line 29: | Line 29: | ||
[\![\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*} | ||
+ | |||
+ | |||
Line 56: | Line 58: | ||
\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))$ | ||
* 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}. 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))\}^*$ | * 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)$ | * Congruence modulo $c$: $(x \equiv y)(\mbox{mod}\ c) = \mbox{Reach}_c(x,y) \lor \mbox{Reach}_c(y,x)$ | ||