[CoFI] Comments on CASL v0.99 DRAFT

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

[The deadline for comments is hereby extended by one week, to:

  12 noon on WEDNESDAY 15 APRIL, 1998

 I'd originally hoped that the minutes of the Language Design meeting,
 summarizing the discussions and proposals from Lisbon, would have been
 sent to this list before the original deadline, but this has not
 happened.  Moreover, many of us have just started the Easter holidays
 - perhaps also with time to take one last look through the CASL design
 and formulate any "last wishes" for (minor) improvements?  

 The Semantics group is asked to accept my apologies for this further
 (but final!) delay with finalizing the CASL Language Summary.  --PDM]

Overall impression:
-------------------
really a nice and comprehensive document!

Comments to specific sections:
------------------------------

2.1.2, p.11, attributes, sentence above "Operation definitions"

A more liberal restriction was proposed in Lisbon.
A suggestion (following OBJ3) would be:
"The declaration enclosing an operation attribute
is ill-formed unless the axioms generated by the 
attribute (using the operation with the profile 
for which it is being declared) are well-formed."

But now I am not sure what the sorts of the variables 
in the axiom of

op __ ++ __ : List * NeList -> NeList assoc

would be:

forall x:List;y,z:NeList . x ++ (y ++ z) = (x ++ y) ++ z

is well-formed, while

forall x,y:List;z:NeList . x ++ (y ++ z) = (x ++ y) ++ z

is not.
I do not know what OBJ3 does here.

[I've mislaid my copy of "Introducing OBJ3" - could someone
 please check this detail and let me know?  --PDM]

Probably it is best to keep the old paragraph
(saying that both argument sorts and the result sort
must be equal).

2.1.5, p.16, sort generation

I assume that the extension of this on subsorts is the
following:
The injections and projections implicitly generated by 
subsort declarations (occurring among the SI_1, ... SI_n) 
also contribute to the set of operations that has to
generate the sorts.
(Note that in 2.1.5., only the *declared* operations
are mentioned, it is not entirely clear whether injections
and projections are part of these.
Further note that it makes a difference if only injections
or also projections are included - I sent examples showing this
to this list.)


Chapter 5, Structured specifications

I suggest to add something on institution indepedence, like:

"The structuring concepts and constructs and their semantics do not 
depend on a specific framework of basic specifications.
This means that Part I of the CASL language design is orthogonal
to Part II (and also Parts III and IV). 
Therefore, CASL basic specifications
as given in Part I can be restricted to sublanguages
or extended in various ways without the need to reconsider
or to change Parts II, III and IV -- and vice versa."

[Should there perhaps be something more explicit about 
 "institutions with syntax"? --PDM]

6.3, Views

I am in favour of the semantic treatment of the applicability
of views (as fitting arguments), as proposed by Andrzej.

[I.e., well-formedness of fitting views does not depend on the names
 of the parameter and target specifications involved, but only on
 their signatures. --PDM]

I think that this should be also combined with implicit
fitting views, as proposed in 6.3.2. The semantics would be
that there has to be a unique view in the global environment
sarisfying the static conditions (i.e. compatibility of signatures),
and moreover that is also satisfies the dynamic conditions
(i.e. model class inclusions).
Andrzej's argument against this was the following:
It may become complicated for readers of specifications
to check well-formedness of implicit fitting views, 
because they have to compute the source and target signatures 
of a lot of declared views before finding the right one 
(or realizing that there is none).
The main pro argument is the elegance of 
	LIST[LIST[NAT]]
opposed to
	LIST[LISTasEQ[NATasEQ]]
where both cases rely on the existence of 
a view LISTasEQ from EQ to LIST,
and a view NATasEQ from EQ to NAT.

[Moreover, the user's guide may still recommend to name parameter and
 argument specifications, to help identify the intended view.  Tools
 checking well-formedness will complain if there is more than one
 possible way of inserting an implicit fitting view.  --PDM]

8.3.1, Unit terms

In Lisbon, I proposed to have reductions along
non-injective signature morphisms, because they
may occur when there is the need to duplicate
a component of a given unit (say, an implementation
of natural numbers) and use it for two or more
components of some generic unit (say, graphs
with egdes and nodes, in order to obtain
a graph of the successor function. Pairs of elem1 and elem2
are another example, but here one could argue
that it is better to have one separate specification
for both elem1 and elem2).

Now it seems that this possibility is already there.

If I understand correctly, in the specification

arch spec Graph_of_increasing_discrete_time =
units
  N:NAT 
  Gr = lambda G:GRAPH . G
result
   Gr[NAT fit nodes |-> nat, edges |-> nat, 
              source |-> id, target |-> succ]
end

the symbols nodes, edges, source and target have to occur in GRAPH, 
whereas nat, id and succ have to occur in NAT.
That is, NAT is reduced along the symbol map to GRAPH,
and thereby the nat-component of NAT is duplicated
and used for both the nodes component and the egdes
component of the resulting UNIT-TERM.
(Practically, one might argue that GRAPH is too loose
to be implemented meaningfully in this way, but then
consider an extension of graph stating some more
properties of the graph of "increasing discrete time".)

If I have misunderstood the paragraph on Unit
Applications, then please formulate it more
precisely. And in this case, I would still
vote for allowing non-injective signature morphisms
in UNIT-REDUCTIONs.
I.e. the symbols right to |-> must be all distinct,
while those left to |-> need not to be.
This has a straightforward semantics: namely form
the signature morphism mapping each symbol right
to |-> to the corresponding symbol left to |->,
and take the reduct along it.
For uniformity reasons, the same should hold
also for REDUCTIONs in structured specs.


10.1.1 Local library names, 10.1.2 Library versions

As I have understood the outcome of a discussion with
Peter and others in Lisbon, we want to have arbitrary
URLs for LOCAL-LIB-IDs, since different sites might
jointly develop a still not registered library.
For VERSION, we would like to have sequences of numbers.
And I have promised to write a more detailed study
note on this (follows in the next couple of weeks).

10.2 Distributed libraries

The paragraph explaining the semantics is not correct,
since names of specifications cannot be replaced
with their definitions without changing the semantics.
So I would propose:
"The semantics corresponds to having included all the
downloaded definitions; ..."

[Note that one could obtain full referential transparency in CASL by
 adding to the language a construct

   SPEC ::=  ... | closed-spec SPEC

 whose semantics would be to give SPEC the empty local environment.
 A SPEC-DEFN could then implicitly involve this construct.  I'm not
 sure that there is any need for writing this construct explicitly,
 but it might be useful to have it there in the background.  The
 concrete syntax could be "closed SP".  Any objections?  --PDM]

C.5 Annotations

Annotations for conservative extensions are missing.

[Right, they were mentioned in Sect. 6.1.4 but I'd forgotten to add
 them to Sect C.5. --PDM]

I would further suggest to have "implies" and "implies
converts" annotations as in Larch, because stating
the intended consequences of a specification make
it more readable a help to communicate more of
the understanding what a specification should mean,
even if the intended consequences have not been
proven yet.

Also, for dealing with error algebras implementing
partial algebras, I would like to have an annotation
for equational conservative extension, where SP'
equationally conservatively extends SP if
for all SP-models M, there is an SP'-model M'
and an injection i:M->M'|_SP. A consequence
of this is the following:
SP' |= t1=t2 implies SP |= t1=t2
for t1,t2 terms in SP.
One possible use: the error algebra implementing
a partial algebra might add new data,
but should not introduce confusion.

[My proposal is simply to leave the set of annotations open.  Provided
 all annotations have a simple syntax, along the lines of that already
 given for label and display annotations, parsers may insert the
 annotations in the abstract syntax tree in a uniform way, and it is
 left to particular tools to process them further.  --PDM]

Appendix E, examples

Is there enough syntax around to specify things
like natural numbers, floating point numbers,
characters and strings in a usable way?
(No doubt that they can be specified in principle,
but the problem is that of a readable syntax.)
Shouldn't this be included in the examples?

[Bernd pointed out to me after the meetings in Lisbon that there is
 actually TOO MUCH syntax for this!  Currently, the concrete syntax
 allows WORDS to start with digits, so "12" can never be parsed as
 "(1)2" even after declaring "1" and "__2".  However, even if one
 restricts WORDS not to start with digits (and perhaps adds digits to
 SIGNS, so that "__+1" would become a valid ID) this doesn't help much
 with providing the conventional notation for characters and strings.

 A general solution may be to provide some standard specifications for
 numbers, characters, lists, and strings with verbose notation, e.g.,
 using the ISO Latin-1 names for characters.  Then "input annotations"
 (analogous to display annotations) would be provided to allow concise
 conventional concrete (input and display) lexical syntax for
 abbreviating the verbose terms.  If someone would like to volunteer
 for working this out in detail, please send a message to this
 mailing list!  Note that ASF+SDF already provides something similar,
 and may be an appropriate starting point.  --PDM]


One point of my going through other languages:
----------------------------------------------

Derived specification morphisms (OBJ3)

Pro argument: In a view, the definitional extensions of
the target specification need not be given explicitly 
(e.g. operation symbols may be mapped to terms).
Contra argument: The corresponding category is
not cocomplete - this is a strong contra argument.
But now ArrowLogic claims there is a cocomplete category 
of derived signature morphisms.
Does anyone know it? I will ask them.


Some typos:
-----------

6.3.1, fitting views
"og" ==> "of"

6.3.2, implicit fitting views
'[view VN[FA_1] ... [FA_n]'  the 2nd closing ']' is missing.


Greetings,
Till

[Many thanks for careful reading - and thinking!  BTW, I see that your
 message almost made the original deadline, having been sent shortly
 after midnight...  --PDM]