Skip to content
Snippets Groups Projects
Select Git revision
  • b6cc8d0664510c171379d077b927971cfd76a18a
  • main default protected
2 results

main.tex

Blame
  • user avatar
    filiot authored
    b6cc8d06
    History
    main.tex 8.06 KiB
    
    \documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{article}
    
    \usepackage{amssymb,amsthm,amsmath}
    
    
    \newtheorem{theorem}{Theorem}
    \newtheorem{corollary}{Corollary}
    
    
    \bibliographystyle{alpha}% the mandatory bibstyle
    
    \title{Exporegular functions} %TODO Please add
    \author{}
    
    
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    
    \begin{document}
    \maketitle
    
    
    
    \begin{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}
    
    
    \section*{Introduction}
    \label{sec:intro}
    
    \section{Words, transducers and logic}
    \label{sec:prelim}
    \subsection{Words, languages and transductions}
    \subsection{Relational structures and logical interpretations}
    \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{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}
    
    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}
    
    \end{document}