diff --git a/main.tex b/main.tex index 5068a572300159d083c66027063e52865dbf346b..f1e600098b11f755ca3d53281ef2bea24de1255e 100644 --- a/main.tex +++ b/main.tex @@ -1,8 +1,27 @@ \documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{article} -\usepackage{amssymb,amsthm,amsmath} - +\usepackage{amssymb,amsthm,amsmath,stmaryrd} +\usepackage{xspace} + +\newcommand{\expreg}{exporegular} +\newcommand{\Expreg}{Exporegular\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{\sst}{\textsf{SST}\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} \newtheorem{theorem}{Theorem} \newtheorem{corollary}{Corollary} @@ -10,7 +29,7 @@ \bibliographystyle{alpha}% the mandatory bibstyle -\title{Exporegular functions} %TODO Please add +\title{\Expreg functions} %TODO Please add \author{} @@ -24,10 +43,10 @@ \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 + functions definable by \sst with copy. We provide diverse + characterizations of \expreg 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} @@ -40,22 +59,31 @@ \label{sec:prelim} \subsection{Words, languages and transductions} \subsection{Relational structures and logical interpretations} -\subsection{Exporegular functions} +Here define \msoi and \foi. +\subsection{Monadic interpretation} -An exporegular function is a function $f : \Sigma^*\rightarrow -\Sigma^*$ defined by a monadic second-order interpretation\footnote{We +\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. +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_{U}(\bar X)$ defining the universe 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(B)$ over $\tsign$: the universe of $B$ is the set $U=\set{\bar X\mid\ A \models \phi_U(\bar X)}$, given $R\in \tsign$ of arity $k$, we define $R$ in $B$ as the set $\set{\tuple{\bar X_1,\ldots,\bar X_k}\in U^k\mid\ \phi_R(\bar X_1,\ldots,\bar X_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}$. + +\fomi is defined by restricting formulas to be in \fo. + +We call string-to-string (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). -We denote by \textsf{ExpF} the class of exporegular functions. +An \expreg function is a string-to-string monadic interpretation. +We denote by \textsf{ExpF} the class of \expreg 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 @@ -72,35 +100,48 @@ 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. + Let $T$ be an \msomi $T$ 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) \psi$ 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)$} \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. + 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 regular language by an exporegular - function is regular. In particular, exporegular functions have + The inverse image of any \fo-definable language by an \expreg + function is regular. In particular, \expreg functions have regular domains. \end{corollary} -\subsection{NMSOMI relations} +\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 +Just as \msot can be extended with parameters to add some form of +non-determinism, \msomi can also be extended with parameters to define +\expreg relations, and the backward translation theorem still +holds. We denote by $\textsf{ExpR}$ the class of \expreg relations. -\section{Expressiveness of exporegular functions} +\section{Expressiveness of \expreg\ functions} + +\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} + \begin{theorem} NSST$_{copy}$ $\subseteq$ \textsf{ExpR}. @@ -145,7 +186,7 @@ are of the form $x\not\in X_i \wedge x\in Y_i$. \end{proof} -\subsection{ExpoRegular functions of polynomial growth} +\subsection{\Expreg functions of polynomial growth} \begin{theorem} $\textsf{ExpF}\cap O(n^d) = \textsf{PolyF}$ @@ -159,17 +200,7 @@ are of the form $x\not\in X_i \wedge x\in Y_i$. 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}