Specifications may be named by definitions and collected in libraries. In the context of a library, the (re)use of a specification may be replaced by a reference to it through its name. The current association between names and the specifications that they reference is called the global environment; it may vary throughout a library, e.g., with linear visibility the global environment for a named specification is determined exclusively by the definitions that precede it.
With referential transparency, a reference to a named specification may always be replaced by a copy of the specification itself. Thus in principle, all references to names could be eliminated from the specifications in a library--provided that there are no mutual or cyclic chains of references, i.e., the library can be linearized.
The local environment given to each named specification in a library should be independent of the other specifications in the library. This allows the well-formedness of each named specification to be independent of the references made to it.
[DTS] I don't understand the last sentence.
Discharged: Delete it.A library may be located at a particular site on the Internet, and addressed by a URL (uniform resource locator). Each library may incorporate the downloading of named specifications from other libraries, which takes place whenever the library is used.
The semantics of a specification library is a map taking each specification name defined in it to the semantics of that specification. The initial global environment for the library is determined by the semantics of any downloaded specifications.