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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescois detailed in Section \ref{sec:free}), 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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescostudied in \cite{BouhoulaJouannaudMeseguer00} 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
f7f399037e1ad094f8373f609c687e847510fda1Adriá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.
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoThe summation 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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescothe information given in $R$ that will be used to label the link between
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescothe node standing for the module expression and the node importing it.
01f8490b545292b8e15df76c1e4095829a69d293Adrián Riesco\subsubsection{Importations}
01f8490b545292b8e15df76c1e4095829a69d293Adrián RiescoAs explained above, each Maude module generates two nodes in the development
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescowhen importing a module, we will select between these nodes 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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescoincluded one. We use 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.
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoAs seen in Section \ref{subsec:views}, a particular case of mapping
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescobetween operators is the mapping between
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescoterms, that has the general form $\verb"op" \; e \; \verb"to term" \; t$.
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%where $e$ is a term consisting of a
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%single operator applied to variables declared either on-the-fly or with
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%variable declarations in the same view and the target term is any term
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%with variables, those in the source $e$ in the corresponding sorts
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%resulting from the mapping.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoSince this shortcut allows to map operators with different profiles,
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescoin these cases it generates an auxiliary node with the signature of the
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescotarget specification extended by an extra operator of the appropriate arity;
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescothis node will be used as new target.
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.
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco\subsubsection{Development graph: An example\label{subsubsec:dg_ex}}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoWe illustrate how to build the development graph with an example. Consider
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescothe following Maude specification:
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}
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián RiescoEach module has generated a node with its name and
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoanother primed one that contains the initial model, while both of them
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián Riescoare linked with a non-persistent free link (in blue in the illustration). Note that
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián Riescotheory \verb"T" did not generate this primed node.
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián RiescoThe 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.
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián RiescoThere is a theorem link (red link in the figure) between \verb"T" and the
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián Riescofree (here, initial) model of
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco\verb"M". This link is labeled with the mapping defined in the view \verb"V",
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesconamely \verb"op _._ to _+_ .".
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián RiescoThe 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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescoby means of a non-persistent free link.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoIt is straightforward to show:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{theorem}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe translation of Maude modules into development graphs is
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescosemantics-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.\
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco``natural numbers are a total order.'' For example, we could prove
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescothe view \verb"V" above
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoWe 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}
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco \item $S^\#$ unites the sorts of $\Phi(\Sigma)$ and the set
5ac8592ed934697a4cd3d3bd5944ffa28277a1f3Adrián Riesco $\{[s] \mid s \in \mi{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}
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoM \ar@{=>}[rr]_{n.p.\mathit{free}}^{\sigma} \ar@{=>}[d]& & N \ar@{=>}[dd]\\
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoM'\ar@{=>}[d]^{\iota_N}& & \\
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoM''\ar@{=>}[r]_{\mathit{free}}^{\sigma^\#} & K \ar@{=>}[r]_{\mathit{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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco$\sigma:\Sigma\rightarrow \Sigma^N$ such that $\mathit{Th}(M)$ is in Horn
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoform, replace it with
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoM \ar@{=>}[r]^{\mathit{incl}} &
f7f399037e1ad094f8373f609c687e847510fda1Adrián RiescoK \ar@{=>}[r]^{\mathit{incl}}_{\mathit{hide}} &
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco}, where $N'$ has the same signature as $N$, $\mathit{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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco$h: \iota(s) \rightarrow? \, s$, for any sort $s$ of $\Sigma^M$
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco%(and $\to?$ indicating it is a partial function)
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescoand $\mathit{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
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescowith all operations as constructors, including $\mathit{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$$
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco\item a second-order formula saying that the kernel of $h$ ($\mathit{ker}(h)$)
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescois the least partial predicative congruence\footnote
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco{A \emph{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),$$
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco$\mathit{congruence}$ is the conjunction of
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,
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riescooperations $\iota(f)$ map terms $t_1, \ldots, t_n$ to the term
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco$\iota(f)(t_1, \ldots, 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}
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco \item $h(\mathit{make}(x)) = x$, if $x \in n_s$ and $s\in \mathit{Sorts}(\Sigma)$;
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco \item $h(\mathit{make}(t)) = h(t)$, otherwise;
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco \item $h(\iota(f)(t_1, \dots, t_n))$ is defined iff $f(h(t_1), \ldots, h(t_n))$
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco is defined in $n$
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco and then $h(\iota(f)(t_1, \ldots, t_n)) = f(h(t_1), \ldots, h(t_n))$;
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco \end{itemize}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\item for predicates in $\iota(\Sigma_M)$ we define
f7f399037e1ad094f8373f609c687e847510fda1Adrián Riesco $\iota(p)(t_1, \ldots, t_n)$ iff $p(h(t_1), \ldots, 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.