m

main.tex

@@ -15,7 +15,12 @@
 \newcommand{\msomi}{\textsf{MSO-MI}\xspace}
 \newcommand{\fomi}{\textsf{FO-MI}\xspace}
 \newcommand{\nmsomi}{\textsf{NMSO-MI}\xspace}
+
 \newcommand{\sst}{\textsf{SST}\xspace}
+\newcommand{\mtt}{\textsf{MTT}\xspace}
+
+\newcommand{\dlin}{\textsc{DLinSpace}}
+
 \newcommand{\ssign}{\mathfrak{S}}
 \newcommand{\tsign}{\mathfrak{T}}
 
@@ -79,6 +84,8 @@ Given a structure $A$ over $\ssign$, we define its image by $T$ by a structure $
 
 \fomi is defined by restricting formulas to be in \fo.
 
+A non-deterministic \msomi (\nmsomi) $S$ from $\ssign$-structures to $\tsign$-structures with $k$ parameters is given by an \msomi $T$ from $\ssign\uplus\set{X_1,\ldots,X_k}$-structures to $\tsign$-structures where $X_1,\ldots,X_k$ are additional unary symbols. Let $\pi$ denote the natural projection from $\ssign\uplus\set{X_1,\ldots,X_k}$-structures to $\ssign$-structures. We define $\sem S(A)=\set{\sem T(C)\mid\ \pi(C)=A}$.
+
 
 We call string-to-string (monadic) interpretations the particular case when the two signatures have unary symbols and one binary symbol which is a linear order (this can be enforced syntactically).
 
@@ -103,7 +110,7 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
     Let $T$ be an \msomi $T$ of dimension $d$ from structures over $\ssign$ to
      structures over $\tsign$ ,and let $\phi(x_1,\dots,x_k)$ be an \fo-formula over
     $\tsign$.
-    We can define an \mso-formula $\psi(\bar X_1,\ldots,\bar X_k)$  such that for any structure $A$ over $\ssign$, $A\models\psi(\bar S_1,\ldots,\bar S_k) \psi$ if and only if $\sem T(A)\models \phi(\bar S_1,\ldots,\bar S_k)$.\footnote{Note that $\bar S_i$ is a position of the structure $\sem T(A)$}
+    We can define an \mso-formula $\psi(\bar X_1,\ldots,\bar X_k)$  such that for any structure $A$ over $\ssign$, $A\models\psi(\bar S_1,\ldots,\bar S_k) $ if and only if $\sem T(A)\models \phi(\bar S_1,\ldots,\bar S_k)$.\footnote{Note that $\bar S_i$ is a position of the structure $\sem T(A)$}
 \end{theorem}
 
 \begin{proof}
@@ -119,13 +126,6 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
     regular domains. 
 \end{corollary}
 
-\subsection{\nmsomi relations}
-
-Just as \msot can be extended with parameters to add some form of
-non-determinism, \msomi can also be extended with parameters to define
-\expreg relations, and the backward translation theorem still
-holds. We denote by $\textsf{ExpR}$ the class of \expreg
-relations. 
 
 
 \section{Expressiveness of \expreg\ functions}
@@ -133,7 +133,7 @@ relations.
 \subsection{Closure properties}
 
 \begin{theorem}
-    FOI $\circ$ MSOMI = MSOMI
+    $\foi\ \circ \msomi\ = \msomi$
 \end{theorem}
 
 \begin{proof}
@@ -259,40 +259,42 @@ Origin = head position
 
 
 \begin{itemize}
-    \item does $MSOT\circ MSOMI \subseteq MSOMI$ holds ? Using Khrone
-      Rhodes theorem of Mikolaj, it seems that the only difficult case
-      is to post-compose a reversible Mealy machine with an
-      MSOMI. Candidate composition which does not seem to be easy to
-      show its membership to MSOMI:
+    \item does $\msot\circ \msomi \subseteq \msomi$ holds ? Using Khrone
+      Rhodes theorem of Miko\l aj, it seems that the only difficult case
+      is to post-compose an \msomi with a reversible Mealy machine. Candidate composition which does not seem to be easy to
+      show its membership to \msomi:
       $$
       even-filter \circ (1-filter \circ subsets)
       $$
       where $1-filter$ only keeps the positions marked $1$ in
       the results of the function $subsets$ and $even-filter$ only
       keeps the even positions. It is easy to see that $(1-filter
-      \circ subsets)$ is MSOMI.
-    \item Is \textsf{ExpF} the smallest subset including the function
-      $subsets$ and the polyregular functions and closed under
-      composition ?
+      \circ subsets)$ is \msomi.
 \end{itemize}
 
+\section{The case of the successor}
+
+\begin{theorem}
+\msomi with successor is equivalent to \dlin
+\end{theorem}
+
+\begin{proof}
+Given an \msomi, we can define a rational letter-to-letter relation which realizes the successor and from this obtain a linear bounded automaton.
+From a linear bounded automaton, the next configuration relation can be defined in \mso.
+\end{proof}
+
+Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\epsilon)$ compute \dlin ?
+
 \subsection{Computational models}
 
 \begin{itemize}
+    \item what about \mtt ? They have doubly-exponential growth, but do
+      they capture \msomi  ?
     \item recursive programming language corresponding or being
-      captured by MSOMI ?
-    \item pebble transducer model ? candidate: transducer with
-      unboundedly many invisible pebbles. 
-    \item what about MTT ? They have doubly-exponential growth, but do
-      they capture MSOMI  ?
-
-      \item MSOMI(succ) ? They have non-regular domains. Do they
-        correspond to LINSPACE ?
-
-      \item ``input rewriting sweeping transducers'': like sweeping
-        transducers but they can rewrite their input (in a
-        letter-to-letter mode) and stops whenever the input belongs to
-        some regular language. They should correspond to MSOMI(succ). 
+      captured by \msomi ?
+    \item pebble transducer model. candidate:
+    layered marble transducers. A finite number of layers. a marble of layer k cannot go through another marble of layer k. However it can go through marbles of layers $<k$.
+	\item Krohn-Rhodes like decomposition eg $\mathsf{polyreg}\circ \mathsf{exp} \circ \mathsf{reg}$, with $\mathsf{exp}$ being some simple class of exponential growth function.
 \end{itemize}