diff --git a/main.tex b/main.tex index a87b03ed8db2c56eeceba963cfdf40f51d16629d..5b551c444b3827434281a463510c64a94cb03450 100644 --- a/main.tex +++ b/main.tex @@ -32,12 +32,20 @@ \newcommand{\eg}{\textit{e.g.~}} \newcommand{\ie}{\textit{i.e.~}} +\newcommand{\mleft}{\mathsf{left}} +\newcommand{\mright}{\mathsf{right}} +\newcommand{\push}{\mathsf{push}} +\newcommand{\pop}{\mathsf{pop}} +\newcommand{\auta}{\mathcal A} + \newtheorem{theorem}{Theorem} \newtheorem{corollary}{Corollary} +\newtheorem{conjecture}{Conjecture} \theoremstyle{definition} \newtheorem{remark}{Remark} \newtheorem{question}{Question} +\newtheorem{example}{Example} \bibliographystyle{alpha}% the mandatory bibstyle @@ -54,14 +62,7 @@ \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 \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} @@ -224,13 +225,41 @@ Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\e We define a model of transducers based on marble transducers. pebble transducer model. candidate: - layered marble transducers. A finite number of layers. a marble of layer k cannot go through another marble of layer k. However it can go through marbles of layers $<k$. - TODO: find a better name than "marble" + nested marble transducers. A finite nesting height. a marble of height k cannot go through another marble of height k. However it can go through marbles of height $<k$. + %TODO: find a better name than "marble" \begin{theorem} Any transduction defined by a nested marble transducer can be expressed as an \msomi. \end{theorem} +\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})^*$. +What the function $f$ does is list all subsets of positions (without $\sharp$) and output the corresponding subword. The subword are output in a specific order, and separated by $\natural$. Let us decribe the order in which these subsets of positions are listed. + +Over a word $u$ without $\sharp$, $f$ outputs the list of all subwords (with multiplicities), in the lexicographic order over the subset of positions of $u$, \eg $f(aab)=\natural b\natural a\natural ab\natural a\natural ab\natural aa\natural aab$; each subword corresponding the the subsets $000,001$, $010$, $011$, $100$, $101$, $110,111$, in respective order. +Basically, the most significant figure inside a block between two $\sharp$ symbols is to the left. However, the most significant blocks are to the right, \eg: $f(a\sharp b)=\natural a \natural b\natural ab$. +\end{example} + +\begin{conjecture} +The function $f$ above is not definable by a nested marble transducer. +\end{conjecture} + + + +\section{Nested invisible pebble transducer} + +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)$ + +\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}. \section{Some remaining questions}