UNIT-TERM ::= UNIT-REDUCTION | UNIT-TRANSLATION | AMALGAMATION | LOCAL-UNIT | UNIT-APPL
Unit terms provide counterparts to most of the constructs of structured specifications: translations, reductions, amalgamations (corresponding to unions), local unit definitions, and applications (corresponding to instantiations).
Unit terms use the same notation as structured specifications--but with a crucially different semantics, however. This is easiest to notice when considering the difference between union and amalgamation as well as between translation and unit translation. For units, static semantics requires that enough sharing is ensured so that the constructs as applied to the given units will always make sense and produce results. This is in contrast with the constructs for structured specifications, where union and (non-injective) translation might introduce inconsistencies.
Taking the unit type of each unit name from its declaration, the unit term must be well-typed. All the constructs involved must get argument units over the appropriate signatures.