Extending

A weaker, yet substantial, requirement about a module importation is expressed by the keyword extending. Intuitively, the idea is to allow ``junk,'' but to rule out confusion. Extending importations may appear naturally in situations in which the data of some sort is extended with new data elements, yet not identifying previously defined data, like adding a new constant infinity to the natural numbers in a module importing NAT. As another example, when defining the semantics of a programming language in Maude, we can have from the beginning a sort Program, and define incrementally the syntax of programs in several modules, say, EXPRESSION, STATEMENT, PROCEDURE, and so on. This will typically give rise to a family of extending module importations as more syntax is added.

For functional modules $M'$ and $M$, where $M'$ has been imported as a submodule in extending mode, either by an explicit extending importation in $M$, or transitively through one of $M$'s submodules, if $(\Sigma',E' \cup A') \subseteq (\Sigma,E \cup A)$ is the theory inclusion defined by the module inclusion $M'\subseteq M$, the extending requirement means that for each sort $s'$ in $\Sigma'$ the function

$$q_{s'}: T_{\Sigma'/E' \cup A',s'} \longrightarrow T_{\Sigma/E \cup A,s'}$$

is injective. For system modules the extending requirement is interpreted exactly as before as far as their underlying equational theories are concerned. That is, if $Q$ extends $Q'$ and the associated theory inclusion is $(\Sigma',E' \cup A',\phi',R')\subseteq (\Sigma,E \cup A,\phi,R)$, then the equational theory inclusion $(\Sigma',E' \cup A') \subseteq (\Sigma,E \cup A)$ must be extending. We furthermore require that for any two ground $\Sigma'$-terms $t$ and $t'$ we can reach $t'$ from $t$ by a sequence of rewrites in the module $M'$ if and only if we can do so in the module $M$; that is, for ground terms in $M'$ the reachability relation is not altered by the supermodule.

Under the Church-Rosser and termination assumptions, the extending $(\Sigma',E' \cup A') \subseteq (\Sigma,E \cup A)$ requirement is a form of conservative extension requirement, in the sense that it implies that for any $\Sigma'$ ground terms $t$ and $t'$ that have a sort in $(\Sigma',E' \cup A')$, $E' \cup A'$ proves $t=t'$ if and only if $E\cup A$ proves $t=t'$. In addition, for system modules it further implies that for any two ground $\Sigma'$-terms $t$ and $t'$ the reachability relation is not altered by the extension. In summary, equality and reachability are conservatively preserved for ground terms.

Note that the extending relation does not destroy protecting importations further down the hierarchy. That is, if $M$ imports $M'$ in extending mode, but $M'$ imports $M''$ in protecting mode, then $M$ still imports $M''$ in protecting mode, not in extending mode. If we do not want $M$ to protect $M''$ (because this is indeed violated), then we have to say so by explicitly giving an extending importation declaration for $M''$ in $M$.