Skip to content
Snippets Groups Projects
Commit 3abbeec0 authored by Nathan Lhote's avatar Nathan Lhote
Browse files

m

parent b6cc8d06
No related branches found
No related tags found
No related merge requests found
\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{article} \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{theorem}{Theorem}
\newtheorem{corollary}{Corollary} \newtheorem{corollary}{Corollary}
...@@ -10,7 +29,7 @@ ...@@ -10,7 +29,7 @@
\bibliographystyle{alpha}% the mandatory bibstyle \bibliographystyle{alpha}% the mandatory bibstyle
\title{Exporegular functions} %TODO Please add \title{\Expreg functions} %TODO Please add
\author{} \author{}
...@@ -24,10 +43,10 @@ ...@@ -24,10 +43,10 @@
\begin{abstract} \begin{abstract}
We introduce a new class of functions of exponential growth (at We introduce a new class of functions of exponential growth (at
most). It captures the class of polyregular functions and of most). It captures the class of polyregular functions and of
functions definable by SST with copy. We provide diverse functions definable by \sst with copy. We provide diverse
characterizations of exporegular functions: monadic-second order characterizations of \expreg functions: monadic-second order
interpretations (MSOMI). As an application, we prove that interpretations (\msomi). As an application, we prove that
model-checking non-deterministic SST with copy as well as model-checking non-deterministic \sst with copy as well as
deterministic k-pebble transducers against a first-order logic deterministic k-pebble transducers against a first-order logic
defining properties of their origin graphs is decidable. defining properties of their origin graphs is decidable.
\end{abstract} \end{abstract}
...@@ -40,22 +59,31 @@ ...@@ -40,22 +59,31 @@
\label{sec:prelim} \label{sec:prelim}
\subsection{Words, languages and transductions} \subsection{Words, languages and transductions}
\subsection{Relational structures and logical interpretations} \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 \footnote{We
\Sigma^*$ defined by a monadic second-order interpretation\footnote{We
could add copy to MSOMI just as in Courcelle to avoid undesirable could add copy to MSOMI just as in Courcelle to avoid undesirable
cornercase behaviours with small words.} $T = cornercase behaviours with small words.}
(\phi_{dom}(\overline{X}), \phi_\leq(\overline{X},\overline{Y}),
\phi_\sigma({\overline{X}}))$ where each of those formulas are MSO 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:
formulas over signature $\{x\leq y,\sigma(x)\}$. We denote by \begin{itemize}
MSOMI(s2s) those MSO-interpretations whose output structure is a \item An \mso-formula $\phi_{U}(\bar X)$ defining the universe of the output structure
string (it is decidable), or just MSOMI if this is clear from the \item For each relation $R\in \tsign$ of arity $k$, a formula $\phi_R(\bar X _1,\ldots, \bar X_k )$
context. If instead FO formulas are used, we denote FO interpretations
with monadic parameters by MSOI. \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\}$ As an example, consider the following function. Let $\Sigma=\{a,b\}$
and $\Gamma = \Sigma\times \{0,1\}\cup \#$. Let $u\in\Sigma^*$. and $\Gamma = \Sigma\times \{0,1\}\cup \#$. Let $u\in\Sigma^*$.
Given a Given a
...@@ -72,35 +100,48 @@ It is easy to see that $subsets\in\textsf{ExpF}$. ...@@ -72,35 +100,48 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
\begin{theorem}[Backward translation theorem] \begin{theorem}[Backward translation theorem]
Given an MSOMI $T$ (from $\sigma$-relational structures to Let $T$ be an \msomi $T$ of dimension $d$ from structures over $\ssign$ to
$\beta$-relational structures) and some FO formula $\phi$ over structures over $\tsign$ ,and let $\phi(x_1,\dots,x_k)$ be an \fo-formula over
$\beta$, $T^{-1}(\phi)$, the set of $\sigma$-relational structures $\tsign$.
$A$ such that $T(A)\models \phi$, is $MSO[\sigma]$-definable. 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} \end{theorem}
\begin{proof} \begin{proof}
Idea: any first-order quantification $\exists x$ in $\phi$ is Idea: any first-order quantification $\exists x$ in $\phi$ is
replaced by the monadic quantification $\exists \overline{X}$, replaced by the monadic quantification $\exists \overline{X}$,
the atoms $x\leq y$ are replaced by the atoms $R(x_1,\dots,x_k)$ are replaced by
$\phi_\leq(\overline{X},\overline{Y})$, etc. $\phi_R(\bar X_1,\ldots,\bar X_k)$, etc.
\end{proof} \end{proof}
\begin{corollary} \begin{corollary}
The inverse image of any regular language by an exporegular The inverse image of any \fo-definable language by an \expreg
function is regular. In particular, exporegular functions have function is regular. In particular, \expreg functions have
regular domains. regular domains.
\end{corollary} \end{corollary}
\subsection{NMSOMI relations} \subsection{\nmsomi relations}
Just as MSOT can be extended with parameters to add some form of Just as \msot can be extended with parameters to add some form of
non-determinism, MSOMI can also be extended with parameters to define non-determinism, \msomi can also be extended with parameters to define
exporegular relations, and the backward translation theorem still \expreg relations, and the backward translation theorem still
holds. We denote by $\textsf{ExpR}$ the class of exporegular holds. We denote by $\textsf{ExpR}$ the class of \expreg
relations. 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} \begin{theorem}
NSST$_{copy}$ $\subseteq$ \textsf{ExpR}. NSST$_{copy}$ $\subseteq$ \textsf{ExpR}.
...@@ -145,7 +186,7 @@ are of the form $x\not\in X_i \wedge x\in Y_i$. ...@@ -145,7 +186,7 @@ are of the form $x\not\in X_i \wedge x\in Y_i$.
\end{proof} \end{proof}
\subsection{ExpoRegular functions of polynomial growth} \subsection{\Expreg functions of polynomial growth}
\begin{theorem} \begin{theorem}
$\textsf{ExpF}\cap O(n^d) = \textsf{PolyF}$ $\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$. ...@@ -159,17 +200,7 @@ are of the form $x\not\in X_i \wedge x\in Y_i$.
Moreover, it is decidable whether an 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} \section{FO model-checking of transductions with origins: SSTs and pebble transducers}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment