dg.tex revision 6294ad597249a611c59e0dbf122ca9b89e679ba8
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.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Parameterized modules}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoAs we have seen in Section \ref{subsec:pmod}, parameterized modules
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoreceive a list of parameters $P_i$ each one associated to a module
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoexpression $M_i$. Since these module expressions are theories, they
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocan have sorts that are not instantiated yet, so to avoid clash of
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesconames these sorts are qualified with the parameter name. These
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoqualifications induce an implicit morphism in the definition links
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoof the development graph between the theory and the parameterized
de29004099dfbf647d6f25aa78a81e5524ebe4ddAdrián Riesco\subsection{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}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The 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
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe union of the information in both expressions. A definition link
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescois also created between the original expressions and the resulting one.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The renaming expression $\mathit{ME} * (R)$ creates a morphism with
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe information given in $R$ that will be used in the link
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item The instantiation module expression\footnote{This module expression
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocannot be used in Core Maude in all places where the rest of expressions
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescocan be used, for more information see \cite{maude-book}} assigns a view
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoor a parameter to each of the
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoNote that an instantiation generates some implicit morphisms and modifies
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescothe ones stated in the views:
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\begin{itemize}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item When the parameter is instantiated with a view
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item As explained in the previous section, parameterized modules can
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescodefine sorts of the form \verb"name{X1, ..., Xn}", where \verb"X1, ..., Xn"
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoare parameter names that can be instantiated or bound by new parameters.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoThus, in addition to the morphism
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\item When the module expression is a simple identifier the development
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescograph remains unchanged.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco\subsection{Importations}
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoEach Maude module generates two nodes in the development
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescograph. The first one contains the theory equipped with the usual
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoloose semantics. The second one, linked
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoto the first one with a free definition link (whose signature morphism
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescois detailed below), contains the same signature but
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescono local axioms and stands for the free models of the theory.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoNote that Maude theories only generate one node, since their initial
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescosemantics is not used by Maude specifications.
c2b9205d94467085f8b07c294c86493d55427074Adriá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
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
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe summation module expression generates a new node that includes all
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe information in its summands. Note that this new node can also need
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoa node with its free model if it is imported in protecting mode.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\subsection{Views}\label{subsec:dg_views}
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoMaude views have a theory as source and either a module or a theory
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoas target. All the sorts and operators declared in the source theory
c1cf2f634a37116ff90e99ca710179a23115cbfbAdriá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
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riescoterms, that has the general form \emph{op $e$ 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,
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoSignature morphisms are produced in different ways; explicitly,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescorenaming of module expressions and views lead to signature
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescomorphisms; however, implicitly we also find other morphisms:
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe sorts defined in the theories are qualified
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowith the parameter in order to distinguish sorts with the same name that
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowill be instantiated later by different ones; moreover, sorts defined
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco(not imported) in parameterized modules can be parameterized as well,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoso when the theory is instantiated with a view these sorts are also
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescorenamed (e.g. the sort \verb"List{X}" for generic lists can become
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\verb"List{Nat}").
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe model class of parameterized modules
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoconsists of free extensions of the models of their parameters, that are
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescopersistent on sorts, but not on kinds. This notion of freeness has been
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescostudied in \cite{BouhoulaJM00} under assumptions like existence of top sorts for kinds
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoand sorted variables in formulas; our results hold under similar
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescohypotheses. Thus,
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescowe use the same non-persistent free links described for protecting
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoimportation to link these modules with their corresponding theories.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco% In order not to break the calculus, we
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%need a way to normalize them. The idea is to replace them with a semantically
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%equivalent development graph in CASL, as follows.
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%a global definition link to
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%of their parameters. In this case, the above free definition link is
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%decorated with the inclusion signature morphism from the parameter
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%signature to the module's signature (while in the unparameterized
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco%case, the parameter signature is taken to be empty).
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoViews do not generate nodes in the development graph but theorem links
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescobetween the node corresponding to the source theory and the node with
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescothe free model of the target. However, Maude views
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoprovide a special kind of mapping between terms, that can in general
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescomap functions of different arity. When this mapping is used we generate
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoa new inner node extending the signature of the target to include functions
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoof the adequate arity.
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}}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\noindent \Hets builds the graph shown in Fig. \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]$
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco is defined to be $[x_1] \ldots [x_n]$.}
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.
c2b9205d94467085f8b07c294c86493d55427074Adrián RiescoThe normalization of Maude freeness is then illustrated in Fig.\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
c2b9205d94467085f8b07c294c86493d55427074Adrián Riescoinclusion $\iota_N$.\footnote{The arrows without labels in Fig.\ref{nf}
6294ad597249a611c59e0dbf122ca9b89e679ba8Adrián Riescocorrespond to heterogeneous links from Maude to \CASL.}
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco\begin{wrapfigure}[12]{r}[0cm]{3.5cm}
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 Riesco\end{wrapfigure}
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.