[AT] This also implies, I think, that SIG-MORPHs (and perhaps RESTRICTIONs) must work not on complete signatures but rather on signature fragments. Moreover, well-formedness of a SPEC (as an extension) relative to the local environment it extends must be determined "from the outside", "top-down". For instance,

enrich sort s
by ( (fun f: s' -> s')
     translated by s' mapsto s )

would be a well-formed, closed specification in spite of the fact that the sort s' is never declared. Or we might impose some ad hoc looking extra closure conditions for specifications to which translations and reductions apply. For reductions, consider:

enrich sort s, const a: s
by ( hide a in (const b:s) )

I guess this should be ill-formed? Or is it okay (that is, hiding applies to the local environment extended by the given specification as well as to the specification itself)? I vote for ill-formedness here. But how do we make this work in some precise way? I guess we will have to use some ad hoc transformations of the local environment "against a SIG-MORPH" for translations.

Discharged: Adjust wording. We are working on signature fragments but translation etc. isn't allowed to affect the part of the signature that is being extended. The first example is ill-formed because we go one stage at a time, and f: s' -> s' uses s' which has not been declared. The second example is ill-formed since a comes from the signature being extended.

[AT] To what extent is re-declaration in specifications of the stuff already present in the local environment allowed? For instance, is

enrich sort s
by sort s

allowed? The analogy with union suggests that it should be allowed, the analogy with a sequence of basic items suggests that it should not be allowed.

Discharged: Re-declaration is allowed; it is now also allowed for basic specifications.

6.1.1 Translations and Reductions

TRANSLATION     ::=   translation SPEC SIG-MORPH

A translation is well-formed when the signature morphism construct
SIG-MORPH expands to a signature morphism applicable to the signature of the component specification SPEC. The translation determines the signature obtained by applying the signature morphism, and the class of models consisting exactly of those models whose reducts along the morphism are among those of SPEC.

SIG-MORPH       ::=   sig-morph SYMB-MAP*
SYMB-MAP        ::=   SORT-MAP | FUN-SYMB-MAP | PRED-SYMB-MAP
SORT-MAP        ::=   sort-map SORT SORT
FUN-SYMB-MAP    ::=   fun-symb-map FUN-SYMB FUN-SYMB
PRED-SYMB-MAP   ::=   pred-symb-map PRED-SYMB PRED-SYMB

A signature morphism construct SIG-MORPH expands to a signature morphism applicable to a particular signature when each first component of a map in the list SYMB-MAP* is a symbol from that signature. Moreover, the union of the maps has to yield a function. Overloaded function symbols FUN-SYMB and predicate symbols PRED-SYMB may be disambiguated by explicit types; when no explicit type is given in a first component of a map SYMB-MAP, all function or predicate symbols with the same name are mapped uniformly.

REDUCTION       ::=   reduction RESTRICTION SPEC 
RESTRICTION     ::=   restriction EXPOSURE SYMB+
EXPOSURE        ::=   hiding | revealing
SYMB            ::=   SORT | FUN-SYMB | PRED-SYMB

A REDUCTION is well-formed when the set of symbols determined by the RESTRICTION is a subset of the symbols declared in the signature of the component specification SPEC. In the case that the specified EXPOSURE is hiding, it determines the largest sub-signature of the signature of the component specification that does not contain these symbols (note that removing a sort entails removing all the functions and predicate symbols whose declared type involves that sort). In the case that the EXPOSURE is revealing, it determines the smallest sub-signature that does contain the indicated symbols (so revealing a function or predicate symbol entails revealing the sorts involved in its declared type). In both cases, the subsort embedding relation is inherited from that declared by SPEC, and the determined class of models is given by the reducts of the models of the component specification SPEC along the inclusion of the sub-signature determined by the RESTRICTION.

6.1.2 Unions and Extensions

UNION           ::=   union SPEC+

A UNION of several specifications abbreviates their joint (non-persistent) extension by an empty specification. The signature is obtained by the ordinary union of the signatures of each SPEC (not the disjoint union).

[DTS] So if a sort/function/predicate symbol appears in more than one SPEC, all are regarded as referring to the same thing, rather than to possibly different things that happen to accidentally have the same name.

Discharged: Adjust wording.

The models are those whose reduct along each of the signature inclusion morphisms is a model of the respective SPEC.

EXTENSION       ::=   extension OF-SPEC* SPEC
OF-SPEC         ::=   PERSISTENT-SPEC | SPEC
PERSISTENT-SPEC ::=   persistent-spec SPEC

An EXTENSION allows the extension of the union of some specifications with further signature and sentences.

[TM] UNIONs are defined in terms of extensions, and EXTENSIONs are defined in terms of unions. How is this cycle resolved? (Delete the first sentence explaining UNIONs.)

Discharged: Adjust wording.

For each PERSISTENT-SPEC used as an OF-SPEC, the reducts of the models of the EXTENSION along the corresponding signature inclusion must give the same class of models as that determined by the SPEC of the PERSISTENT-SPEC, otherwise the EXTENSION is deemed to be inconsistent.

[AT] What exactly does persistency mean here, when even an EXTENSION may itself be an extension? For instance:

enrich const a: int
by (enrich persistently const b: int
    by axiom a = 5)

I would say that this is inconsistent, although in some sense the declaration of b is not affected. I have not checked, but there may also be a difference whether we view persistency pointwise w.r.t. the models of the local environment for the EXTENSION (for each model of the local environment, the class of its extensions to the models of OF-SPEC is persistently extended to the models of SPEC) or for all models of the local environment together.

Discharged: We should perhaps speak of protection rather than persistency, since once a specification has been protected once it should remain protected for subsequent extensions as well. The example is forbidden, since "persistency" on b implicitly protects a as well -- the OF-SPEC* part is implicitly fed into the "leaves" of the SPEC part.

All the OF-SPECs in an EXTENSION get the current local environment; the component SPEC gets moreover all the symbols declared by the OF-SPECs.

[HB] So the OF-SPECs determine a local environment for SPEC. Then SPEC has to be given a semantics w.r.t. a local environment. For a BASIC-SPEC one assumes a non-empty initial local environment. However, what is the semantics of the specification building operations (e.g., REDUCTION, TRANSLATION, EXTENSION) w.r.t. to a given local environment? Does the local environment contribute to the argument or to the result of, e.g., TRANSLATION?

Discharged: These things can't modify the local environment.

FREE-SPEC       ::=   free-spec SPEC

By using a FREE-SPEC as the component SPEC of an EXTENSION, the class of models is that given by the free extension. When a FREE-SPEC is used other than in an extension, it abbreviates the free extension of an empty OF-SPEC list, which restricts the models to the initial models of the component specification.

[AT] Every SPEC is an extension, adopting the above view. So, a FREE-SPEC is always the class of free extensions of the models of the current local environment to the models of the SPEC component of the FREE-SPEC.

Discharged: This is correct.

---

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk