REDUCTION ::= reduction SPEC RESTRICTION
RESTRICTION ::= HIDE | REVEAL
HIDE ::= hide SYMB-ITEMS+
REVEAL ::= reveal SYMB-MAP-ITEMS+
A hiding reduction is written:
SP hide SLA revealing reduction is written:
SP reveal SMSymbol lists SL and symbol mappings SM are described in Section 6.4.
The symbols listed by SL, or mapped by SM, must be among those declared by SP.
In the case of a hiding reduction, the signature Sigma given by SP and the set of symbols listed by SL determine the inclusion of the largest subsignature Sigma' of Sigma that does not contain any of the listed symbols, as explained in Chapter 5. Note that hiding a sort entails hiding all the operations and predicate symbols whose profiles involve that sort.
In the case of a revealing reduction, the signature Sigma given by SP and the set of symbols mapped by SM determine the inclusion of the smallest subsignature Sigma' of Sigma that contains all of the listed symbols, as explained in Chapter 5. Note that revealing an operation or predicate symbol entails revealing the sorts involved in its profile.
In both cases, the subsort embedding relation is inherited from that declared by SP, and a model class M is given by the reducts of the models of SP along the inclusion of Sigma' in Sigma.
In the case of a hiding reduction, its model class is simply M. In the case of a revealing reduction, however, the signature Sigma' and the mapping SM of (all) the symbols in it determine a signature morphism to a signature Sigma", as explained in Chapter 5. The class of models of the reduction then consists exactly of those models over Sigma" whose reducts along this morphism are in M.
A reduction must not affect the symbols already declared in the local environment, which is passed unchanged to SP.