Select Git revision
postfilter_loader.pl
main.tex 17.32 KiB
\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}
\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^{1} + \ssign^{>1}\times\set{\sqsubseteq}$, where $\ssign^{1}$, $\ssign^{>1}$ denote the symbols of arity one and at least two, respectively. 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 $1$ is $\bigotimes_{i\leq n} \inter_{A_i}(R)$. The interpretation of $(R,\sumorder)$ is: $$\bigcup_{j\leq n}\quad \bigotimes_{i<j}\Delta_{i,k} \times\inter_{A_j}\times\bigotimes_{j<i\leq n}\dom_{A_i}$$
where $\Delta_{i,k}=\set{(a,\ldots,a)\in \dom_{A_i}^k\mid\ a\in \dom_{A_i}}$ is the $k$-fold diagonal of $\dom_{A_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 $O((2^n)^d)=O(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{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}