diff --git a/main.tex b/main.tex index f1e600098b11f755ca3d53281ef2bea24de1255e..75ca06dd20e6839fbb14dd3811d5099a77e877a4 100644 --- a/main.tex +++ b/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}