m

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}