A \emph{signature}$\ssign$ is a set $S$ of \emph{symbols}\footnote{We only consider relational signatures.}, together with an \emph{arity function}, which we denote by $\ar:S\rightarrow\nat$. Abusing notations, we will often write $R\in\ssign$ instead of $R\in S$.
\paragraph{Structures} A \emph{structure} (sometimes \emph{model}) $A$ over a signature $\ssign$ is given as a \emph{domain}$\dom_A$ together with an \emph{interpretation function} which maps any symbol $R$ of $\ssign$ to a set denoted $\inter_A(R)$ such that $\inter_A(R)\subseteq\dom(A)^r$, with $r=\ar(R)$.
\paragraph{Structures} A \emph{structure} (sometimes \emph{model}) $A$ over a signature $\ssign$ is given as a \emph{domain}$\dom_A$ together with an \emph{interpretation function} which maps any symbol $R$ of $\ssign$ to a set denoted $\inter_A(R)$ such that $\inter_A(R)\subseteq\dom_A^r$, with $r=\ar(R)$.
\paragraph{Operations}
Any structure over a signature can be seen as a structure over a larger signature where additional symbols are interpreted as empty sets.
...
...
@@ -219,7 +220,7 @@ From the backward translation theorem.
\subsubsection{Exponential growth}
\begin{remark}
An \msomi of dimension $d$ has growth $O((2^n)^d)=O(2^{dn})=2^{O(n)}$.
An \msomi of dimension $d$ has growth $\leq(2^n)^d=2^{dn}=2^{O(n)}$.
\end{remark}
\begin{corollary}
...
...
@@ -358,6 +359,26 @@ For rational turing machines, the following hold:
\end{enumerate}
\end{theorem}
\section{List functions}
Types:
\begin{itemize}
\item$\tau^*$
\item$\tau^{\underline*}$
\item$\tau+\sigma$
\item$\tau\times\sigma$
\item$\tau\rightarrow\sigma$
\end{itemize}
Atomic programs: same as for polyregular list functions, except for \texttt{split}. Moreover each program involving $*$ has an equivalent version using $\astb$. Moreover we introduce a new basic program:
