
\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{article}

\usepackage{amssymb,amsthm,amsmath,stmaryrd}
\usepackage{xspace}

\newcommand{\expreg}{exp-regular\xspace}
\newcommand{\Expreg}{Exp-regular\xspace}



\newcommand{\mso}{\textsf{MSO}\xspace}
\newcommand{\fo}{\textsf{FO}\xspace}
\newcommand{\msot}{\textsf{MSO-T}\xspace}
\newcommand{\fot}{\textsf{FO-T}\xspace}
\newcommand{\msoi}{\textsf{MSO-I}\xspace}
\newcommand{\foi}{\textsf{FO-I}\xspace}
\newcommand{\msomi}{\textsf{MSO-MI}\xspace}
\newcommand{\fomi}{\textsf{FO-MI}\xspace}
\newcommand{\nmsomi}{\textsf{NMSO-MI}\xspace}
\newcommand{\pow}[1]{\mathsf{2}^{#1}}
\newcommand{\ar}{\mathsf{ar}}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\lefto}{\mathsf{left}}
\newcommand{\righto}{\mathsf{right}}
\newcommand{\inter}{\mathsf{I}}
\newcommand{\sumorder}{\sqsubseteq}

\newcommand{\sst}{\textsf{SST}\xspace}
\newcommand{\mt}{\textsf{MT}\xspace}
\newcommand{\ipt}{\textsf{IPT}\xspace}
\newcommand{\mtt}{\textsf{MTT}\xspace}

\newcommand{\rev}{\textsf{rev}\xspace}
\newcommand{\rtm}{\textsf{RTM}\xspace}
\newcommand{\drtm}{\textsf{DRTM}\xspace}
\newcommand{\reg}{\textsf{Reg}}
\newcommand{\homo}{\textsf{Hom}\xspace}



\newcommand{\dlinspace}{\textsc{DLinSpace}\xspace}
\newcommand{\dlogspace}{\textsc{DLogSpace}\xspace}
\newcommand{\dptime}{\textsc{DPTime}\xspace}
\newcommand{\dexptime}{\textsc{DExpTime}\xspace}

\newcommand{\ssign}{\mathfrak{S}}
\newcommand{\tsign}{\mathfrak{T}}

\newcommand{\set}[1]{\left\{#1\right\}}
\newcommand{\tuple}[1]{\left(#1\right)}
\newcommand{\sem}[1]{\left\llbracket #1\right\rrbracket}

\newcommand{\nat}{\mathbb{N}}

\newcommand{\eg}{\textit{e.g.~}}
\newcommand{\ie}{\textit{i.e.~}}

\newcommand{\mleft}{\mathsf{left}}
\newcommand{\mright}{\mathsf{right}}
\newcommand{\push}{\mathsf{push}}
\newcommand{\pop}{\mathsf{pop}}
\newcommand{\auta}{\mathcal A}
\newcommand{\autb}{\mathcal B}
\newcommand{\astb}{{\star}}

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{conjecture}{Conjecture}

\theoremstyle{definition}
\newtheorem{remark}{Remark}
\newtheorem{question}{Question}
\newtheorem{example}{Example}


\bibliographystyle{alpha}% the mandatory bibstyle

\title{\textsc{Exponential growth\\ word-to-word transductions}} %TODO Please add
\author{}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\maketitle



\begin{abstract}

\end{abstract}


\section*{Introduction}
\label{sec:intro}

\section{Words, transducers and logic}
\label{sec:prelim}
\subsection{Words, languages and transductions}
\subsection{Relational structures and logical interpretations}

\subsubsection{Relational structures}
\paragraph{Signature}
A \emph{signature} $\ssign$ is a set $S$ of \emph{symbols}\footnote{We only consider relational signatures.}, together with an \emph{arity function}, which we denote by $\ar:S\rightarrow \nat$. Abusing notations, we will often write $R\in \ssign$ instead of $R\in S$.

\paragraph{Structures} A \emph{structure} (sometimes \emph{model}) $A$ over a signature $\ssign$ is given as a \emph{domain} $\dom_A$ together with an \emph{interpretation function} which maps any symbol $R$ of $\ssign$ to a set denoted $\inter_A(R)$ such that $\inter_A(R)\subseteq \dom_A^r$, with $r=\ar(R)$.

\paragraph{Operations}
Any structure over a signature can be seen as a structure over a larger signature where additional symbols are interpreted as empty sets.

The \emph{disjoint union} (or coproduct) of two structures $A,B$ over the signature $\ssign$ is a structure $A+B$ over signature $\ssign+\set{\lefto,\righto}$ where $\lefto, \righto$ are unary symbols. The domain of $A+B$ is $\dom_A+\dom_B=(\dom_A{\times}\set{1}) \cup (\dom_B{\times}\set{2}) $. The interpretation of a symbol $R$ is $\inter_A(R)+\inter_B(R)$. The interpretation of $\lefto$ is $\dom_A\times\set{1}$ and the interpretation of $\righto$ is $\dom_B\times\set{2}$.

The \emph{product} of two structures $A,B$ over a signature $\ssign$ is a structure $A\times B$ over signature $\ssign\times\set{\lefto,\righto}$ where $(R,\lefto)$ and $(R, \righto)$ have the same arity as $R$. The domain of $A\times B$ is $\dom_A\times\dom_B$. The interpretation of a symbol $(R,\lefto)$ is $\inter_A(R)\times \dom_B$ and the interpretation of $(R,\righto)$ is $\dom_A\times \inter_B(R)$.

The \emph{ordered coproduct} of a sequence of structures $A_1,\cdots, A_n$ over the same signature $\ssign$ is a structure $\bigoplus_{i\leq n} A_i$ over the signature $\ssign+\set{\sqsubseteq}$, where $\sqsubseteq$ has arity $2$. The domain of $\bigoplus_{i\leq n} A_i$ is $\bigoplus_{i\leq n} \dom_{A_i}=\bigcup_{i\leq n} \dom_{A_i}{\times}\set{i}$. The interpretation of a symbol $R$ is $\bigoplus_{i\leq n} \inter_{A_i}(R)$. The interpretation of $\sumorder$ is $\bigcup_{i\leq j\leq n}(\dom_{A_i}{\times}\set{i})\times(\dom_{A_j}{\times}\set{j})$.

The \emph{ordered product} of a sequence of structures $A_1,\cdots, A_n$ over the same signature $\ssign$ is a structure $\bigotimes_{i\leq n} A_i$ over the signature $\ssign + \set{\sim}$, where $\sim$ has arity $2$ and holds for tuples that are equal over all coordinates except one. The domain of $\bigotimes_{i\leq n} A_i$ is $\bigotimes_{i\leq n} \dom_{A_i}$.
The interpretation of a symbol $R$ of arity $k$ is $\set{(\bar a_1,\dots,\bar a_k)\mid\ \forall i\leq n,\ (\bar a_1[i],\dots,\bar a_k[i])\in  \inter_{A_i}(R)}$. The interpretation of $\sim$ is $ \set{(\bar a,\bar b)\mid \exists ! i\leq n,\ \bar a[i] \neq \bar b[i]}$


The \emph{powerset structure} of a structure $A$ over signature $\ssign$ is a structure $\pow A$ over signature $\ssign\uplus \set{\subseteq}$, where $\subseteq$ is a binary symbol. The domain of $\pow A$ is $\pow{\dom_A}$. The interpretation of a symbol $R$ is the set $\set{(\set{x_1},\dots,\set{x_k})\mid\ (x_1,\ldots,x_n)\in \inter_A(R)}$.
The interpretation of $\subseteq$ is the actual set inclusion $\set{(x,y)\mid\ x\subseteq y\subseteq \dom_A}$.
\paragraph{Word models}
The \emph{ordered model} of a word $w$ over alphabet $\Sigma$ is the usual model with one unary predicate $a$ per letter $a\in \Sigma$, interpreted as the set of positions with letter $a$. Additionally the binary symbol $\leq$ is interpreted as the linear order over the positions of the word.

The \emph{powerset model} of a word is the powerset structure of the structure associated with a word.
Any \mso-formula can be seen as an \fo-formula over the powerset model.
We sometimes say \emph{word} to mean its \emph{ordered model} (or even \emph{powerset model}), relying on context to avoid confusion.

\subsubsection{Logical interpretation}
Here define \msoi and \foi.
\subsection{Monadic interpretation}

\footnote{We
could add copy to \msomi just as in Courcelle \msot 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:
\begin{itemize}
\item An \mso-formula $\phi_{\dom}(\bar X)$ defining the domain of the output structure
\item For each relation $R\in \tsign$ of arity $k$, a formula $\phi_R(\bar X _1,\ldots, \bar X_k )$

\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(A)$ over $\tsign$: the domain of $B$ is the set $D=\set{\bar S\mid\ A \models \phi_\dom(\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 \dom_A^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}$.


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 word-to-word (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).

An \expreg function is a word-to-word monadic interpretation.



\section{Expressiveness of \expreg\ functions}

\subsection{Backward translation theorem}

\begin{theorem}[Backward translation theorem]
    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$ denotes either a tuple of sets of positions of $A$, or a position of $\sem T(A)$}
\end{theorem}

\begin{proof}
    Idea: any first-order quantification $\exists x$ in $\phi$ is
    replaced by the monadic quantification $\exists \bar{X}$,
    the atoms $R(x_1,\dots,x_k)$ are replaced by
    $\phi_R(\bar X_1,\ldots,\bar X_k)$, etc. 
\end{proof}

\begin{corollary}
    The inverse image of any \fo-definable language by an \expreg
    function is regular. In particular, \expreg functions have
    regular domains. 
\end{corollary}

\begin{remark}
\label{rem:power}
An \msomi can also be seen as an \foi over the powerset model.
\end{remark}


\subsection{Closure properties}

\subsubsection{Postcomposition by \foi}
\begin{theorem}
    $\foi\ \circ \msomi\ = \msomi$
\end{theorem}

\begin{proof}
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. 
    
    Alternatively this comes from Remark~\ref{rem:power}, and the fact that \foi are closed under composition.
\end{proof}


\subsubsection{Precomposition by \msot}
\begin{theorem}
    $\msomi\ \circ \msot\ = \msomi$
\end{theorem}

\begin{proof}
    From the usual proof of closure under composition of \msot.
\end{proof}



\subsection{Growth}

\subsubsection{Exponential growth}

\begin{remark}
An \msomi of dimension $d$ has growth $\leq (2^n)^d=2^{dn}=2^{O(n)}$.

\end{remark}
\begin{corollary}
\begin{itemize}~

\item \Expreg functions are \emph{not} closed under composition.

\item \Expreg functions are \emph{not} closed under pre-composition by functions of superlinear growth, in particular polyregular functions.

\end{itemize}
\end{corollary}
\begin{theorem}
    An \msomi of growth $O(n^d)$ can be realized by an \msoi of dimension $d$.
\end{theorem}








\section{Nested marble transducer}

We define a model of transducers based on marble transducers.
 A finite nesting height. a marble of height k cannot go through another marble of height k. However it can go through marbles of height $<k$.
    
    
A marble automaton is a restriction of an invisble-pebble automaton, with two kinds of allowed transitions: $\push$ followed by $\mright$ or $\pop$.



A marble automaton $\auta$ is given by:
\begin{itemize}
\item a finite set of letters $A$, and two extra letters $\set{\vdash,\dashv}$
\item a finite set of states $Q$
\item a transition function $\delta: A_{\vdash,\dashv}{\times} Q \rightarrow {\set{\push}}{\times}Q^2 +\set{\pop}{\times}(Q{\rightarrow}Q)$


\end{itemize}

Let us explain how the automaton is run over a word $u\in A^*$. The automaton actually runs over the word $v={\vdash} u {\dashv}$.
A \emph{configuration} $c$ over the word $v$ of length $n$ is a word over $Q\times\set{1,\ldots,n}$. The configuration is actually a stack of reading heads over the input word. The head of the stack is the \emph{active head}.
The \emph{initial configuration} of $\auta$ over $v$ is the word $(q_0,1)$. Given a non-empty configuration $c(p,i)$ the \emph{successor configuration} $c'$ is defined according to $\delta(v[i],p)=\alpha$ in the following way:
\begin{itemize}
\item if $\alpha=(\push,q_1,q_2)$ and $i<n$ then $c'=c(q_1,i)(q_2,i+1)$
\item if $\alpha= (\pop,f)$ and $c=d(r,j)$ then $c'=d(f(r),j)$
\item in all other cases, $c'$ is not defined
\end{itemize}


\begin{remark}
~
\begin{itemize}


\item Nested marble transducers subsume both pebble and marble transducers.

\item They are closed under postcomposition by polyregular functions.

\item They are closed under pre-composition by rational functions
\end{itemize}


\end{remark}

\begin{example}
Let $A=\set{a,b}$. Let us define an \expreg function $f:\left(A\cup \set{\sharp}\right)^*\rightarrow (A\times \cup\set{0,1,\natural})^*$.
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 annotations, in the lexicographic order over the subset of positions of $u$, \eg

$f(aab)=a0a0b0\natural a0a0b1\natural a0a1b0\natural a0a1b1\natural a1a0b0\natural a1a0b1\natural a1a1b0\natural  a1a1b1$.

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$.
\end{example}

\begin{conjecture}
The function $f$ above is not definable by a nested marble transducer.
\end{conjecture}




\section{Nested invisible pebble transducer}

An invisible-pebble automaton $\auta$ is given by:
\begin{itemize}
\item a finite set of letters $A$, and two extra letters $\set{\vdash,\dashv}$
\item a finite set of states $Q$
\item a transition function $\delta: A_{\vdash,\dashv}{\times} Q \rightarrow {\set{\mleft,\mright}}{\times}Q + {\set{\push}}{\times}Q^2 +\set{\pop}$


\end{itemize}

Let us explain how the automaton is run over a word $u\in A^*$. The automaton actually runs over the word $v={\vdash} u {\dashv}$.
A \emph{configuration} $c$ over the word $v$ of length $n$ is a word over $Q\times\set{1,\ldots,n}$. The configuration is actually a stack of reading heads over the input word. The head of the stack is the \emph{active head}.
The \emph{initial configuration} of $\auta$ over $v$ is the word $(q_0,1)$. Given a non-empty configuration $c(p,i)$ the \emph{successor configuration} $c'$ is defined according to $\delta(v[i],p)=\alpha$ in the following way:
\begin{itemize}
\item if $\alpha=(\mleft,q)$, and $i>1$ then $c'=c(q,i-1)$
\item if $\alpha=(\mright,q)$, and $i<n$ then $c'=c(q,i+1)$
\item if $\alpha=(\push,q_1,q_2)$ then $c'=c(q_1,i)(q_2,i)$
\item if $\alpha= \pop$ then $c'=c$
\item in all other cases, $c'$ is not defined
\end{itemize}


A \emph{$1$-nested} invisible-pebble automaton $\auta$ is simply an invisible pebble automaton.
A \emph{$d+1$-nested} invisible-pebble automaton is given by a pair $(\auta,\autb)$

\begin{theorem}
   Any transduction defined by a nested marble transducer can be expressed as an \msomi. 
\end{theorem}

\begin{question}

Does $\ipt\subseteq \mt\circ\msot$ hold?
\end{question}


\section{Rational Turing Machine}


A \emph{Rational Turing Machine} is a Turing Machine with a reachability relation over configurations that is rational.


\begin{theorem}
A function is \expreg if and only if it is definable by a \drtm.
\end{theorem}

\begin{theorem}
For rational turing machines, the following hold:
\begin{enumerate}
\item \drtm = \dlinspace
\item \dlogspace= \dptime
\end{enumerate}
\end{theorem}

\section{List functions}

Types:

\begin{itemize}
\item $\tau^*$
\item $\tau^{\underline *}$
\item $\tau + \sigma$
\item $\tau \times \sigma$
\item $\tau \rightarrow \sigma$
\end{itemize}

Atomic programs: same as for polyregular list functions, except for \texttt{split}. Moreover each program involving $*$ has an equivalent version using $\astb$. Moreover we introduce a new basic program:

\begin{itemize}
\item $\texttt{subsets}^\tau: \tau^*\rightarrow ((\tau+\tau)^*)^\astb$

\end{itemize}



\section{The case of the successor}

Let us denote by \homo the class of free monoid homomorphisms.

\begin{theorem}
$\homo \circ\msomi$ with successor is equivalent to \dlinspace reductions.
\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. We use the homomorphism to erase the transitions that produce nothing.
\end{proof}


\section{Some remaining questions}

\subsection{Closure}

\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. In other words the problem can be formulated as: does $\rev\circ \msomi \subseteq \msomi$ hold? 
\end{question}
It works for commutative groups.

\subsection{Computing image}

\begin{question}
Given a (fixed) \msomi realizing $f$, can one compute the image of a word $u$ in time $O \big( |u|+|f(u)|\big)$ ?
\end{question}

   





\subsection{Computational models}

\begin{itemize}
    \item what about \mtt ? They have doubly-exponential growth, but do
      they capture \msomi  ?
    \item recursive programming language corresponding to or being
      captured by \msomi ?
	\item Krohn-Rhodes like decomposition \eg $\msoi\circ \mathsf{exp} \circ \msot$, with $\mathsf{exp}$ being some simple class of exponential growth function.
	
	\item Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\epsilon)$, with sequential functions compute \dlinspace ?
\end{itemize}




\bibliography{biblio}

\end{document}
