\subsection{Relational structures and logical interpretations}
\subsubsection{Relational structures}
\paragraph{The orderned model of words}
\paragraph{The powerset model of words}~\\
Any \mso-formula can be seen as an \fo-formula over the powerset model
\subsubsection{Logical interpretation}
Here define \msoi and \foi.
\subsection{Monadic interpretation}
\footnote{We
could add copy to MSOMI just as in Courcelle to avoid undesirable
could add copy to \msomi just as in Courcelle to 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:
...
...
@@ -106,8 +122,14 @@ $$
It is easy to see that $subsets\in\textsf{ExpF}$.
\section{Expressiveness of \expreg\ functions}
\subsection{Backward translation theorem}
\begin{theorem}[Backward translation theorem]
Let $T$ be an \msomi$T$of dimension $d$ from structures over $\ssign$ to
Let $T$ be an \msomi 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)$ 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)$}
...
...
@@ -126,10 +148,20 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
regular domains.
\end{corollary}
\begin{remark}
\label{rem:power}
An \msomi can also be seen as an \foi over the powerset model.
\end{remark}
\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?
\end{question}
\section{Expressiveness of \expreg\ functions}
\begin{question}
Given a (fixed) \msomi realizing $f$, can one compute the image of a word $u$ in time $O(|u|+|f(u)|)$ ?
\end{question}
\subsection{Closure properties}
\begin{theorem}
...
...
@@ -137,122 +169,57 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
\end{theorem}
\begin{proof}
Use standard ideas for composition logical transductions: formula
substitutions. The first-order parameters of the FOI becomes
From the backward translation theorem.
Use standard ideas for composition of logical transductions: formula
substitutions. The first-order parameters of the \foi become
monadic parameters.
\end{proof}
\begin{theorem}
NSST$_{copy}$$\subseteq$\textsf{ExpR}.
\end{theorem}
\begin{proof}
See IPAD notes.
Alternatively this comes from Remark~\ref{rem:power}, and the fact that \foi are closed under composition.
\end{proof}
\subsection{Lexicographic MSOMI and SST}
An MSOMI $T$ is lexicographic if
$\phi_{\leq}(\overline{X},\overline{Y})$ is of the following form, for
\subsection{\Expreg functions of polynomial growth}
\begin{theorem}
$\textsf{ExpF}\cap O(n^d)=\textsf{PolyF}$
An \msomi of growth $O(n^d)$ can be realized by an \msoi of dimension $d$.
\end{theorem}
\begin{proof}
See mail Nathan sent to Mikolaj on Saturday 2 April
2022. Moreover, an MSOMI of $O(n^d)$ growth can be converted into
an MSOI of dimension $d$ (with $d$ first-order parameters).
\end{proof}
Moreover, it is decidable whether an
\subsection{Layered marble transducer}
We define a model of transducers based on marble transducers.
\section{FO model-checking of transductions with origins: SSTs and pebble transducers}
\label{sec:mc}
\subsection{Model-checking (copyfull) SSTs with origin}
\begin{itemize}
\item Origin := input position where the output position was created in a
register update.
\item FO[o] := FO[$\leq_in,\leq_out,o(x,y)$], i.e. FO over origin graphs
\end{itemize}
\section{The case of the successor}
\begin{theorem}
Model-checking non-deterministic SST with copy against FO[o] is decidable.
\end{theorem}
\begin{proof}
Use the backward translation theorem.
\end{proof}
\begin{theorem}
Model-checking $O(n^2)$ deterministic SST with copy against MSO[o] is undecidable.
\msomi with successor is equivalent to \dlin
\end{theorem}
\begin{proof}
See IPAD notes.
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}
\begin{question}
\subsection{Model-checking pebble transducers with origin}
Origin = head position
Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ\cdots\circ f_{a_n}(\epsilon)$ compute \dlin ?
\begin{theorem}
Model-checking non-deterministic 2-pebble transducers against FO[o] is undecidable.
\end{theorem}
\begin{proof}
See IPAD notes.
\end{proof}
\end{question}
\section{Nested marble transducer}
We define a model of transducers based on marble transducers.
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$.
TODO: find a better name than "marble"
\begin{theorem}
Model-checking deterministic pebble transducers against FO[o] is decidable.
Any transduction defined by a nested marble transducer can be expressed as an \msomi.
\end{theorem}
\begin{proof}
Use DPT = MSOI and the backward translation theorem.
\end{proof}
\section{Some remaining questions}
...
...
@@ -260,32 +227,12 @@ Origin = head position
\subsection{Expressiveness}
\begin{itemize}
\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.
\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}
...
...
@@ -294,12 +241,12 @@ Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\e
they capture \msomi ?
\item recursive programming language corresponding or being
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.
\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.
