CASL - Symbol maps with default mechanism

[Till Mossakowski <till@tzi.de>]

Dear friends,

while writing [more precisely: polishing  --PDM] both the semantics and
the basic datatypes, we have found a little problem with the semantics
of symbol maps within fitting morphisms.  Consider the following
specification that is a minimized form of a specification from the
basic datatypes:

spec Nat =
  sort Nat
  ops 1,2:Nat;
  min : Nat*Nat->Nat
end

spec Array[ops min,max:Nat] given Nat =
{} %% further stuff
end 

spec EFPN =
Array[Nat fit min |-> 1, max |-> 2]
end

Currently, the above instantiation of Array becomes illegal, since 
min |-> 1 leads to a symbol mapping that maps both min:Nat from the
formal parameter and min:Nat*Nat->Nat from the import to 1:Nat.  Of
course, this does not even give a signature morphism.

[Qualifying min as min:Nat would avoid any possibility of unintended
 mapping of imported symbols - but being required to insert such
 qualifications would surely be quite annoying.  --PDM]

Thus, we have some, in my view undesirable, interaction of the fitting
map with the rule that the import is implicitly mapped identically.

My suggestion is therefore to implement a default mechanism:
unqualified symbols in a symbol map only affect symbols that are not
explicitly mapped by a fully qualified symbol (or by the import
mechanism).  Here is a proposal for the change of wording in
Sect. 6.4.2 in a future release of the CASL Summary:

  SYi |-> SY'i denotes the map that takes the symbol SYi to the symbol
  SY'i. The mapped symbols in the list must be distinct. Overloaded
  operation symbols and predicate symbols may be disambiguated by
  explicit qualification; when SYi is not qualified, the effect is as
  if all (sort, operation, or predicate) symbols declared with the
! name SYi in the current environment (other than those explicitly
! mapped as fully qualified symbols) are mapped uniformly to SY'i.

The previous wording of the last two lines was:

  same name in the current environment are mapped uniformly
  to SY'i. 

This slight change would make the above instantiation correct, and
generally would ensure that unqualified symbol maps cannot interact
with the imports.

[As far as I know, there was never any intention in the CASL design
 to allow unqualified symbol maps to affect imports.  The proposed
 change to the wording in the Summary should help to clarify the
 intended interpretation of unqualified symbol maps - which is
 however a bit more subtle than previously thought.  --PDM]

Please send any objections to this proposal to this list before

		END OF AUGUST, 2001

Greetings,
Till

[In the absence of objections, this issue will be regarded as settled,
 and the proposed wording incorporated in a future release of the CASL
 Summary.  --PDM]