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 Both sides next revision
msol_over_strings [2007/05/10 18:15]
vkuncak 		msol_over_strings [2007/05/10 18:15]
vkuncak
Line 28: Line 28:
   [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0. [\![F]\!](e[v \mapsto S])   [\![\exists v. F]\!]e &=& \exists S. S\ \mbox{is finite}\ \land\ S \subseteq N_0. [\![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 46: Line 47:
 **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*} \begin{equation*}
-  \mbox{Closed}(S,​R) = (\forall x,y. One(x) \land One(y) \land x \in S \land F(x,y) \rightarrow y \in S)+  \mbox{Closed}(S,​F) = (\forall x,y. One(x) \land One(y) \land x \in S \land F(x,y) \rightarrow y \in S)
 \end{equation*} \end{equation*}
 Then $(u,v) \in \{(x,y) \mid F(x,y)\}^*$ is defined by Then $(u,v) \in \{(x,y) \mid F(x,y)\}^*$ is defined by
 \begin{equation*} \begin{equation*}
-  \forall S. u \in S \land \mbox{Closed}(S,​R) \rightarrow v \in S+  \forall S. u \in S \land \mbox{Closed}(S,​F) \rightarrow v \in S
 \end{equation*} \end{equation*}