after meeting of April 2022

main.tex

 
 \documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{article}
 
+\usepackage{amssymb,amsthm,amsmath}
+
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{corollary}{Corollary}
+
 
 \bibliographystyle{alpha}% the mandatory bibstyle
 
-\title{FO Model-Checking Superlinear\\ Transductions with Origin\\
-\small{and also a logic for SSTs}} %TODO Please add
+\title{Exporegular functions} %TODO Please add
 \author{}
 
 
@@ -17,7 +22,14 @@
 
 
 \begin{abstract}
-The abstract.
+    We introduce a new class of functions of exponential growth (at
+    most). It captures the class of polyregular functions and of
+    functions definable by SST with copy. We provide diverse
+    characterizations of exporegular functions: monadic-second order
+    interpretations (MSOMI). As an application, we prove that
+    model-checking non-deterministic SST with copy as well as
+    deterministic k-pebble transducers against a first-order logic
+    defining properties of their origin graphs is decidable. 
 \end{abstract}
 
 
@@ -28,17 +40,229 @@ The abstract.
 \label{sec:prelim}
 \subsection{Words, languages and transductions}
 \subsection{Relational structures and logical interpretations}
-\subsection{SSTs and pebble transducers, semantics with an without origin}
+\subsection{Exporegular functions}
+
+An exporegular function is a function $f : \Sigma^*\rightarrow
+\Sigma^*$ defined by a monadic second-order interpretation\footnote{We
+could add copy to MSOMI just as in Courcelle to avoid undesirable
+cornercase behaviours with small words.} $T =
+(\phi_{dom}(\overline{X}), \phi_\leq(\overline{X},\overline{Y}),
+\phi_\sigma({\overline{X}}))$ where each of those formulas are MSO
+formulas over signature $\{x\leq y,\sigma(x)\}$. We denote by
+MSOMI(s2s) those MSO-interpretations whose output structure  is a
+string (it is decidable), or just MSOMI if this is clear from the
+context. If instead FO formulas are used, we denote FO interpretations
+with monadic parameters by MSOI.
+
+
+We denote by \textsf{ExpF} the class of exporegular functions. 
+As an example, consider the following function. Let $\Sigma=\{a,b\}$
+and $\Gamma = \Sigma\times \{0,1\}\cup \#$. Let $u\in\Sigma^*$.
+Given a
+subset $U\subseteq Pos(u)$, we let $u_U\in \Gamma^*$ such that
+$|u_U| = |u|$ and for all positions $p$, $u_U(p) = (u(p), p\in
+U)$. Given another subset $V$, $U\leq_{lex} V$ if $U = V$ or the
+smallest $x$ such that $x\in V$ iff $x\not\in U$ satisfies $x\in V$
+and $x\not\in U$. Finally, we let $subsets(u) = \prod_{U\subseteq Pos(u) \text{ in
+    lexicographic order}} u_U\#$. For example,
+$$
+subsets(ab) = (a,0)(b,0)\#(a,0)(b,1)\#(a,1)(b,0)\#(a,1)(b,1)\#
+$$
+It is easy to see that $subsets\in\textsf{ExpF}$. 
+
+
+\begin{theorem}[Backward translation theorem]
+    Given an MSOMI $T$ (from $\sigma$-relational structures to
+    $\beta$-relational structures) and some FO formula $\phi$ over
+    $\beta$, $T^{-1}(\phi)$, the set of $\sigma$-relational structures
+    $A$ such that $T(A)\models \phi$, is $MSO[\sigma]$-definable. 
+\end{theorem}
+
+\begin{proof}
+    Idea: any first-order quantification $\exists x$ in $\phi$ is
+    replaced by the monadic quantification $\exists \overline{X}$,
+    the atoms $x\leq y$ are replaced by
+    $\phi_\leq(\overline{X},\overline{Y})$, etc. 
+\end{proof}
+
+\begin{corollary}
+    The inverse image of any regular language by an exporegular
+    function is regular. In particular, exporegular functions have
+    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
+exporegular relations, and the backward translation theorem still
+holds. We denote by $\textsf{ExpR}$ the class of exporegular
+relations. 
+
+
+\section{Expressiveness of exporegular functions}
+
+\begin{theorem}
+    NSST$_{copy}$ $\subseteq$ \textsf{ExpR}. 
+\end{theorem}
+
+\begin{proof}
+    See IPAD notes. 
+\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
+$n=|\overline{X}|=|\overline{Y}|$:
+
+$$
+\overline{X} = \overline{Y}\vee \bigvee_{i=1}^{n} (\bigwedge_{1\leq
+  j<i} X_j = Y_j)\wedge \exists x\ \textsf{first-diff}(x,X_i,Y_i)\wedge \psi_i(x,X_i,Y_i)
+$$
+where $\psi_i$ are MSO-formulas and $\textsf{first-diff}(x,X_i,Y_i)$
+holds true if $x$ is the $\leq$-smallest position in $X_i\cup Y_i$
+such that $x\in X_i\leftrightarrow y\not\in Y_i$. 
+
+
+An MSOMI $T$ is \emph{purely} lexicographic if all $\psi_i(x,X_i,Y_i)$
+are of the form $x\not\in X_i \wedge x\in Y_i$.
+
+\begin{theorem}
+    A transduction $f$ is definable by an SST with copy iff it is
+    definable by a purely lexicographic MSOMI. 
+\end{theorem}
+
+\subsection{Polyregular functions}
+
+
+\begin{theorem}
+    \textsf{PolyF} $\subseteq$ \textsf{ExpF}
+\end{theorem}
+
+\begin{proof}
+\textsf{PolyF} = MSOI $\subseteq$ MSOMI = \textsf{ExpF}
+\end{proof}
+
+
+\subsection{ExpoRegular functions of polynomial growth}
+
+\begin{theorem}
+    $\textsf{ExpF}\cap O(n^d) = \textsf{PolyF}$
+\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{Closure properties}
+
+\begin{theorem}
+    FOI $\circ$ MSOMI = MSOMI
+\end{theorem}
+
+\begin{proof}
+    Use standard ideas for composition logical transductions: formula
+    substitutions. The first-order parameters of the FOI becomes
+    monadic parameters. 
+\end{proof}
+
 
 \section{FO model-checking of transductions with origins: SSTs and pebble transducers}
 \label{sec:mc}
-\subsection{The Backward Translation Theorem}
 \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}
+
+
+\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.
+\end{theorem}
+
+\begin{proof}
+    See IPAD notes.
+\end{proof}
+
+
 \subsection{Model-checking pebble transducers with origin}
 
-\section{SSTs and lexicographic MSO-interpretations}
-\label{sec:sst-lex}
+Origin = head position
+
+\begin{theorem}
+    Model-checking non-deterministic 2-pebble transducers against FO[o] is undecidable.
+\end{theorem}
+
+\begin{proof}
+    See IPAD notes.
+\end{proof}
+
+
+\begin{theorem}
+    Model-checking deterministic pebble transducers against FO[o] is decidable.
+\end{theorem}
+
+\begin{proof}
+    Use DPT = MSOI and the backward translation theorem. 
+\end{proof}
+
+
+\section{Some remaining questions}
+
+\subsection{Expressiveness}
+
+
+\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:
+      $$
+      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 ?
+\end{itemize}
+
+\subsection{Computational models}
+
+\begin{itemize}
+    \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). 
+\end{itemize}
 
 
 \bibliography{biblio}