Study Note HO extensions; Questions on V1.0 draft

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

[Dear Friends,

the study note L-10
         Subsorted Partial Higher-order Logic  as an extension of CASL
has been installed. The note should be a base for discussions at the
Cachan meeting.
	http://www.brics.dk/Projects/CoFI/Notes.html, then announce it on

Furthermore, two questions from Till:
- Sharing in unit terms,
- Semantics of fitting maps
 (BKB)]

------------------------------------------------------

Dear all,

concerning unit terms in architectural specifications,
I have the following comment to 1.0 draft:

The outcome of a discussion between Maura, Andrzej and
me was that sharing of symbols in unit terms has to
be understood with the overloading relation (with some
technical complicated details).
Therefore, I suggest to replace "identity" and "same
symbol" by "shared symbol" in 8.3.1.1. and the last
sentence of 8.3.1.5.
Probably it also makes sense to state in 8.3.1. that
sharing is related to the overloading relation.

A possible wording might be:
Any sharing of symbols in a unit-term must be supported
by a sharing of symbols in a common unit.
(Leaving the details of "supported by" unspecified here).

Greetings,
Till

------------------------------------------------------

Dear all,

I have some questions concerning implicit fitting morphisms.
The current reading in the summary is (end of section 5):

Given another signature Sigma', a mapping of symbols in
|Sigma| to symbols in |Sigma'| determines the set of
all morphisms from Sigma to Sigma' that both extend
the given mapping, and are identity on common symbols of
Sigma and Sigma', other than those already in the
domain of the mapping.  (Mapping an operation or
predicate symbol implies mapping the sorts in the profile
consistently.)

My first question is: should't this be modified as follows:

..., and are *as much as possible* the identity on
common symbols ...

At least, that would be what I have understood from the recent
discussion on views.

Consider the following example

spec FORMAL = sorts Elem
 ops nil:Elem

spec ACTUAL = sorts List
 ops nil:List

The fitting map nil:Elem |-> nil (may be
abbreviated by nil |-> nil) would be legal here,
and imply that Elem is mapped to List (since mapping
an operation symbol implies mapping the sorts
in the profile consistently).
The empty fitting map would be illegal, since the
induced sort mapping is not the identity. However,
it is the identity *as much as possible*. So with the
new formulation, the empty fitting map would be o.k.
It would even be o.k. in (example from Andrzej)

spec FORMAL = sorts s,t
 ops a:t, f:s->s

spec ACTUAL = sorts s,t
 ops b:s, g:t->t

In a mail from 10 Sept., Andrzej suggested to allow this.


My second question is:
Consider

spec FORMAL = sorts s,t
 ops f:s, f:t->t

spec ACTUAL = sorts s,t
 ops g:s, f:t->t

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.


For those who are intereseted in technical details,
here is the corresponding semantics of the
"as much as possible" version of the paragraph in section 5:

Let signatures Sigma, Sigma' and a symbol map h be given.
For a set of symbols SYs and a signature morphism
sigma:Sigma->Sigma', say that (SYs,sigma) fits h iff
      (h \cup ID_SYs) \subseteq graph(|sigma|)

Now h determines the set of all signature morphisms
sigma:Sigma->Sigma' such that there is some SYs with
 1) (SYs,sigma) fits h
 2) SYs is maximal with the property that
        for some theta, (SYs,theta) fits h

Greetings,
Till