%!TEX root = main.tex
We describe in this section how Maude structuring mechanisms
described in Section \ref{sec:maude}
are translated into development graphs. Then, we explain how these development
graphs are normalized to deal with freeness constraints.
\subsection{Creating the development graph}
We describe here how Maude modules, theories, and views are translated into
development graphs, illustrating it with an example.
\subsubsection{Modules}
Each Maude module generates two nodes in the development
graph. The first one contains the theory equipped with the usual
loose semantics. The second one, linked
to the first one with a free definition link (whose signature morphism
is detailed in Section \ref{sec:free}), contains the same signature but
no local axioms and stands for the free models of the theory.
Note that Maude theories only generate one node, since their initial
semantics is not used by Maude specifications.
The model class of parameterized modules
consists of free extensions of the models of their parameters, that are
persistent on sorts, but not on kinds. This notion of freeness has been
studied in \cite{BouhoulaJouannaudMeseguer00} under assumptions like existence of top sorts for kinds
and sorted variables in formulas; our results hold under similar
hypotheses. We use non-persistent free links to link these modules with
their corresponding theories.
\subsubsection{Module expressions}\label{subsec:me}
Maude module expressions allow to combine and modify the information
contained in Maude modules:
\begin{itemize}
\item
When the module expression is a simple identifier the development
graph remains unchanged.
\item
The summation of the module expressions $\mathit{ME}_1$ and
$\mathit{ME}_2$ generates a new node in the development graph
$(\mathit{ME}_1 + \mathit{ME}_2)$ with
the union of the information in both summands. A definition link
is also created between the original expressions and the resulting one.
\item
The renaming expression $\mathit{ME} * (R)$ creates a morphism with
the information given in $R$ that will be used to label the link between
the node standing for the module expression and the node importing it.
\end{itemize}
\subsubsection{Importations}
As explained above, each Maude module generates two nodes in the development
graph;
when importing a module, we will select between these nodes depending on the
chosen importation mode:
\begin{itemize}
\item
The \verb"protecting" mode generates a non-persistent free link between
the current node and the node standing for the free semantics of the
included one. We use the same links for the parameters in
parameterized modules.
\item
The \verb"extending" mode generates a global link with the annotation
\textsf{PCons?}, that stands for proof-theoretic conservativity and that
can be checked with a special conservativity checker that is
integrated into \Hets.
\item
The \verb"including" mode generates a global definition link between the
current node and the node standing for the loose semantics of the
included one.
\end{itemize}
\subsubsection{Views}\label{subsec:dg_views}
Maude views have a theory as source and either a module or a theory
as target. All the sorts and the operators declared in the source theory
have to be mapped to sorts and operators in the target.
As seen in Section \ref{subsec:views}, a particular case of mapping
between operators is the mapping between
terms, that has the general form $\verb"op" \; e \; \verb"to term" \; t$.
%where $e$ is a term consisting of a
%single operator applied to variables declared either on-the-fly or with
%variable declarations in the same view and the target term is any term
%with variables, those in the source $e$ in the corresponding sorts
%resulting from the mapping.
Since this shortcut allows to map operators with different profiles,
in these cases it generates an auxiliary node with the signature of the
target specification extended by an extra operator of the appropriate arity;
this node will be used as new target.
Views generate a theorem
link between the theory and the module satisfying it.
Note that an instantiation generates some implicit morphisms and modifies
the ones stated in the views, see Section \ref{subsec:adv_feat} for details:
\begin{itemize}
\item
Sorts and labels are qualified by the parameter name in order to distinguish
different labels/sorts with the same name defined in different theories. Thus,
the mapping indicated by the view (more specifically, the source sorts) is
modified depending on the name of the parameter.
\item
As explained in the Section \ref{subsec:pmod}, parameterized modules can
define parameterized sorts, that is, sorts that use the parameters as part of
the sort name and hence they are modified by the mapping in the view.
Moreover, when the target of a view is a theory the identifiers of these sorts
are extended with the name of the view and the name of the new parameter.
%
Thus, the sort morphism is extended with these new renamings.
\end{itemize}
%%%%%% PAPER
\subsubsection{Development graph: An example\label{subsubsec:dg_ex}}
We illustrate how to build the development graph with an example. Consider
the following Maude specification:
{\codesize
\begin{verbatim}
fmod M1 is fmod M2 is
sort S1 . sort S2 .
op _+_ : S1 S1 -> S1 [comm] . endfm
endfm
th T is mod M3{X :: T} is
sort S1 . sort S4 .
op _._ : S1 S1 -> S1 . endm
eq V1:S1 . V2:S1 = V2:S1 . V1:S1 [nonexec] .
endth
mod M is view V from T to M is
ex M1 + M2 * (sort S2 to S) . op _._ to _+_ .
endm endv
\end{verbatim}
}
\begin{figure}[t]
\begin{center}
\includegraphics[scale=.47]{dg}
\caption{Development Graph for Maude Specifications\label{fig:dg}}
\end{center}
\end{figure}
\noindent \Hets builds the graph shown in Figure \ref{fig:dg},
where the following steps take place:
\begin{itemize}
\item
Each module has generated a node with its name and
another primed one that contains the initial model, while both of them
are linked with a non-persistent free link (in blue in the illustration). Note that
theory \verb"T" did not generate this primed node.
\item
The summation expression has created a new node that includes the theories
of \verb"M1" and \verb"M2", importing the latter with a renaming; this new
node, since it is imported in \verb"extending" mode, uses a link with the
\textsf{PCons?} annotation.
\item
There is a theorem link (red link in the figure) between \verb"T" and the
free (here, initial) model of
\verb"M". This link is labeled with the mapping defined in the view \verb"V",
namely \verb"op _._ to _+_ .".
\item
The parameterized module \verb"M3" includes the theory of its parameter
with a renaming, that qualifies the sort. Note that these nodes are connected
by means of a non-persistent free link.
\end{itemize}
It is straightforward to show:
\begin{theorem}
The translation of Maude modules into development graphs is
semantics-preserving.
\end{theorem}
Once the development graph is built, we can apply the (logic
independent) calculus rules that reduce global theorem links to local
theorem links, which are in turn discharged by local theorem proving
\cite{MAH-05-a}. This can be used to prove Maude views, like e.g.\
``natural numbers are a total order.'' For example, we could prove
the view \verb"V" above
We show in the next
section how we deal with the freeness constraints imposed by free
definition links.
\subsection{Normalization of free definition links}
\label{sec:free}
Maude uses initial and free semantics intensively. The semantics of
freeness is, as mentioned, different from the one used in \CASL in
that the free extensions of models are required to be persistent
only on sorts and new error elements can be added on the
interpretation of kinds. Attempts to design the translation to \CASL
in such a way that Maude free links would be translated to usual free
definition links in \CASL have been unsuccessful. We decided thus to
introduce a special type of links to represent Maude's freeness in
\CASL. In order not to break the development graph calculus, we need
a way to normalize them. The idea is to replace them with a
semantically equivalent development graph in \CASL. The main idea is
to make a free extension persistent by duplicating parameter sorts
appropriately, such that the parameter is always explicitly included
in the free extension.
For any Maude signature $\Sigma$, let us define
an extension $\Sigma^\# = (S^\#, \leq^\#, F^\#, P^\#)$ of the
translation $\Phi(\Sigma)$ of $\Sigma$ to \CASL as follows:
\begin{itemize}
\item $S^\#$ unites the sorts of $\Phi(\Sigma)$ and the set
$\{[s] \mid s \in \mi{Sorts}(\Sigma)\}$;
\item $\leq^\#$ extends the subsort relation $\leq$ with pairs
$(s, [s])$ for each sort $s$ and $([s],[s'])$ for any sorts $s \leq s'$;
\item $F^\#$ adds the function symbols $\{f:[w] \rightarrow [s]\}$ for all
function symbols on sorts $f:w \rightarrow s $;\footnote{$[x_1 \ldots x_n]$
is defined to be $[x_1] \ldots [x_n]$.} and
\item $P^\#$ adds the predicate symbol $rew$ on all new sorts.
\end{itemize}
Now, we consider a Maude non-persistent free definition link and let
$\sigma: \Sigma \rightarrow \Sigma'$ be the morphism labeling it.%
\footnote{In Maude, this would usually be an injective renaming.}
We define a \CASL signature morphism
$\sigma^\# : \Phi(\Sigma) \rightarrow \Sigma'^\#$: on sorts,
$\sigma^\#(s) := \sigma^{sort}(s)$ and $\sigma^\#([s]):=[\sigma^{sort}(s)]$;
on operation symbols, we can define $\sigma^ \#(f) :=
\sigma^{op}(f)$ and this is correct because the operation symbols were
introduced in $\Sigma'^\#$; $rew$ is mapped identically.
The normalization of Maude freeness is then illustrated in Figure \ref{nf}.
Given a free non-persistent definition link $\flinka{M}{\sigma}{N}$, with
$\sigma:\Sigma\rightarrow \Sigma_N$, we first take the translation of the nodes
to \CASL (nodes $M'$ and $N'$) and then introduce a new node, $K$, labeled with
$\Sigma^\#_N$, a global definition link from $M'$ to $M''$ labeled with the
inclusion $\iota_N$ of $\Sigma_N$ in $\Sigma^\#_N$, a free definition link from
$M''$ to $K$ labeled with
$\sigma^\#$ and a hiding definition link from $K$ to $N'$ labeled with the
inclusion $\iota_N$.\footnote{The arrows without labels in Figure \ref{nf}
correspond to heterogeneous links from Maude to \CASL.}
\begin{figure}
$$
\xymatrix{
M \ar@{=>}[rr]_{n.p.\mathit{free}}^{\sigma} \ar@{=>}[d]& & N \ar@{=>}[dd]\\
M'\ar@{=>}[d]^{\iota_N}& & \\
M''\ar@{=>}[r]_{\mathit{free}}^{\sigma^\#} & K \ar@{=>}[r]_{\mathit{hide}}^{\iota_n} & N'
}
$$
\caption{Normalization of Maude free links}\label{nf}
\end{figure}
Notice that the models of $N$ are Maude reducts of \CASL models of $K$,
reduced along the inclusion $\iota_N$.
The next step is to eliminate \CASL free definition links.
The idea is to use then a transformation specific to the second-order
extension of \CASL to normalize freeness.
The intuition behind this construction is that
it mimics the quotient term algebra construction,
that is, the free model is specified as the homomorphic image
of an absolutely free model (i.e.\ term model).
We are going to make use of the following known facts \cite{Reichel87}:
\begin{fact}
Extensions of theories in Horn form admit free extensions of models.
\end{fact}
\begin{fact}
Extensions of theories in Horn form are monomorphic.
\end{fact}
Given a free definition link $\flinka{M}{\sigma}{N}$, with
$\sigma:\Sigma\rightarrow \Sigma^N$ such that $\mathit{Th}(M)$ is in Horn
form, replace it with
\xymatrix{
M \ar@{=>}[r]^{\mathit{incl}} &
K \ar@{=>}[r]^{\mathit{incl}}_{\mathit{hide}} &
N'
}, where $N'$ has the same signature as $N$, $\mathit{incl}$ denotes inclusions and
the node $K$ is constructed as follows.
The signature $\Sigma^K$ consists of the signature $\Sigma^M$ disjointly
united with a copy of $\Sigma^M$, denoted $\iota(\Sigma_M)$ which makes all function symbols total
(let us denote $\iota(x)$ the corresponding symbol in this copy for each
symbol $x$ from the signature $\Sigma^M$) and augmented with new operations
$h: \iota(s) \rightarrow? \, s$, for any sort $s$ of $\Sigma^M$
%(and $\to?$ indicating it is a partial function)
and $\mathit{make}_s:s\rightarrow \iota(s)$, for any sort $s$ of the source
signature $\Sigma$ of the morphism $\sigma$ labelling the free definition link.
The axioms $\psi^K$ of the node $K$ consist of:
\begin{itemize}
\item
sentences imposing the bijectivity of \textit{make};
\item axiomatization of the sorts in $\iota(\Sigma_M)$ as free types
with all operations as constructors, including $\mathit{make}$ for the sorts
in $\iota(\Sigma)$;
\item homomorphism conditions for $h$:
$$ h(\iota(f)(x_1, \dots, x_n)) = f(h(x_1), \dots, h(x_n)) $$
and
$$\iota(p)(t_1, \dots, t_n) \Rightarrow p(h(t_1), \dots, h(t_n))$$
\item surjectivity of homomorphisms:
$$\forall y : s . \exists x:\iota(s) . h(x) \EEQ y$$
\item a second-order formula saying that the kernel of $h$ ($\mathit{ker}(h)$)
is the least partial predicative congruence\footnote
{A \emph{partial predicative congruence} consists of a symmetric
and transitive binary relation for each sort and a relation
of appropriate type for each predicate symbol.} satisfying
$Th(M)$. This is done by quantifying over a predicate symbol for each sort
for the binary relation and one predicate symbol for each relation symbol
as follows:
$$\begin{array}{l}
\forall \{P_s : \iota(s), \iota(s)\}_{s \in Sorts(\Sigma_M)} ,
\{P_{p:w} : \iota(w)\} _{p:w \in \Sigma_M} \\
.~
\mathit{symmetry}
\land \mathit{transitivity}
\land \mathit{congruence}
\land \mathit{satThM}
\implies \mathit{largerThenKerH}
\end{array}
$$
where $\mathit{symmetry}$ stands for
$$\bigwedge_{s\in Sorts(\Sigma^M)} \forall x:{\iota(s)},y:{\iota(s)}.P_s(x,y)\implies P_s(y, x),$$
$\mathit{transitivity}$ stands for
$$\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),$$
$\mathit{congruence}$ is the conjunction of
$$
\begin{array}{l}
\bigwedge_{f_{w\rightarrow s}\in\Sigma^M} \forall x_1\ldots x_n:{\iota(w)},y_1\ldots y_n:{\iota(w)}\,.\,\,\\
D(\iota(f_{w,s})(\bar{x}))\land D(\iota(f_{w,s})(\bar{y}))\land P_w(\bar{x},\bar{y})
\implies P_s(\iota(f_{w,s})(\bar{x}),\iota(f_{w,s})(\bar{y}))
\end{array}
$$
and
$$
\begin{array}{l}
\bigwedge_{p_w \in\Sigma^M} \forall x_1\ldots x_n:{\iota(w)},y_1\ldots y_n:{\iota(w)}\,.\,\,\\
D(\iota(f_{w,s})(\bar{x}))\land D(\iota(f_{w,s})(\bar{y}))\land P_w(\bar{x},\bar{y})
\implies P_{p:w}(\bar{x}) \Leftrightarrow P_{p:w}(\bar{y})
\end{array}
$$
\noindent where $D$ indicates definedness. $\mathit{satThM}$ stands for
denotes the simultaneous substitution of $sy'_i$ for $sy_i$ in
all formulas of $\Psi$ (while possibly instantiating the meta-variables
$t$ and $u$).
%
Finally $\mathit{largerThenKerH}$ stands for
$$\begin{array}{l}
\bigwedge_{s\in Sorts(\Sigma^M)} \forall x:{\iota(s)},y:{\iota(s)}.h(x)\EEQ h(y)\implies P_s(x, y)\\
\bigwedge \land_{p_w\in\Sigma^M} \forall \bar{x}:{\iota(w)}.\iota(p:w)(\bar{x})
\implies P_{p:w}(\bar{x})
\end{array}
$$
\end{itemize}
\begin{proposition}
The models of the nodes $N$ and $N'$ are
the same.
\end{proposition}%\ednote{AR: Proof in appendix?}
{\noindent\it Proof.}
%
Let $n$ be a $N$-model. To prove that $n$ is also a $N'$-model,
we need to show that it has a $K$-expansion.
Let us define the following $\Sigma_K$ model, denoted $k$:
\begin{itemize}
\item on $\Sigma_M$, $k$ coincides with $n$;
\item on $\iota(\Sigma_M)$, the interpretation of sorts and function symbols
is given by the free types axioms (i.e. sorts are interpreted as set of terms,
operations $\iota(f)$ map terms $t_1, \ldots, t_n$ to the term
$\iota(f)(t_1, \ldots, t_n)$). We define interpretation of predicates after defining $h$;
\item $make$ assigns to each $x$ the term $make(x)$;
\item the homomorphism $h$ is defined inductively as follows:
\begin{itemize}
\item $h(\mathit{make}(x)) = x$, if $x \in n_s$ and $s\in \mathit{Sorts}(\Sigma)$;
\item $h(\mathit{make}(t)) = h(t)$, otherwise;
\item $h(\iota(f)(t_1, \dots, t_n))$ is defined iff $f(h(t_1), \ldots, h(t_n))$
is defined in $n$
and then $h(\iota(f)(t_1, \ldots, t_n)) = f(h(t_1), \ldots, h(t_n))$;
\end{itemize}
\item for predicates in $\iota(\Sigma_M)$ we define
$\iota(p)(t_1, \ldots, t_n)$ iff $p(h(t_1), \ldots, h(t_n))$.
\end{itemize}
Notice that the first three types of axioms of the node $K$ hold by construction and also
notice that $ker(h)$ satisfies $Th(M)$ because $n$ is a $M$-model.
The surjectivity of $h$ and the minimality of $ker(h)$ are exactly the
``no junk'' and the ``no confusion'' properties of the free model $n$.
For the other inclusion, let $n'$ be a model of $N'$, $n_0$ be its $\Sigma$-reduct and
$k'$ a $K$-expansion of $n'$.
Using the fact that the theory of $M$ is in Horn form, we get an expansion of $n_0$ to a
$\sigma$-free model $n$. We have seen that all free models are also models of $N'$ and moreover
we have seen that $ker(k_h)$ is the least predicative congruence satisfying $Th(M)$. The free types
axioms of $K$ fix the interpretation of $\iota(\Sigma_M)$ and therefore $ker(k'_h)$ and
$ker(k_h)$ are both minimal on the same set, and must be the same. This and the surjectivity
of $k_h$ and $k'_h$ allow us to define easily
an isomorphism between $n$ and $n'$ and because $n'$ is isomorphic with a free model it must be free as well.
\qed