could add copy to \msomi just as in Courcelle to avoid undesirable
could add copy to \msomi just as in Courcelle \msotto avoid undesirable
cornercase behaviours with small words.}
Given two relational signatures $\ssign,\tsign$, an \mso monadic interpretation $T$ of dimension $d$ from structures over $\ssign$ to structures over $\tsign$ is given by:
...
...
@@ -96,7 +96,7 @@ Given two relational signatures $\ssign,\tsign$, an \mso monadic interpretation
\end{itemize}
where $\bar X$ denotes a $d$-tuple of monadic variables.
Given a structure $A$ over $\ssign$, we define its image by $T$ by a structure $B=\sem T(B)$ over $\tsign$: the universe of $B$ is the set $U=\set{\bar S\mid\ A \models\phi_U(\bar S)}$, given $R\in\tsign$ of arity $k$, we define $R$ in $B$ as the set $\set{\tuple{\bar S_1,\ldots,\bar S_k}\in U^k\mid\ \phi_R(\bar S_1,\ldots,\bar S_k)}$.
Given a structure $A$ over $\ssign$, we define its image by $T$ by a structure $B=\sem T(A)$ over $\tsign$: the universe of $B$ is the set $U=\set{\bar S\mid\ A \models\phi_U(\bar S)}$, given $R\in\tsign$ of arity $k$, we define $R$ in $B$ as the set $\set{\tuple{\bar S_1,\ldots,\bar S_k}\in U^k\mid\ \phi_R(\bar S_1,\ldots,\bar S_k)}$.
%Given tuples $\bar X_1,\ldots,\bar X_l$, we extend $\sem T$ by $\sem T(A,\bar X_1,\ldots,\bar X_l)=B,\set{\bar X_1},\ldots,\set{\bar X_l}$.
\fomi is defined by restricting formulas to be in \fo.
...
...
@@ -109,7 +109,7 @@ We call string-to-string (monadic) interpretations the particular case when the
An \expreg function is a string-to-string monadic interpretation.
We denote by \textsf{ExpF} the class of \expreg functions.
As an example, consider the following function. Let $\Sigma=\{a,b\}$
and $\Gamma=\Sigma\times\{0,1\}\cup\#$. Let $u\in\Sigma^*$.
and $\Gamma=\Sigma{\times}\{0,1\}\cup\set{\#}$. Let $u\in\Sigma^*$.
Given a
subset $U\subseteq Pos(u)$, we let $u_U\in\Gamma^*$ such that
$|u_U| = |u|$ and for all positions $p$, $u_U(p)=(u(p), p\in
...
...
@@ -156,7 +156,7 @@ An \msomi can also be seen as an \foi over the powerset model.
\begin{question}
Does $\msot\circ\msomi\subseteq\msomi$ hold? Using Krohn-Rhodes theorem of Miko\l aj, it seems that the only difficult case
is to post-compose an \msomi with a reversible Mealy machine. That is the problem can be rephrased as: does $\rev\circ\msomi\subseteq\msomi$ hold?
is to post-compose an \msomi with a reversible Mealy machine. In other words the problem can be formulated as: does $\rev\circ\msomi\subseteq\msomi$ hold?
Let $A=\set{a,b}$. Let us define an \expreg function $f:\left(A\cup\set{\sharp}\right)^*\rightarrow(A\times\set{0,1}\cup\set{\natural})^*$.
What the function $f$ does is list all subsets of positions (without $\sharp$) and output the corresponding subword. The subword are output in a specific order, and separated by $\natural$. Let us decribe the order in which these subsets of positions are listed.
What the function $f$ does is list all subsets of positions (without $\sharp$) and output the word labelled with the corresponding subset. The labelled words are output in a specific order, and separated by $\natural$. Let us decribe the order in which these subsets of positions are listed.
Over a word $u$ without $\sharp$, $f$ outputs the list of all subwords (with multiplicities), in the lexicographic order over the subset of positions of $u$, \eg$f(aab)=\natural b\natural a\natural ab\natural a\natural ab\natural aa\natural aab$; each subword corresponding the the subsets $000,001$, $010$, $011$, $100$, $101$, $110,111$, in respective order.
Basically, the most significant figure inside a block between two $\sharp$ symbols is to the left. However, the most significant blocks are to the right, \eg: $f(a\sharp b)=\natural a \natural b\natural ab$.
Over a word $u$ without $\sharp$, $f$ outputs the list of all annotations, in the lexicographic order over the subset of positions of $u$, \eg
Basically, the most significant figure inside a block between two $\sharp$ symbols is to the left. However, the most significant blocks are to the right, \eg: $f(aa\sharp b)=a0a0b0\natural a0a1b0\natural a1a0b0\natural a1a1b0\natural a0a0b1\natural a0a1b1\natural a1a0b1\natural a1a1b1$.
