19 no local axioms and stands for the free models of the theory.
23 The model class of parameterized modules
24 consists of free extensions of the models of their parameters, that are
25 persistent on sorts, but not on kinds. This notion of freeness has been 
26 studied in \cite{BouhoulaJouannaudMeseguer00} under assumptions like existence of top sorts for kinds
43 The summation of the module expressions $\mathit{ME}_1$ and
46 the union of the information in both summands. A definition link
66 the current node and the node standing for the free semantics of the
78 current node  and the node standing for the loose semantics of the
88 As seen in Section \ref{subsec:views}, a particular case of mapping
91 %where $e$ is a term consisting of a 
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;
111 modified depending on the name of the parameter.
115 define parameterized sorts, that is, sorts that use the parameters as part of
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.
163 another primed one that contains the initial model, while both of them
169 of \verb"M1" and \verb"M2", importing the latter with a renaming; this new
175 free (here, initial) model of
180 The parameterized module \verb"M3" includes the theory of its parameter
182 by means of a non-persistent free link.
187 The translation of Maude modules into development graphs is
203 \subsection{Normalization of free definition links}
206 Maude uses initial and free semantics intensively. The semantics of
208 that the free extensions of models are required to be persistent
210 interpretation of kinds. Attempts to design the translation to \CASL
213 introduce a special type of links to represent Maude's freeness in
222 an extension $\Sigma^\# = (S^\#, \leq^\#, F^\#, P^\#)$ of the
223 translation $\Phi(\Sigma)$ of $\Sigma$ to \CASL as follows:
227  \item $S^\#$ unites the sorts of $\Phi(\Sigma)$ and the set 
250 The normalization of Maude freeness is then illustrated in Figure \ref{nf}.
252 $\sigma:\Sigma\rightarrow \Sigma_N$, we first take the translation of the nodes
255 inclusion $\iota_N$ of $\Sigma_N$ in $\Sigma^\#_N$, a free definition link from 
269 \caption{Normalization of Maude free links}\label{nf}
272 Notice that the models of $N$ are Maude reducts of \CASL models of $K$, 
277 extension of \CASL to normalize freeness. 
281 of an absolutely free model (i.e.\ term model).
283 We are going to make use of the following known facts \cite{Reichel87}:
287 Extensions of theories in Horn form admit free extensions of models.
293 Extensions of theories in Horn form are monomorphic.
307 The signature $\Sigma^K$ consists of the signature $\Sigma^M$ disjointly 
308 united with a copy of $\Sigma^M$, denoted $\iota(\Sigma_M)$ which makes all function symbols total 
311 $h: \iota(s) \rightarrow? \, s$, for any sort $s$ of $\Sigma^M$
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
334 \item surjectivity of homomorphisms:
338 \item a second-order formula saying that the kernel of $h$ ($\mathit{ker}(h)$)
340 {A \emph{partial predicative congruence} consists of a symmetric 
342 of appropriate type for each predicate symbol.} satisfying
363 $\mathit{congruence}$ is the conjunction of
383 where, for a set of formulas $\Psi$, $\Psi[sy_1/sy'_1;\ldots ;sy_n/sy'_n]$
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
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, 
420 $\iota(f)(t_1, \ldots, t_n)$).  We define interpretation of predicates after defining $h$;
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
448 $k'$ a $K$-expansion of $n'$.
449 Using the fact that the theory of $M$ is in Horn form, we get an expansion of $n_0$ to a
450 $\sigma$-free model $n$. We have seen that all free models are also models of $N'$ and moreover
452 axioms of $K$ fix the interpretation of $\iota(\Sigma_M)$ and therefore $ker(k'_h)$ and
454 of $k_h$ and $k'_h$ allow us to define easily

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