REDUCTION ::= reduction SPEC RESTRICTION ! RESTRICTION ::= HIDE | REVEAL
A reduction is written:
SP Rwhere the restriction R determines a set of symbols, and possibly a mapping of them.
It is well-formed when the set of symbols determined by R is a subset of the symbols declared in the signature Sigma of SP.
When R is a hide construct, the reduction determines the largest sub-signature of Sigma that does not contain these symbols (note that hiding a sort entails hiding all the operations and predicate symbols whose profiles involve that sort).
In the case that R is a reveal construct, the reduction determines the smallest sub-signature of Sigma that does contain the indicated symbols (so 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 the determined model class is given by the reducts of the models of SP along the inclusion of the sub-signature determined by the restriction. A reduction must not affect the symbols already declared in the local environment, which is passed unchanged to SP.
When a reveal construct determines a mapping of some of the revealed symbols, the corresponding translation is applied to the resulting reducts.
! HIDE ::= hide SYMB-ITEMS+
A hide construct is written:
hide SY_1, ..., SY_nKeywords indicating the syntactic categories of the following symbols may be inserted in the list, as for the translation constructs.
It determines the set of symbols { SY_1, ..., SY_n}, to be hidden by the restriction.
! REVEAL ::= reveal SYMB-OR-MAP-ITEMS+ ! SYMB-OR-MAP-ITEMS::= symb-or-map-items SYMB-KIND SYMB-OR-MAP+ ! SYMB-OR-MAP ::= SYMB | SYMB-MAP
A reveal construct may be written:
reveal SY_1, ..., SY_nSome or all of the revealed symbols SYi may be simultaneously renamed to symbols SY'i, by writing ` SY_i |-> SY'_i'. Keywords indicating the syntactic categories of the following symbols may be inserted in the list, as for the translation and hiding constructs.
The reveal construct determines the set of symbols { SY_1, ..., SY_n}, to be revealed by the restriction, together with any specified mappings of SYi to SY'i.