Re: [CoFI] Proposal for named morphisms in CASL

[tarlecki@mimuw.edu.pl]

[Below is Andrzej's immediate reaction to my original message: when he
sent it to me, he hadn't seen my resume of the background for the
proposal, nor my sketch of a rationale for it.  The same goes for the
reactions from Bernd and Till, appended.  BTW, I hope that I didn't
misrepresent Didier's "very basic proposal" from Note L-6 in my
message - if I did, I hope he'll react and put things straight... 
--PDM]

Dear Peter,

Again, with apologies for the lack of any earlier reaction from me. I
haven't seen any reply from the others, so let me try now.

First, I think that Hubert and Till should have a quick look at the
proposal for the named morphisms, as they have done most of the work
on (the semantics of) symbol morphisms and their role in structured
specs so far --- and probably will have to cope with the new proposal
in their semantics. Hence the CC to them; I will also forward your
message to them in a minute. I hope you do not mind.

Second, it is a pity we did not have time to at least briefly discuss
this in Bremen. I must say that I have some doubts about the proposal
now, and it is possible that it would be trivial to clear them out then.

The basic doubt is that I am not sure what really should be introduced
into the language as named entities:

1) symbol maps (SYMB-MAP*)

2) specification morphisms (with indicated source and target specs)

3) signature morphisms (with indicated source and target signatures)

I think that the current proposal goes for 2, and least at the
surface.  But then I have a number of semantic doubts: it seems that
it would be logical to check whether the specification morphisms when
used to transform a specification (e.g. as a fitting morphisms, or as
a morphism used in translation) is "semantically applicable", that is,
whether the source or target specification of the morphism is a
(semantic) subspecification of the one we transform. I do not think
that this is the intention here.

In addition, I do not like (if I understand this at all) the use of a
VIEW as a fitting argument without any actual parameter specification
(which I guess then implicitly is given as the target of the view).
This seems like another, quite different use of the specification
morphism, which to me feels like going against the basic intuitions we
put into CASL.

[However, it seems to be the *only* use of named morphisms in OBJ3!
Is there really such a conflict between CASL intuitions and OBJ3
intuitions?  If so, it certainly wasn't intended!!  -PDM]

This last possibility would not be an option if we dealt with named
signature morphisms only. Since we do not have any syntactic category
for signatures in the language, in the definition it still could
appear to go between specs, but they would be implicitly coerced to
their underlying signatures only.

In both cases though it is not clear to me if and how we can use the
morphisms as fitting morphisms in instantiations of generics. The
trick is that we should still extend them somehow to other (larger)
signatures and specs there, allowing for non-trivial things like
generalisation to compound identifiers. It feels wrong to do this with
"closed entities" declared to work on given specifications and
signatures only. Of course: this is "do-able", but only after viewing
these morphisms as symbols maps (which they "underneath" are).

[I'm afraid that the IFIP referees who asked for named morphisms to be
added to the language would be a bit disappointed by the above - how
would we explain it to them? --PDM]

************************************************************************
MY PROPOSAL
************************************************************************
So, I guess, my proposal would be to admit from the very beginning
that we introduce only a *very limited* potential for naming
morphisms, by allowing the user to name symbol maps. Then they could
be used in any place a symbol map could be used, and moreover could be
extended by some other symbol maps (a possibility which does not seem
to be allowed by the current proposal).  

[But is that possibility likely to be useful in practice? - sorry, I
know very little about such methodological aspects!  Is it perhaps
already found in some existing language?  --PDM]

This would simply mean that we could add to CASL something that amounts
to the following (ad hoc names and notation, of course):

SYMB-MAPPING-DEFN  ::= symbols-mapping SYMB-MAPPING-NAME SYMB-MAPPING
SYMB-MAPPING       ::= SYMB-MAPPING-NAME 
                     | symb-maps (SYMB-MAP | SYMB-MAPPING)*

and use SYMB-MAPPING wherever SYMB-MAP* (or SYMB-MAP+) was used
before.
************************************************************************

I should also admit that I do not understand the following statement
from your message: it is just not clear to me how this differs (if at
all) from what we currently do when using symb maps).

> The semantics is intended to allow the insertion of a unique defined
> view between the PARAM and ARG specs, and the abbreviation of views by
> omitting SYMB-MAPs that are uniquely determined (e.g., when the larger
> spec only has one candidate op of a particular profile). 

[SYMB-MAPs are extended to signature morphisms in CASL only by letting
them be identity on symbols that are not explicitly mapped, I think.
The extra generality of the proposal is that if one only has one sort
in the target signature, or only one operation or predicate of a
particular profile, then also a non-identity mapping for symbols is
regarded as uniquely determined.  So if NAT has only one sort, the
unique view from {sort Elem} to NAT can be defined without mentioning
any explicit symbols at all - e.g. "view E_N from ELEM to NAT".
I'm not sure how often this is useful in practice; OBJ3 relies also on
the notion of the "principal sort" of a specification, and the default
is to map a single sort to that, I believe.  Would someone who is
properly familiar with views in OBJ3 kindly clarify the pragmatics
here?  --PDM]

Aha: no, I do not see any need for any special view-of-units
concept. This is given by the corresponding signature morphism, and so
any of the above could be used. Although, of course, using a
specification morphism to reduce a unit outside the semantics of the
target specification would stretch the flexibility of the language a
bit.  Still, this is not much different form using a view to transform
any specification, so yes, I would allow also:

FITTING-ARG-UNIT ::=  ... | fitting-arg-unit UNIT-TERM VIEW-NAME

(but of course, no, no, no to
	FITTING-ARG-UNIT ::=  ... | fitting-arg-unit VIEW-NAME
).

Best regards,

Andrzej

==============================================================================

[Bernd's immediate reaction to the proposal was as follows - before
seeing Andrzej's message above.  --PDM]

Abstract Syntax; Views
----------------------

I am a little lost w.r.t. views. I thought the only thing necessary is
an abbreviation for SYMB-MAP*, i.e.
	VIEW-DEFN	::=	view-defn VIEW-NAME SYMB-MAP*
You will have to help me understand the reasoning why there are TWO
cases of SPEC (looks heavy). The question is, maybe, whether we
abbreviate the morphism or the result of its application, together with
it; I thought it was the former.

More technically: there may be the need for a constructor for VIEW-NAME
in FITTING-ARG, e.g.
	FITTING-ARG	::=	FITTING-SPEC | SPEC-VIEW
	SPEC-VIEW	::= spec-view SPEC? VIEW-NAME
or better avoiding the option by an extra alternative.

best regards
Bernd

==============================================================================

[Finally, Till's reactions. --PDM]

Dear Peter,

concerning named morphisms, I support Andrzej's proposal.
I just want to add that actual parameter specifications
may be fragments relative to the local environment,
and morphisms for these fragments are called "signature
extension morphisms" in the semantics. These are reflected
best by symbol mappings (and not by signature or 
specification morphisms) in the language.

Greetings,
Till

[I'm wondering whether the generality of using fragments as actual
parameters is likely to be exploited in practice... but maybe there
were other reasons to base the semantics on sig extension morphisms? 
--PDM]