8 \subsection{Creating the development graph}
14 Each Maude module generates two nodes in the development
15 graph. The first one contains the theory equipped with the usual
17 to the first one with a free definition link (whose signature morphism
18 is detailed in Section \ref{sec:free}), contains the same signature but
19 no local axioms and stands for the free models of the theory.
24 consists of free extensions of the models of their parameters, that are
33 Maude module expressions allow to combine and modify the information
39 When the module expression is a simple identifier the development
43 The summation of the module expressions $\mathit{ME}_1$ and
44 $\mathit{ME}_2$ generates a new node in the development graph
46 the union of the information in both summands. A definition link
47 is also created between the original expressions and the resulting one.
51 the information given in $R$ that will be used to label the link between
52 the node standing for the module expression and the node importing it.
58 As explained above, each Maude module generates two nodes in the development
60 when importing a module, we will select between these nodes depending on the
66 the current node and the node standing for the free semantics of the
67 included one. We use the same links for the parameters in
71 The \verb"extending" mode generates a global link with the annotation
77 The \verb"including" mode generates a global definition link between the
78 current node  and the node standing for the loose semantics of the
85 as target. All the sorts and the operators declared in the source theory
86 have to be mapped to sorts and operators in the target.
89 between operators is the mapping between
90 terms, that has the general form $\verb"op" \; e \; \verb"to term" \; t$.
92 %single operator applied to variables declared either on-the-fly or with
93 %variable declarations in the same view and the target term is any term
94 %with variables, those in the source $e$ in the corresponding sorts
95 %resulting from the mapping.
97 in these cases it generates an auxiliary node with the signature of the
98 target specification extended by an extra operator of the appropriate arity;
102 link between the theory and the module satisfying it.
104 the ones stated in the views, see Section \ref{subsec:adv_feat} for details:
108 Sorts and labels are qualified by the parameter name in order to distinguish
109 different labels/sorts with the same name defined in different theories. Thus,
110 the mapping indicated by the view (more specifically, the source sorts) is
111 modified depending on the name of the parameter.
114 As explained in the Section \ref{subsec:pmod}, parameterized modules can
115 define parameterized sorts, that is, sorts that use the parameters as part of
116 the sort name and hence they are modified by the mapping in the view.
117 Moreover, when the target of a view is a theory the identifiers of these sorts
118 are extended with the name of the view and the name of the new parameter.
120 Thus, the sort morphism is extended with these new renamings.
129 We illustrate how to build the development graph with an example. Consider
130 the following Maude specification:
158 \noindent \Hets builds the graph shown in Figure \ref{fig:dg},
159 where the following steps take place:
163 another primed one that contains the initial model, while both of them
164 are linked with a non-persistent free link (in blue in the illustration). Note that
168 The summation expression has created a new node that includes the theories
169 of \verb"M1" and \verb"M2", importing the latter with a renaming; this new
170 node, since it is imported in \verb"extending" mode, uses a link with the
174 There is a theorem link (red link in the figure) between \verb"T" and the
176 \verb"M". This link is labeled with the mapping defined in the view \verb"V",
180 The parameterized module \verb"M3" includes the theory of its parameter
181 with a renaming, that qualifies the sort. Note that these nodes are connected
191 Once the development graph is built, we can apply the (logic
196 the view \verb"V" above
199 We show in the next
200 section how we deal with the freeness constraints imposed by free 
207 freeness is, as mentioned, different from the one used in \CASL in
208 that the free extensions of models are required to be persistent
209 only on sorts and new error elements can be added on the
210 interpretation of kinds. Attempts to design the translation to \CASL
214 \CASL.  In order not to break the development graph calculus, we need
218 appropriately, such that the parameter is always explicitly included
219 in the free extension.
222 an extension $\Sigma^\# = (S^\#, \leq^\#, F^\#, P^\#)$ of the
227  \item $S^\#$ unites the sorts of $\Phi(\Sigma)$ and the set 
230  \item $\leq^\#$ extends the subsort relation $\leq$ with pairs
233  \item $F^\#$ adds the function symbols $\{f:[w] \rightarrow [s]\}$ for all
236  \item $P^\#$ adds the predicate symbol $rew$ on all new sorts.
240 $\sigma: \Sigma \rightarrow \Sigma'$ be the morphism labeling it.%
246  \sigma^{op}(f)$ and this is correct because the operation symbols were
252 $\sigma:\Sigma\rightarrow \Sigma_N$, we first take the translation of the nodes
254 $\Sigma^\#_N$, a global definition link from $M'$ to $M''$ labeled with the 
257 $\sigma^\#$ and a hiding definition link from $K$ to $N'$ labeled with the
272 Notice that the models of $N$ are Maude reducts of \CASL models of $K$, 
273 reduced along the inclusion $\iota_N$. 
276 The idea is to use then a transformation specific to the second-order 
279 it mimics the quotient term algebra construction,
280 that is, the free model is specified as the homomorphic image
283 We are going to make use of the following known facts \cite{Reichel87}:
304 }, where $N'$ has the same signature as $N$, $\mathit{incl}$ denotes inclusions and 
305 the node $K$ is constructed as follows. 
307 The signature $\Sigma^K$ consists of the signature $\Sigma^M$ disjointly 
309 (let us denote $\iota(x)$ the corresponding symbol in this copy for each
310 symbol $x$ from the signature $\Sigma^M$) and augmented with new operations 
313 and $\mathit{make}_s:s\rightarrow \iota(s)$, for any sort $s$ of the source
314 signature $\Sigma$ of the morphism $\sigma$  labelling the free definition link.
316 The axioms $\psi^K$ of the node $K$ consist of:
321 sentences imposing the bijectivity of \textit{make};
323 \item axiomatization of the sorts in $\iota(\Sigma_M)$ as free types
324 with all operations as constructors, including $\mathit{make}$ for the sorts
338 \item a second-order formula saying that the kernel of $h$ ($\mathit{ker}(h)$)
339 is the least partial predicative congruence\footnote
344 for the binary relation and one predicate symbol for each relation symbol
363 $\mathit{congruence}$ is the conjunction of
384 denotes the simultaneous substitution of $sy'_i$ for $sy_i$ in
385 all formulas of $\Psi$ (while possibly instantiating the meta-variables
401 The models of the nodes $N$ and $N'$ are
402 the same.
411 Let us define the following $\Sigma_K$ model, denoted $k$:
417 \item on $\iota(\Sigma_M)$, the interpretation of sorts and function symbols 
418 is given by the free types axioms (i.e. sorts are interpreted as set of terms, 
419 operations $\iota(f)$ map terms $t_1, \ldots, t_n$ to the term
422 \item $make$ assigns to each $x$ the term $make(x)$;
424 \item the homomorphism $h$ is defined inductively as follows:
442 Notice that the first three types of axioms of the node $K$ hold by construction and also
444 The surjectivity of $h$ and the minimality of $ker(h)$ are exactly the
445 ``no junk'' and the ``no confusion'' properties of the free model $n$.  
447 For the other inclusion, let $n'$ be a model of $N'$, $n_0$ be its $\Sigma$-reduct and
449 Using the fact that the theory of $M$ is in Horn form, we get an expansion of $n_0$ to a
451 we have seen that $ker(k_h)$ is the least predicative congruence satisfying $Th(M)$. The free types 
452 axioms of $K$ fix the interpretation of $\iota(\Sigma_M)$ and therefore $ker(k'_h)$ and
453 $ker(k_h)$ are both minimal on the same set, and must be the same. This and the surjectivity

Indexes created Tue Jul 24 14:28:13 CEST 2018