FREE-SPEC ::= free-spec SPEC
A free specification FREE-SPEC is written:
free { SP }Note that the specification written:
free types DD1; ... DDn;is parsed as a free datatype of a basic specification, but it usually has the same interpretation as the free structured specification written:
free { types DD1; ... DDn; }This equivalence holds at least in the framework for basic specifications given in Part I, under some minor restrictions: in a datatype declaration with more than one alternative, any selector that is declared as total for some alternative must be declared as a total selector with the same result sort for every other alternative; and the sorts and qualified operation symbols declared by the datatype declaration must not be already declared in the local environment.
When the current local environment is empty, SP must determine a complete signature Sigma; otherwise, it must determine an extension from the local environment to a complete signature Sigma. In both cases, Sigma is the signature determined by the free specification.
When the current local environment is empty, the free specification determines the class of initial models of SP; otherwise, it determines the class of models that are free extensions for SP of their own reducts to models of the current local environment.