diff --git a/main.tex b/main.tex index 32fbf416cf080c3cd37772dad77789283407034f..9807e302c0a4bbfbcf54ca98f66082cd1d48877e 100644 --- a/main.tex +++ b/main.tex @@ -20,6 +20,11 @@ \newcommand{\nmsomi}{\textsf{NMSO-MI}\xspace} \newcommand{\pow}[1]{\mathsf{2}^{#1}} \newcommand{\ar}{\mathsf{ar}} +\newcommand{\dom}{\mathsf{dom}} +\newcommand{\lefto}{\mathsf{left}} +\newcommand{\righto}{\mathsf{right}} +\newcommand{\inter}{\mathsf{I}} +\newcommand{\sumorder}{\sqsubseteq} \newcommand{\sst}{\textsf{SST}\xspace} \newcommand{\mt}{\textsf{MT}\xspace} @@ -91,9 +96,18 @@ \paragraph{Signature} 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} $w$ over a signature $\ssign$ is given as a \emph{domain} $D$ together with a function which maps any symbol $R$ of $\ssign$ to a set denoted $R^w$ such that $R^w\subseteq D^r$, with $r=\ar(R)$. +\paragraph{Structures} A \emph{structure} $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} The \emph{disjoint union} of two structures over +\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. + +The \emph{disjoint union} (or coproduct) of two structures $A,B$ over the signature $\ssign$ is a structure $A+B$ over signature $\ssign+\set{\lefto,\righto}$ where $\lefto, \righto$ are unary symbols. The domain of $A+B$ is $\dom_A+\dom_B=(\dom_A{\times}\set{1}) \cup (\dom_B{\times}\set{2}) $. The interpretation of a symbol $R$ is $\inter_A(R)+\inter_B(R)$. The interpretation of $\lefto$ is $\dom_A\times\set{1}$ and the interpretation of $\righto$ is $\dom_B\times\set{2}$. + +The \emph{product} of two structures $A,B$ over a signature $\ssign$ is a structure $A\times B$ over signature $\ssign\times\set{\lefto,\righto}$ where $(R,\lefto)$ and $(R, \righto)$ have the same arity as $R$. The domain of $A\times B$ is $\dom_A\times\dom_B$. The interpretation of a symbol $(R,\lefto)$ is $\inter_A(R)\times \dom_B$ and the interpretation of $(R,\righto)$ is $\dom_A\times \inter_B(R)$. + +The \emph{ordered coproduct} of a sequence of structures $A_1,\cdots, A_n$ over the same signature $\ssign$ is a structure $\bigoplus_{i\leq n} A_i$ over the signature $\ssign+\set{\sqsubseteq}$, where $\sqsubseteq$ has arity $2$. The domain of $\bigoplus_{i\leq n} A_i$ is $\bigoplus_{i\leq n} \dom_{A_i}=\bigcup_{i\leq n} \dom_{A_i}{\times}\set{i}$. The interpretation of a symbol $R$ is $\bigoplus_{i\leq n} \inter_{A_i}(R)$. The interpretation of $\sumorder$ is $\bigcup_{i\leq j\leq n}(\dom_{A_i}{\times}\set{i})\times(\dom_{A_j}{\times}\set{j})$. + +The \emph{ordered product} of a sequence of structures $A_1,\cdots, A_n$ over the same signature $\ssign$ is a structure $\bigotimes_{i\leq n} A_i$ over the signature $\ssign\times\set{\sqsubseteq}$. The domain of $\bigotimes_{i\leq n} A_i$ is $\bigotimes_{i\leq n} \dom_{A_i}$. The interpretation of a symbol $R$ is $\bigoplus_{i\leq n} \inter_{A_i}(R)$. The interpretation of $\sumorder$ is $\bigcup_{i\leq j\leq n}(\dom_{A_i}{\times}\set{i})\times(\dom_{A_j}{\times}\set{j})$. \paragraph{The orderned model of words}