diff --git a/main.tex b/main.tex index 9750026e57c53313b3f941f293ea33ac0b1eda22..8eb9f885902a59464a376065cb85ff43c374e3fb 100644 --- a/main.tex +++ b/main.tex @@ -6,6 +6,8 @@ \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} @@ -15,11 +17,17 @@ \newcommand{\msomi}{\textsf{MSO-MI}\xspace} \newcommand{\fomi}{\textsf{FO-MI}\xspace} \newcommand{\nmsomi}{\textsf{NMSO-MI}\xspace} -\newcommand{\rev}{\textsf{rev}\xspace} + \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{\dlin}{\textsc{DLinSpace}\xspace} \newcommand{\ssign}{\mathfrak{S}} @@ -99,7 +107,6 @@ 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 universe of $B$ is the set $U=\set{\bar S\mid\ A \models \phi_U(\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 U^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}$. -\fomi is defined by restricting formulas to be in \fo. 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}$. @@ -231,6 +238,18 @@ pebble transducer model. candidate: \begin{theorem} Any transduction defined by a nested marble transducer can be expressed as an \msomi. \end{theorem} +\begin{remark} +~ +\begin{itemize} + + +\item Nested marble transducers subsume both pebble and marble transducers. + +\item They are closed under postcomposition by polyregular functions. TODO check +\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 \set{0,1}\cup \set{\natural})^*$. @@ -255,16 +274,26 @@ 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,\push,\pop}$ -\item a push function: $\push: A_{\vdash,\dashv}\times Q\rightarrow Q$ -\item a pop update function: $\pop: A_{\tiny{\vdash,\dashv}}\times Q\rightarrow (Q\rightarrow Q)$ +\item a transition function $\delta: A_{\vdash,\dashv}\times Q \rightarrow \set{\mleft,\mright,\push,\pop}\times Q$ + \end{itemize} -Let us explain how the automaton is run over a word $w\in A^*$. The automaton actually runs over the word ${\vdash} w {\dashv}$. -A \emph{configuration} $c$ over a word ${\vdash} w {\dashv}$ 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}. +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)=(t,q)$ in the following way: +\begin{itemize} +\item if $t=\mleft$, and $i>1$ then $c'=c(q,i-1)$ +\item if $t=\mright$ and $i<n$ then $c'=c(q,i+1)$ +\item if $t=\push$ then $c'=c(p,i)(q,i)$ +\item if $t=\pop$ and $c=d(r,j)$ then $c'=d(q,j)$ +\item in all other cases, $c'$ is not defined +\end{itemize} +\begin{question} +Does $\ipt=\mt\circ\msot$ hold? +\end{question} \section{Some remaining questions} \subsection{Expressiveness} @@ -284,7 +313,7 @@ A \emph{configuration} $c$ over a word ${\vdash} w {\dashv}$ of length $n$ is a they capture \msomi ? \item recursive programming language corresponding or being captured by \msomi ? - \item Krohn-Rhodes like decomposition \eg $\mathsf{polyreg}\circ \mathsf{exp} \circ \mathsf{reg}$, with $\mathsf{exp}$ being some simple class of exponential growth function. + \item Krohn-Rhodes like decomposition \eg $\msoi\circ \mathsf{exp} \circ \msot$, with $\mathsf{exp}$ being some simple class of exponential growth function. \end{itemize}