TRANSLATION ::= translation SPEC RENAMING
RENAMING ::= renaming SYMB-MAP-ITEMS+
A translation is written:
SP with SMSymbol mappings SM are described in Section 6.4.
The symbols mapped by SM must be among those declared by SP. The signature Sigma given by SP and the mapping SM then determine a signature morphism to a signature Sigma', as explained in Chapter 5. The morphism must not affect the symbols already declared in the local environment, which is passed unchanged to SP.
The class of models of the translation consists exactly of those models over Sigma' whose reducts along the morphism are models of SP.
When the symbol mapping SM is simply a list of identity maps (which may be abbreviated to a simple list of symbols) the only effect of the translation on the semantics of SP is to require that the symbols listed are indeed included in the signature given by SP, otherwise the translation is not well-formed.