Re: More comments on 1.0

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,

here a quick reply to your reactions (leaving out everything I agree
with).

>> Is the fitting map f |-> g illegal?
>> I would say yes, because it expands to
>> f:s |-> g:s, f:t->t |-> g:t->t, which does not work.
>> This assumes that symbol maps get their qualification
>> only in dependency of the source signature (otherwise,
>> the semantics would be more complicated).
>>
>> In any case, f:s |-> g would be o.k.

>I see now that v1.0-DRAFT says:
>
>  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 that

>  all operation or predicate symbols with the same name are mapped
>  uniformly to SY'i.
>
>Would you like to propose a wording consistent with your answer to the
>above question?
>
>BTW, I think that an analogous comment about overloading should be
>added 6.4.1, since hiding or revealing an unqualified overloaded
>symbol presumably affects all its qualifications too?

Yes. I think the right place to state this is at the end of 6.4.1 and
6.4.2.
I suggested a wording in my comments about institution independence:

  I therefore suggest to change the last paragraph in section 6.4.1:
  "The list determines a set of qualified symbols, obtained
  from the listed symbols by using qualification information
  of a given signature..."
  (Similarly for 6.4.2)
  The signature is either the local environment signature
  or the source signature of the signature morphism.

>> p.42, 6.2.1
>> Perhaps swap "imports" with "paramemters" because this order
>> is also used in the syntax?
>
>I need a decision on whether to revert to the v0.99 order or not!

I did not at all want to revert the order in the language, but just
revert
the order in the explanation text in the summary to make it consistent
with the language. But this is not really important...

>> Editorial comments/typos
>> ------------------------
>> ...
>> p. C-7/C-8
>> What is the precedence of TOKEN __ ... __ TOKEN ?
>
>Does it need one?

I do not know - we did not implement mixfix parsing in Bremen yet.

Greetings,
Till