Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:weak_monadic_logic_of_one_successor [2008/05/15 09:50] vkuncak |
sav08:weak_monadic_logic_of_one_successor [2008/05/15 10:02] vkuncak |
||
---|---|---|---|
Line 28: | Line 28: | ||
Note in particular that quantification is restricted to finite sets (elements of $D$). | Note in particular that quantification is restricted to finite sets (elements of $D$). | ||
+ | |||
===== Expressive Power ===== | ===== Expressive Power ===== | ||
Line 57: | Line 58: | ||
**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 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\}^*)$ | * 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)$ |