dg.tex revision 01f8490b545292b8e15df76c1e4095829a69d293
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoWe describe in this section how Maude structuring mechanisms
6294ad597249a611c59e0dbf122ca9b89e679ba8Adrián Riescodescribed in Section \ref{sec:maude}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoare translated into development graphs. Then, we explain how these development
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescographs are normalized to deal with freeness constraints.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsection{Creating the development graph}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoWe describe here how Maude modules, theories, and views are translated into
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescodevelopment graphs, illustrating it with an example.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Modules}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoEach Maude module generates two nodes in the development
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescograph. The first one contains the theory equipped with the usual
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoloose semantics. The second one, linked
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoto the first one with a free definition link (whose signature morphism
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescois detailed below), contains the same signature but
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescono local axioms and stands for the free models of the theory.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoNote that Maude theories only generate one node, since their initial
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescosemantics is not used by Maude specifications.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoThe model class of parameterized modules
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoconsists of free extensions of the models of their parameters, that are
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescopersistent on sorts, but not on kinds. This notion of freeness has been
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescostudied in \cite{BouhoulaJM00} under assumptions like existence of top sorts for kinds
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoand sorted variables in formulas; our results hold under similar
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescohypotheses. We use non-persistent free links to link these modules with
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescotheir corresponding theories.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Module expressions}\label{subsec:me}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude module expressions allow to combine and modify the information
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocontained in Maude modules.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoWhen the module expression is a simple identifier the development
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescograph remains unchanged.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoThe summation expression of the module expressions $\mathit{ME}_1$ and
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco$\mathit{ME}_2$ generates a new node in the development graph
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco$(\mathit{ME}_1 + \mathit{ME}_2)$ with
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescothe union of the information in both summands. A definition link
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescois also created between the original expressions and the resulting one.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoThe renaming expression $\mathit{ME} * (R)$ creates a morphism with
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescothe information given in $R$ that will be used as to label the link.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Importations}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoAs explained above, each Maude module generates two nodes in the development
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescowhen importing a module, we will select the node used depending on the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescochosen importation mode:
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe \verb"protecting" mode generates a non-persistent free link between
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe current node and the node standing for the free semantics of the
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoincluded one. Note that we used the same links for the parameters in
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoparameterized modules.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe \verb"extending" mode generates a global link with the annotation
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\textsf{PCons?}, that stands for proof-theoretic conservativity and that
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescocan be checked with a special conservativity checker that is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescointegrated into \Hets.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe \verb"including" mode generates a global definition link between the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescocurrent node and the node standing for the loose semantics of the
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Views}\label{subsec:dg_views}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude views have a theory as source and either a module or a theory
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoas target. All the sorts and the operators declared in the source theory
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescohave to be mapped to sorts and operators in the target.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoA particular case of mapping between operators is the mapping between
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoterms, that has the general form $\verb"op" \; e \; \verb"to term" \; t$
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescowhere $e$ is a term consisting of a
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosingle operator applied to variables declared either on-the-fly or with
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescovariable declarations in the same view and the target term is any term
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescowith variables, those in the source $e$ in the corresponding sorts
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoresulting from the mapping.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoSince this shortcut allows to map operators with different profiles,
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoViews generate a theorem
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescolink between the theory and the module satisfying it.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoNote that an instantiation generates some implicit morphisms and modifies
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescothe ones stated in the views, see Section \ref{subsec:adv_feat} for details:
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\begin{itemize}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoSorts and labels are qualified by the parameter name in order to distinguish
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescodifferent labels/sorts with the same name defined in different theories. Thus,
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescothe mapping indicated by the view (more specifically, the source sorts) is
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescomodified depending on the name of the parameter.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoAs explained in the Section \ref{subsec:pmod}, parameterized modules can
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescodefine parameterized sorts, that is, sorts that use the parameters as part of
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescothe sort name and hence they are modified by the mapping in the view.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoMoreover, when the target of a view is a theory the identifiers of these sorts
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoare extended with the name of the view and the name of the new parameter.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoThus, the sort morphism is extended with these new renamings.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Development graph: An example}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoWe illustrate how to build the development graph with an example. Consider
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe following Maude specifications:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{verbatim}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescofmod M1 is fmod M2 is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco sort S1 . sort S2 .
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco op _+_ : S1 S1 -> S1 [comm] . endfm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoth T is mod M3{X :: T} is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco sort S1 . sort S4 .
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco op _._ : S1 S1 -> S1 . endm
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco eq V1:S1 . V2:S1 = V2:S1 . V1:S1 [nonexec] .
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescomod M is view V from T to M is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco ex M1 + M2 * (sort S2 to S) . op _._ to _+_ .
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\end{verbatim}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{figure}[t]
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{center}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\includegraphics[scale=.47]{dg}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\caption{Development Graph for Maude Specifications\label{fig:dg}}
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\noindent \Hets builds the graph shown in Figure \ref{fig:dg},
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowhere the following steps take place:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item Each module has generated a node with its name and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoanother primed one that contains the initial model, while both of them
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoare linked with a non-persistent free link. Note that theory \verb"T" did not
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescogenerate this primed node.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item The summation expression has created a new node that includes the theories
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoof \verb"M1" and \verb"M2", importing the latter with a renaming; this new
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesconode, since it is imported in \verb"extending" mode, uses a link with the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\textsf{PCons?} annotation.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item There is a theorem link between \verb"T" and the free (here: initial) model of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\verb"M". This link is labeled with the mapping defined in the view \verb"V".
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item The parameterized module \verb"M3" includes the theory of its parameter
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowith a renaming, that qualifies the sort. Note that these nodes are connected
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoby means of a non-persistent freeness link.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoIt is straightforward to show:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{theorem}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe translation of Maude modules into development graphs is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosemantics-preserving. %\ednote{Undefined semantics-preserving}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoOnce the development graph is built, we can apply the (logic
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoindependent) calculus rules that reduce global theorem links to local
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescotheorem links, which are in turn discharged by local theorem proving
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\cite{MAH-05-a}. This can be used to prove Maude views, like e.g.\
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco``natural numbers are a total order.'' We show in the next
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosection how we deal with the freeness constraints imposed by free
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescodefinition links.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\subsection{Normalization of free definition links}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\label{sec:free}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoMaude uses initial and free semantics intensively. The semantics of
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescofreeness is, as mentioned, different from the one used in \CASL in
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothat the free extensions of models are required to be persistent
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoonly on sorts and new error elements can be added on the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescointerpretation of kinds. Attempts to design the translation to \CASL
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoin such a way that Maude free links would be translated to usual free
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescodefinition links in \CASL have been unsuccessful. We decided thus to
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescointroduce a special type of links to represent Maude's freeness in
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\CASL. In order not to break the development graph calculus, we need
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoa way to normalize them. The idea is to replace them with a
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosemantically equivalent development graph in \CASL. The main idea is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoto make a free extension persistent by duplicating parameter sorts
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoappropriately, such that the parameter is always explicitly included
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoin the free extension.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoFor any Maude signature $\Sigma$, let us define
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoan extension $\Sigma^\# = (S^\#, \leq^\#, F^\#, P^\#)$ of the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescotranslation $\Phi(\Sigma)$ of $\Sigma$ to \CASL as follows:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $S^\#$ unites with the sorts of $\Phi(\Sigma)$ the set
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $\{[s] \mid s \in Sorts(\Sigma)\}$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $\leq^\#$ extends the subsort relation $\leq$ with pairs
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $(s, [s])$ for each sort $s$ and $([s],[s'])$ for any sorts $s \leq s'$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $F^\#$ adds the function symbols $\{f:[w] \rightarrow [s]\}$ for all
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco function symbols on sorts $f:w \rightarrow s $;\footnote{$[x_1 \ldots x_n]$
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco is defined to be $[x_1] \ldots [x_n]$.} and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $P^\#$ adds the predicate symbol $rew$ on all new sorts.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoNow, we consider a Maude non-persistent free definition link and let
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\sigma: \Sigma \rightarrow \Sigma'$ be the morphism labeling it.%
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\footnote{In Maude, this would usually be an injective renaming.}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoWe define a \CASL signature morphism
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $\sigma^\# : \Phi(\Sigma) \rightarrow \Sigma'^\#$: on sorts,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $\sigma^\#(s) := \sigma^{sort}(s)$ and $\sigma^\#([s]):=[\sigma^{sort}(s)]$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco on operation symbols, we can define $\sigma^ \#(f) :=
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \sigma^{op}(f)$ and this is correct because the operation symbols were
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco introduced in $\Sigma'^\#$; $rew$ is mapped identically.
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoThe normalization of Maude freeness is then illustrated in Figure \ref{nf}.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoGiven a free non-persistent definition link $\flinka{M}{\sigma}{N}$, with
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\sigma:\Sigma\rightarrow \Sigma_N$, we first take the translation of the nodes
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoto \CASL (nodes $M'$ and $N'$) and then introduce a new node, $K$, labeled with
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\Sigma^\#_N$, a global definition link from $M'$ to $M''$ labeled with the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoinclusion $\iota_N$ of $\Sigma_N$ in $\Sigma^\#_N$, a free definition link from
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$M''$ to $K$ labeled with
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\sigma^\#$ and a hiding definition link from $K$ to $N'$ labeled with the
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riescoinclusion $\iota_N$.\footnote{The arrows without labels in Figure \ref{nf}
6294ad597249a611c59e0dbf122ca9b89e679ba8Adrián Riescocorrespond to heterogeneous links from Maude to \CASL.}
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\begin{figure}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoM \ar@{=>}[rr]_{n.p.free}^{\sigma} \ar@{=>}[d]& & N \ar@{=>}[dd]\\
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoM'\ar@{=>}[d]^{\iota_N}& & \\
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoM''\ar@{=>}[r]_{free}^{\sigma^\#} & K \ar@{=>}[r]_{hide}^{\iota_n} & N'
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\caption{Normalization of Maude free links}\label{nf}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoNotice that the models of $N$ are Maude reducts of \CASL models of $K$,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoreduced along the inclusion $\iota_N$.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe next step is to eliminate \CASL free definition links.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe idea is to use then a transformation specific to the second-order
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoextension of \CASL to normalize freeness.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe intuition behind this construction is that
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoit mimics the quotient term algebra construction,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothat is, the free model is specified as the homomorphic image
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoof an absolutely free model (i.e.\ term model).
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoWe are going to make use of the following known facts \cite{Reichel87}:
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoExtensions of theories in Horn form admit free extensions of models.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoExtensions of theories in Horn form are monomorphic.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoGiven a free definition link $\flinka{M}{\sigma}{N}$, with
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\sigma:\Sigma\rightarrow \Sigma^N$ such that $Th(M)$ is in Horn
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoform, replace it with
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoM \ar@{=>}[r]^{incl} &
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoK \ar@{=>}[r]^{incl}_{hide} &
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco}, where $N'$ has the same signature as $N$, $incl$ denotes inclusions and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe node $K$ is constructed as follows.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe signature $\Sigma^K$ consists of the signature $\Sigma^M$ disjointly
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescounited with a copy of $\Sigma^M$, denoted $\iota(\Sigma_M)$ which makes all function symbols total
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco(let us denote $\iota(x)$ the corresponding symbol in this copy for each
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosymbol $x$ from the signature $\Sigma^M$) and augmented with new operations
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$h: \iota(s) \rightarrow ?s$, for any sort $s$ of $\Sigma^M$ and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$make_s:s\rightarrow \iota(s)$, for any sort $s$ of the source
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosignature $\Sigma$ of the morphism $\sigma$ labelling the free definition link.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe axioms $\psi^K$ of the node $K$ consist of:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosentences imposing the bijectivity of \textit{make};
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item axiomatization of the sorts in $\iota(\Sigma_M)$ as free types
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowith all operations as constructors, including $make$ for the sorts
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoin $\iota(\Sigma)$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item homomorphism conditions for $h$:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $$ h(\iota(f)(x_1, \dots, x_n)) = f(h(x_1), \dots, h(x_n)) $$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\iota(p)(t_1, \dots, t_n) \Rightarrow p(h(t_1), \dots, h(t_n))$$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item surjectivity of homomorphisms:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\forall y : s . \exists x:\iota(s) . h(x) \EEQ y$$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item a second-order formula saying that the kernel of $h$ is the least
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescopartial predicative congruence\footnote
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco{A partial predicative congruence consists of a symmetric
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoand transitive binary relation for each sort and a relation
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoof appropriate type for each predicate symbol.} satisfying
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$Th(M)$. This is done by quantifying over a predicate symbol for each sort
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescofor the binary relation and one predicate symbol for each relation symbol
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\begin{array}{l}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \forall \{P_s : \iota(s), \iota(s)\}_{s \in Sorts(\Sigma_M)} ,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \{P_{p:w} : \iota(w)\} _{p:w \in \Sigma_M} \\
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\mathit{symmetry}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \land \mathit{transitivity}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \land \mathit{congruence}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\land \mathit{satThM}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\implies \mathit{largerThenKerH}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowhere $\mathit{symmetry}$ stands for
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\bigwedge_{s\in Sorts(\Sigma^M)} \forall x:{\iota(s)},y:{\iota(s)}.P_s(x,y)\implies P_s(y, x),$$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\mathit{transitivity}$ stands for
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\bigwedge_{s\in Sorts(\Sigma^M)} \forall x:{\iota(s)},y:{\iota(s)},z:{\iota(s)}.P_s(x, y)\land P_s(y, z)\implies P_s(x, z),$$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\mathit{congruence}$ stands for
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{array}{l}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\bigwedge_{f_{w\rightarrow s}\in\Sigma^M} \forall x_1\ldots x_n:{\iota(w)},y_1\ldots y_n:{\iota(w)}\,.\,\,\\
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoD(\iota(f_{w,s})(\bar{x}))\land D(\iota(f_{w,s})(\bar{y}))\land P_w(\bar{x},\bar{y})
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\implies P_s(\iota(f_{w,s})(\bar{x}),\iota(f_{w,s})(\bar{y}))
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{array}{l}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\bigwedge_{p_w \in\Sigma^M} \forall x_1\ldots x_n:{\iota(w)},y_1\ldots y_n:{\iota(w)}\,.\,\,\\
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoD(\iota(f_{w,s})(\bar{x}))\land D(\iota(f_{w,s})(\bar{y}))\land P_w(\bar{x},\bar{y})
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\implies P_{p:w}(\bar{x}) \Leftrightarrow P_{p:w}(\bar{y})
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\noindent where $D$ indicates definedness. $\mathit{satThM}$ stands for
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$Th(M)[\EEQ/P_s; p:w/P_{p:w}; D(t)/P_s(t,t); t=u/P_s(t,u)\lor(\neg P_s(t,t)\land\neg P_s(u,u))]$$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowhere, for a set of formulas $\Psi$, $\Psi[sy_1/sy'_1;\ldots ;sy_n/sy'_n]$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescodenotes the simultaneous substitution of $sy'_i$ for $sy_i$ in
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoall formulas of $\Psi$ (while possibly instantiating the meta-variables
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoFinally $\mathit{largerThenKerH}$ stands for
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$$\begin{array}{l}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\bigwedge_{s\in Sorts(\Sigma^M)} \forall x:{\iota(s)},y:{\iota(s)}.h(x)\EEQ h(y)\implies P_s(x, y)\\
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\bigwedge \land_{p_w\in\Sigma^M} \forall \bar{x}:{\iota(w)}.\iota(p:w)(\bar{x})
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\implies P_{p:w}(\bar{x})
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{proposition}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe models of the nodes $N$ and $N'$ are
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\end{proposition}%\ednote{AR: Proof in appendix?}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco{\noindent\it Proof.}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoLet $n$ be a $N$-model. To prove that $n$ is also a $N'$-model,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowe need to show that it has a $K$-expansion.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoLet us define the following $\Sigma_K$ model, denoted $k$:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item on $\Sigma_M$, $k$ coincides with $n$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item on $\iota(\Sigma_M)$, the interpretation of sorts and function symbols
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescois given by the free types axioms (i.e. sorts are interpreted as set of terms,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescooperations $\iota(f)$ map terms $t_1,..t_n$ to the term
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\iota(f)(t_1,..,t_n)$). We define interpretation of predicates after defining $h$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item $make$ assigns to each $x$ the term $make(x)$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item the homomorphism $h$ is defined inductively as follows:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \begin{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $h(make(x)) = x$, if $x \in n_s$ and $s\in Sorts(\Sigma)$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $h(make(t)) = h(t)$, otherwise;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \item $h(\iota(f)(t_1,..t_n))$ is defined iff $f(h(t_1), ..h(t_n))$ is defined in $n$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco and then $h(\iota(f)(t_1,..t_n)) = f(h(t_1), ..h(t_n))$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \end{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item for predicates in $\iota(\Sigma_M)$ we define
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco $\iota(p)(t_1,..t_n)$ iff $p(h(t_1),..,h(t_n))$.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoNotice that the first three types of axioms of the node $K$ hold by construction and also
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesconotice that $ker(h)$ satisfies $Th(M)$ because $n$ is a $M$-model.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe surjectivity of $h$ and the minimality of $ker(h)$ are exactly the
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco``no junk'' and the ``no confusion'' properties of the free model $n$.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoFor the other inclusion, let $n'$ be a model of $N'$, $n_0$ be its $\Sigma$-reduct and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$k'$ a $K$-expansion of $n'$.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoUsing the fact that the theory of $M$ is in Horn form, we get an expansion of $n_0$ to a
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$\sigma$-free model $n$. We have seen that all free models are also models of $N'$ and moreover
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowe have seen that $ker(k_h)$ is the least predicative congruence satisfying $Th(M)$. The free types
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoaxioms of $K$ fix the interpretation of $\iota(\Sigma_M)$ and therefore $ker(k'_h)$ and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco$ker(k_h)$ are both minimal on the same set, and must be the same. This and the surjectivity
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoof $k_h$ and $k'_h$ allow us to define easily
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoan isomorphism between $n$ and $n'$ and because $n'$ is isomorphic with a free model it must be free as well.