Including

The most general form of module importation is provided by the including keyword. No requirements are made in an including importation about maps of the form $q_{s'}$: there can now be junk (lack of surjectivity) and/or confusion (lack of injectivity). Likewise, for system modules it is not anymore required that the reachability relation between ground terms in the submodule is preserved. The including keyword does however impose some requirements. First of all, there is the requirement that the equational attributes of subsort-overloaded operators must be the same. Furthermore, the including relation does not destroy protecting or extending importations further down the hierarchy. That is, if $M$ imports $M'$ in including mode, but $M'$ imports $M''$ in protecting (resp. extending) mode, then $M$ still imports $M''$ in protecting (resp. extending) mode, not in including mode. If we do not want $M$ to protect or extend $M''$ (because this is indeed violated), then we have to say so by explicitly giving an including importation declaration for $M''$ in $M$.

Given that, as already mentioned, there is no difference at runtime between the different modes of importation because the Maude system does not check the corresponding requirements, from a pragmatic point of view, when a user is doubtful about the appropriate importation mode, the best idea is to use the including mode so that at least no false assertion is made.