Comments on Language Summary (version 0.9, 0.91)

[pdmosses@brics.dk]

COMMENTS on Summary of the CoFI Tentative Language Design
- versions 0.9, 0.91

Edited by Peter D. Mosses <pdmosses@brics.dk>

Contributors (thanks!):

AT>  From: tarlecki@mimuw.edu.pl (Andrzej Tarlecki) (re v0.91)
BKB> From: bkb@Informatik.Uni-Bremen.DE (Bernd Krieg-Brueckner) (re v0.91)
DB>  From: "Didier Bert" <Didier.Bert@imag.fr> (re v0.9)
ES>  From: Erik Saaman <erik@cs.rug.nl> (re v0.9)
PC>  From: Pietro Cenciarelli <pietro@cs.rug.nl> (re v0.91)
>    From: Peter D. Mosses <pdmosses@brics.dk>

The comments have been collated according to the primary section
addressed, and I've added an indication of my reactions.

In any replies to this message, please do not cite more of it than
strictly necessary.

ES> - Have you considered the name CoLa (Common Language). It can be nicely
ES> prefixed for different extensions/restrictions (CoCA CoLa, PEpSi CoLa?)

It was mentioned by several people at the Dagstuhl seminar (incl. the
chairman of IFIP WG 14.3!) that we should be sure to have the word
"Algebraic" in the name/acronym of our language - hence the "Alcol"
suggestion... 

BKB> I do not like ALCOL at all; Ground-CoFI could be OK but does not convey
BKB> the "narrow waist" - middle level idea; I still like Black CoFI (seriously)
BKB> Please omit ALCOL from the body of the document as it may manifest itself
BKB> to early.

OK, changed to "X" (hoping that nobody would like it as the name... :-)

*** 1. Basic concepts:
 
AT> I do not like the use of the term "logic" for the proof or inference
AT> system; for me the "logic" covers the model theory as well...  And in
AT> the part about the logic, I would add that the inference is expected
AT> to be preserved under translation of sentences as well, although at
AT> the moment it is not essential (sicne we do not deal with inference at
AT> all).

Changed to "proof system" - OK?

AT> PC> (6,14) - (page,line)
AT> PC> Why are signatures of basic specifications required to be finite?
AT> PC> In this way it's not legal to assume, say, a constant for each natural
AT> PC> number. Many common metalanguages for denotational semantics feature 
AT> PC> families of operations indexed by infinite sets of indices, e.g.
AT> PC> fixed point operators in LCF. Similarly for predicates, e.g. equality.
AT> PC> Is this situation uncommon in formal specification?
AT> 
AT> I think we could allow infinite signatures without any pain. However,
AT> this would not necessarily mean that they would be user-definable,
AT> since I do not think we would like to design a special syntax now for
AT> declarations of infinite sets of operations etc. This was the reason
AT> why I did not made this point myself. What Pietro rightly points out
AT> though is that some of the built-in specifications may have infinite
AT> number of constants. On the other hand, in all cases which come to my
AT> mind, these infinitely many constants might be viewed just as convenient
AT> shorthands for some ground terms.
AT> 
AT> Things like equality (and fixpoint operators, if we had any) do not
AT> lead to a need for infinitary signatures, as far as I can see: in our
AT> view they are not part of the signature of anything, but are
AT> constructors of syntactic phrases of appropriate kinds. In this way,
AT> they are available for any sort (perhaps of some required form) but
AT> are not part of individual signatures.

The "(finite)" has been removed.

AT> PC> (6,15)
AT> PC> Why are the axioms of basic specifications required to be finite?
AT> PC> This means that axiom schemes are not permitted, e.g. Scott induction
AT> PC> on any (inductive) formula.
AT> 
AT> I guess he would like to allow axiom schemata in basic specs. This is
AT> possible, of course, but then we would have to worry about exact
AT> syntax for definition of such schemata. They would have to be
AT> different from sentences, of course, and have some variables ranging
AT> over syntax of the language, I guess. Don, Bpb Harper and me tried to
AT> play with these things some years ago, but nothing terribly exciting
AT> was coming out of this anyway. An extension?
AT> 
AT> The role of various induction schemata is taken over in teh language
AT> by (generating) constraints. Of course, soem proof-theorey would have
AT> to provide and cope with them still.

The "(finite)" has been removed.

AT> PC> (6,22)
AT> PC> "Satisfaction is required to be preserved by translation." Does the
AT> PC> term "preserve" indicate the following if-and-only-if `satisfaction'
AT> PC> condition?
AT> 
AT> PC> 	   For all signature morphisms f: S -> S',
AT> PC> 	   for all sentence A in Sen(S) and model M in Mod(S')
AT> PC> 
AT> PC> 		   M |= Sen(f)(A)  iff  Mod(f)(M) |= A.
AT> 
AT> Yes, I also understood this as the satisfaction condition for the
AT> underlying institution.

I haven't added the formal statement - should I?

AT> PC> Two comments:
AT> 
AT> PC> 1. For most doctrines in categorical logic, e.g. for all formal
AT> PC> languages whose models are described by finite limit theories, functors
AT> PC> of the form Mod(f): Mod(S') -> Mod(S), obtained contravariantly from
AT> PC> translations f: S -> S', have left adjoints. I suspect this state of
AT> PC> affairs is described precisely by the satisfaction condition above.
AT> PC> It would be interesting to understand if a universal property indeed
AT> PC> links Sen(f) and Mod(f) in the institution for the common language,
AT> PC> that is if, for all morphisms f there is a *unique* functor Mod(f)
AT> PC> satisfying the condition.
AT> 
AT> That is, whether the satisfaction condition determines the reduct
AT> functor (up to iso)? No, i do not think this is true. The satisfaction
AT> condition deteremines the reduct functor up to logical equivalence of
AT> the models. In general, i can see no way to strengthen this. However,
AT> if one considers a more detailed structure of sentences, as e.g. in
AT> parchments, where term evaluation is taken into account, then perhaps
AT> some more properties follow. Even then though I would be surprised if
AT> the reducts were determined unambigously, since there may be funny
AT> things happening on parts of the models that cannot be named by
AT> syntactic entities. There may be somthing interesting to be said here
AT> for models that are reachable, but then things may become easy since
AT> logical equivalence (w.r.t. just ground equations in teh standard
AT> case) plus reachability assumption identifies algebras up to iso.
AT> 
AT> PC> 2. Maybe it would be more general to distinguish between signature
AT> PC> morphisms and translations, the first mapping symbols to symbols and
AT> PC> the second mapping sentences to sentences. Of course, any signature
AT> PC> morphism induces a translation. However, for various logics, but also
AT> PC> in universal algebra, there are interesting translations which do not
AT> PC> arise from signature morphisms, e.g. mapping primitive to derived
AT> PC> operations when proving the equivalence of algebraic theories. If
AT> PC> the notion of translation is restricted to maps of the form Sen(f),
AT> PC> the duality (a la Gabriel-Ulmer) relating translations and functors
AT> PC> between categories of models (e.g. varieties for algebraic theories)
AT> PC> fails.
AT> 
AT> Yes, of course, there are interesting and important notions of
AT> signature morphism that are more general than just symbol-to-symbol
AT> mappings. For me, the essence of a signature morphism is that it
AT> induces translations of sentences and of models so that teh
AT> satisfaction condition holds. However, arbitrary translations between
AT> syntax of sentences do not seem sufficient for our purposes, since we
AT> (at least, I) want to base the semantics of the langauge on model
AT> theory.
AT> 
AT> In several places in the language we could easily admit a
AT> generalisation of the renaming to a map from operations to terms, for
AT> instance. This, however, can be viewed as a derived form for first
AT> extending the target signature by new symbols and defining (by axioms)
AT> the new symbols to be equal to terms and then mapping the source
AT> signature operations to these new symbols. I am not sure how useful
AT> introducing this abbreviation would be in practice. I think that
AT> things like that are easily and most adequately done if there is a
AT> simple definitional langauge (for operations, and more generally
AT> algebras) around (revive abstract programs :-)

We agreed that a definitional language would be left to an extension.

*** 1.1 Signatures

ES> - It is required that the inclusion relation is partially-ordered. Is it
ES> really necessary that it is anti-symmetric. I have dropped this
ES> requirement. In our case studies there are some (not much) situations where
ES> is useful to have two sorts which are `equivalent' (the include each other)
ES> but not the same.

Please send examples showing where mutual embedding was found useful.

AT> PC> (7,1)
AT> PC> Why imposing antisymmetry on the ordering on sorts? Why not using
AT> PC> preorders rather than partial orders?
AT> 
AT> I do not think there would be any extra problems with this. However,
AT> if the ordering is to be interpreted as inclusion of the corresponding
AT> carriers then all sorts that are equivalent in the preordering would
AT> have to have the same carriers. So, no point. If, in turn, we stick
AT> only to embeddings between a sub- and supersorts, then there may be a
AT> point in allowing pre-orders here. Interestingly, it does not seem to
AT> follow then that the embeddings in a circular chain are actually
AT> bijective. This may be a good argument against pre-orderings here,
AT> since the intuition of equivalence would not be necessarily preserved...

Embeddings now induce a strict order: mutual (implicit) embedding is
not allowed.  So the difference between pre- and partial-orders disappears.

BKB> I would omit the "regularity..." comment here altogether;
BKB> there is a separate section for this (and obviously this needs analysis).

OK - and see study note [MC+PDM-1] for an analysis.

*** 1.2 Models

AT> PC> (7,16)
AT> PC> The requirement that the carrier of a sort is a *set* is in accord
AT> PC> with the tradition of universal algebra but may be too restrictive for
AT> PC> applications in computer science. I think in software specification
AT> PC> one may want to axiomatise properties, e.g. fixed points, which may be
AT> PC> unsound in a world of sets, unless a large piece of domain theory is
AT> PC> axiomatised as well. In these cases, a more liberal notion of first
AT> PC> order structure (e.g. a hyperdoctrine with suitable structure) may
AT> PC> relieve the user from order-theoretic concerns. Similarly, extensions
AT> PC> to the core language, e.g. to include polymorphism, may require a
AT> PC> notion of model not based on sets.
AT> 
AT> This is very true. Any extension going outside the standard algebraic
AT> formalism may require that the underlying notion of a model is
AT> enriched (by requiring continuous ordering on the carrier, for
AT> instance). Well, we have to settle for something and we decided to
AT> settle for something close to the most common thing in algebraic
AT> specifications.

In particular, we decided to exclude specification of infinite streams
and the like in the intermediate-level common language.

AT> I was surprised to see no compatibility conditions for overloaded
AT> operation symbols here. 

See the new 1.3.

BKB> I would omit the "not required to be a subset..." comment here altogether;
BKB> there is a separate section for this (and obviously this needs analysis).
BKB> I am worried that people may think we want (eventually implicit) coercions
BKB> that actually imply a real value conversion; I do not think we decided that.
BKB> I would not like it; such things should be explicit.
BKB> Also: you call it an *inclusion* order (!), so it should probably be a set
BKB> inclusion?

At Munich we agreed to go for embeddings, not set inclusions; see the
minutes.  Embeddings are injective: 1-1, total.  OK?

BKB> Also: the notion of a projection as the inverse of an embedding would
BKB> not hurt to be introduced here, as a derived concept
BKB> [perhaps with the comment that it is partial, see 1.4]

Only needed for casts, see the new 2.2.4, so not worth introducing
projections as a concept at all.

*** 1.3 Sentences

ES> - What is exactly meant by `Occurrences of ... assumed to be disambiguated' at
ES> the end of Section 1.3 (15 July version). Can I find something about this in
ES> any of the other documents. I am paying special attention to the point of
ES> ambiguous function application (need to, if you make a type checker). The
ES> remark made in the CoFI document on the subject seems a bit poor.

See 1.3, 2.1.2, 2.2.4, and [MC+PDM-1] for the revised proposal
concerning disambiguation of embedding.
 
AT> I would add here explicitly that equalities are between terms of a
AT> common sort, and that definedness asertions talk about definedness of
AT> terms.

OK.

AT> Then about the comment on explicit embeddings: so far, they seem to be
AT> necessary. Otherwise we might not be able to evaluate terms
AT> unambigously. In my view, the whole idea of introducing order-sorted
AT> signatures is to be able to avoid writing embeddings explcitly. So
AT> far, as far as I can see, there is nothing in the proposal which would
AT> make this possible.

See 1.3, 2.1.2, 2.2.4, and [MC+PDM-1] for the revised proposal
concerning disambiguation of embedding.

AT> PC> (7,-8)
AT> PC> Here, the user of the language is required to be aware of the
AT> PC> difference between two forms of equality, existential and strong.
AT> PC> Wouldn't he/she be mystified by discovering that the two notions
AT> PC> (as well as the definedness predicate) are in fact interdefinable?
AT> 
AT> Of course, something like this will be carefully explained in some
AT> manual or whatever. It does not have to be explained here. In fact,
AT> the mutual definability is a bit questionable, as we know, since one
AT> direction (strong from existential equality) holds only at the level
AT> of sentences: the strong equality cannot be defined as a predicate.
 
When the user sees the equivalent ways of expressing the two kinds of
equations (in the reference manual) this may help the appreciation of
the distinction between them.

BKB> I would reorder the atomic formulae as 3,1,2, or 2,3,1, or 2,1,3
BKB> (the definedness assertions are a bit forlone amid the others, where
BKB> equations are like a kind of predicate)
BKB> [after reading 1.4: order 2,3,1 is best as an order of "complication"]

Now 3,2,1 - not wanting to make definedness assertions appear so
prominent, as they are the least used.

BKB> * Terms
BKB> I think there should be NO implicit projections; the projection implies
BKB> a proof obligation or else ... (this is the discussion about QUA etc.).
BKB> This has NOT only to do with overloading resolution.
BKB> In chapter 1 (semantic basis), explicit embeddings and projections are OK,
BKB> with perhaps a forward reference to the fact that embeddings are always
BKB> implicit while projections are a more complicated issue.

There are no implicit projections.  Casts allow explicit projection,
or rather, inhibition of implicit injections, giving undefined if the
value of the term is not in the specified subsort.  The notion of
proof obligation is a subsidiary notion, concerning methodology but
not the semantics of the language.

*** 1.4 Satisfaction

AT> Projections, referred to here, have not been defined anywhere. I guess
AT> they should be mentioned in 1.2 Models (as the obvious partial
AT> inverses to embeddings).

See above.

BKB> * inclusion-related sorts
BKB> [see my comment on 1.2 about the term "inclusion-related sorts";
BKB> also, if you agree to omit implicit projections in this chapter or make
BKB> both explicit here, the first sentence of the last paragraph in 1.4
BKB> essentially goes away. I would still keep the comment though, perhaps move
BKB> it to 1.2.

See an earlier response above.

AT> PC> (8,14-17)
AT> PC> I find this sentence not very clear.
AT> 
AT> I am not sure which sentence this refers to. If he means "The
AT> application of a function symbolk f to a tuple of argument terms..."
AT> in sec.1.4, then I think that the statement is correct, but indeed not
AT> very easy to follow...

BKB> * evaluation of terms
BKB> The "unless" is a bit confusing [also typo evaluations ... giveS]; why not
BKB> "... is undefined if an evaluation of an argument term is undefined, or ...".

Changed.  Better now?

AT> PC> Finally, I was wondering how can non-strict functions be specified in
AT> PC> the framework of the common language. It seems unlikely that one can
AT> PC> sensibly do so "by hand," that is by explicitely manipulating bottom
AT> PC> elements, because that would not fit with the notion of partiality
AT> PC> built in the logic. A "type-theoretic" approach could be to introduce
AT> PC> a sort constructor (_)' for "lifting," where the intended carrier of
AT> PC> (s)' is obtained by adjoining a bottom element to the carrier of the
AT> PC> sort s. Then, partial functions from s1 to s2 have arity s1 -> (s2)'
AT> PC> while non-strict functions from s1 to s2 have arity (s1)' -> s2.
AT> 
AT> Each instance of what he is sketching here can be handled in the
AT> order-sorted framework, I think. On the other hand, he is right that
AT> since our "built-in" partial functions are true partial functions, we
AT> cannot turn them into non-strict ones in any uniform way. Again, i
AT> think this was a concious design decision, reflecting our view that
AT> true non-strictness is a relatively rare thing (we are not talking
AT> here about a well-defined error-recover, where we have some specific
AT> set of values classified as errors, but about true undefinedness and
AT> "lazy" functions that can truly disregard the evaluation of their
AT> arguments).

Agreed.

BKB> * evaluation of formulae
BKB> [see 1.3: order 2,3,1 is best as an order of "complication"]

Changed to 3,2,1, as above.

*** 1.5 Logic.

AT> The word "logic" was used for "inference" or "proof system" so far;
AT> in the last sentence here ("the logic is to remain 2-valued.") it
AT> referres to some semantic issue (I guess you mean that the meanings of
AT> formulae are in the standard two-valued set of logical values).

BKB> [typo: ... TO take INTO account ... ]
BKB> shouldn't the paragraph say something like:
BKB> "the logic HAS BEEN adjusted ... "; otherwise the impression is raised
BKB> that we do not know whether this is possible; also:
BKB> " the logic REMAINS TO BE 2-valued"

Formulation changed.  OK?

*** 1.6 Constraints

AT> To "...a term built just from this symbols" I think one should add
AT> "...and variables of other sorts" and perhaps mention a valuation of
AT> variables somewhere. Also, perhaps "every element" should be
AT> disambiguated to something like "every element of a sort in S".

Changed.  OK?

*** 2.1 Declarations of Symbols

BKB> * SYMBOL
BKB> I have made a similar comment before on the AS, although in a different context:
BKB> I do not like the explicit discrimination betwen different kinds of symbols
BKB> (or IDs). I do not mind the distinction of SYMBOLs as in
BKB> SYMBOL ::= SORT | CONST | ...
BKB> especially as they are nicely linked to the associated "types" on the next
BKB> line. But then they should go to ID directly, e.g. SORT ::= ID; this
BKB> emphasizes that resp. applied occurences are distinguished by their "type".
BKB> I realize that my major reason is extendibility to higher order; but even
BKB> in first order the fact that an ID is a FUN, for example, doesn't tell you
BKB> much, you have to know the type, i.e. you will generally have to have the
BKB> mapping from ID to TYPE (where ID eventually has to be unique; this is the
BKB> real issue).

Changed.  Better now?

BKB> * TYPE
BKB> I realize terminology (and finding suggestive terms) is not easy. I also
BKB> like (to indicate the uniformity I suggested and even in a way in
BKB> preparation for higher order) that the qualifying "thing" in a DECL is
BKB> uniformly denoted by TYPE. However, I feel a bit awkward with the term TYPE
BKB> here since it may lead to confusion, especially with SORT-TYPE; or does it
BKB> not? perhaps replace TYPE by KIND?

SORT-TYPE has now been removed - otherwise it could indeed have been
replaced by SORT-KIND.  Personally, I prefer to use "sort" for symbols
identifying sets, and "type" for general terms denoting sets.  If
there is a better terminology, please let me know.

BKB> * several symbols ...
BKB> I do not understand the sentence; it makes me worried.

Expanded a bit.  Better?

*** 2.1.1 Sorts

DB> 1- The notion of "structured sort" appears in 4.2 and 4.3 and does not
DB> seem to be defined previously, nor reflected in the abstract syntax.
DB> Does it refer to subsort relations ? or to types defined by schema ?

No.

DB> 2- In the Minutes of the Munich meeting, it is mentioned at the end
DB> the wish (or the need ?) to use "sort expressions" like "set[nat]".
DB> Is this notation the same notion as the one in point 1 ?

Yes - see the changed 2.1, 4.2, 4.3.

*** 2.2 Sort inclusions

AT> Ughhh. Do you really think that allowing sequences like this is
AT> useful. I found this surprising and perhaps unnecessary, certainly not
AT> worth encouraging. I personally would just leave
AT> 
AT> SORT-INCL ::= sort-incl SORT SORT
AT> 
AT> here. If anything, then perhaps i would feel tempted by:
AT> 
AT> SORT-INCL ::= sort-incl SORT+
AT> 
AT> with the intention of a linear order on a sequence of sorts. Or
AT> perhaps sort-incl (SORT+)+ to joint the two proposals :-)

I was wanting to follow OBJ here...  Now that sort declarations are
bundled together with specifying embeddings, it is actually necessary
to allow *all* the subsorts of a new sort to be specified at once, and
linear chains cannot be specified directly.

We might reconsider whether a sort declaration should be restricted to
declaring a single new sort, but it's a rather minor issue, IMHO.

BKB> I do not mind the term "inclusion" if is one (see 1.2); otherwise just
BKB> "order on sorts".

"Embedding" now, OK?

BKB> I hed to read the sentence twice; perhaps better "contributes the
BKB> inclusion ... second sequence to the partial order on the set of sorts".
BKB> I find the generalization to sequences a bit confusing and probably not so
BKB> often useful in practice, but I guess that's probably OK. I understand A <=
BKB> B, C and A, B <= C; then A, B <= C, D presumably means A <= C, D and B <=
BKB> C, D. A more useful generalization might be a concrete syntax such as A <=
BKB> B <= D for a chain, and there are obvious combinations. But do we need/want
BKB> all this?

OBJ does.  (What other languages have subsorts, and what do they allow?)
Chains are not relevant to the new proposal for embeddings anyway.

*** 2.2 Sort Inclusions

Removed, affecting the section numbering (the section numbers below
refer to version 0.9, 0.91).

*** 2.3.1 Quantifiers

BKB> VAR ::=
BKB> is missing.
BKB> Typo: *more* than
BKB> 
BKB> shouldn't it be "nesting of quantifications" rather than "sequence of
BKB> successive  quantifications"?

Changed.  OK?

*** 2.3.3. Atomic formulae

AT> Something must be said here more explicitly about the sort of terms
AT> involved equalities and in the membership assertions. For the former,
AT> i guess the sorts must be related (it may be too strong to demand that
AT> the two terms have a common sort). For the latter, I guess the same
AT> (that the term has a sort related to SORT) even though the text seem
AT> to suggest that SORT must be a subsort of a sort of the term.

The difference would only arise in the lack of "coherence", I
suppose.  OBJ insists on coherence; are there natural examples of
incoherent order-sorted specs?  (BTW, Maura and I considered requiring
coherence, but dropped it as it is non-modular.)

BKB> * equations
BKB> What do you mean by "are equally expressive"? this sounds confusing. If you
BKB> mean one can be expressed in terms of the other (plus definedness), than
BKB> say so and preferably give the definition.

It's a subtle point, and I think too technical for the summary.  I've
removed the offending phrase, OK?

BKB> * definedness
BKB> typo: is *is*
BKB> 
BKB> Should be "... is the same as (or included by) the sort ..."
BKB> 
BKB> I suppose these rather involved sentences will go away once we have a
BKB> concrete syntax to express equivalences/definitional transformations.
BKB> Or should we use AS here to do it? e.g., for T a TERM:
BKB>         definedness T <==> equation existential T T
BKB> and, for T a TERM, where the SORT of T is S:
BKB> if S <= S1 then:  membership T S1 <==> definedness T
BKB> if S >  S1 then:  membership T S1 <==> definedness (cast T S1)

I'd prefer to keep the present summary as concise and informal as
possible.  Once the formal semantics has been worked out, we may
replace the involved sentences by accurate definitive statements
following your suggestion.

*** 2.3.4 Terms

BKB> * cast
BKB> "... is included in or equal to ... of an embedding or the identity, resp.;
BKB> when ..."

Changed, OK?

*** 2.4 Sort Generation

BKB> I would reduce SORT+ in SORT-GEN to SORT;
BKB> I see no practical use for more than one sort to be generated by the same
BKB> symbols and it is an unneccessary requirement for the concrete syntax.

Please forget about concrete syntax for now!  Andrzej: do we have
practical examples requiring the extra generality?  I guess if one
wanted something like a type-definition schema but only requiring sort
generation rather than freeness, one would need it... but does one
want that in practice?

*** 2.5 Type Definition Schema

BKB> I hope that we will eventually define them by definitional transformations.
BKB> Even now I guess it would not hurt to include a sentence like "are
BKB> equivalent to a specification as follows ..." ??

BKB> * type definition
BKB> "... constants, these are declared as total *constructors* with ..."

OK

BKB> What needs to be checked about the mixing?

Only whether you like the extra generality or not... :-)

Part II
-------

*** 3 Structuring Concepts

DB> 3- I think that it is possible to introduce what I call "sort expressions"
DB> in the language (because this has been done (at least) in LPG and GLIDER).
DB> But the meaning of such notations must be well understood. It is a
DB> notation for refering to a sort of an instantiated module, so we have to be
DB> able to
DB> 3.1- associate a sort (or any other SYMBOL) to the specification of
DB> its declaration;
DB> 3.2- determine a complete list of RENAMING (in PAR-INST) from the
DB> list of actual sorts (inference of actual operators and predicates, if any);
DB> 3.3- compare specification expressions.
DB> 
DB>   The last point is probably the most difficult, because the specification
DB> expression language is very rich (at least at the level of the abstract
DB> syntax).
> Kindly expand on the reasons for 3.3, which I don't appreciate yet.
DB>   Using sort expressions (e.g. seq[nat] but also matrix[polynome[rational]],
DB> etc.) assumes that we have implicit specification expressions, i.e seq[nat]
DB> is the sort "seq" in the imported and/or implicit specification :
DB> 
DB> 	of-spec spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat)
DB> 
DB> From now on, we can have two strategies :
DB> 
DB> A) either "seq[nat]" is a simple new name, as if we write :
DB> 
DB>  	of-spec translation renaming (seq => seq[nat])
DB> 		(spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat))
DB> 
DB> B) or we consider that "seq[nat]" contains the information of the origin
DB> specification together with the "fitting" or instantiating morphism. This
DB> is a first step towards considering the equality of SYMBOLs as the equality
DB> of the origin + equality of importation morphism.
DB> 
DB> Examples :
DB> 
DB>   With the first assumption (case A), if we have together :
DB> 
DB> 	of-spec spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat)
DB>  	of-spec translation renaming (seq => seq_nat)
DB>  		(spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat))
DB> 
DB> then seq[nat] is different from seq_nat.
DB> 
DB>   In the second case (B), both can be considered as equal, even if they have
DB> not the same "surface name".
DB> 
DB> Comment on sharing : What I consider problematic in the ASL style
DB> is that all the SYMBOL names are considered independently from their
DB> specification module. We have a kind of large and unstructured "name space".
DB> This is acceptable for names of very loose specifications (e.g. associativity)
DB> where the declared SYMBOL names are not significant and may be renamed in
DB> the specifications where they are used. But it is not the same for names of
DB> specifications with (more or less) standard interpretation like SYMBOLSs
DB> occuring in data types. It is why I am a bit perplex when I see something
DB> like :
DB> 
DB>  	of-spec translation renaming (seq => seq_nat1)
DB>  		(spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat))
DB>  	of-spec translation renaming (seq => seq_nat2)
DB>  		(spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat))
DB> 
DB> and where the distinction between the two modules is done only by the new name
DB> of the sort "seq". If there is a declaration in SEQ like :
DB> 
DB> 	f : nat -> nat
DB> 
DB> the two occurrences of f are confused and this can lead to identification
DB> problems when using f. This point is connected to the issues raised in the
DB> specification SP3, in my previous message.
DB> 
DB>   Maybe a better solution in that case is to use an explicit "copy" construct
DB> giving two fresh copies of SEQ and then to use renaming in order to avoid
DB> confusion of names coming from (this time) different specifications. I am not
DB> in favor of a systematic implicit copy when using an instantiated module.

In my understanding, we are aiming at a much simpler notion that what
you describe, purely to provide some implicit, easily-explained,
renaming for use with instantiation.  I don't see the relevance of
specification expressions for this renaming at all.  Anyway, it's
listed as an issue to be discussed in version 0.92.

DB> 4- The third paragraph of 3 (Structuring Concepts) addresses the
DB> main problem in naming and renaming instantiations of generic specifications.
DB> This problem is well known. In a specification such as (in a kind of
DB> simplified abstract syntax):
DB> 
DB> defn SP1
DB>     extension
DB> 	of-spec spec-fun-inst SEQ par-inst ELEM BOOL renaming (elem => bool)
DB> 	of-spec spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat)
DB> 	<BY-SPEC1>
DB> 
DB> Here, the ASL strategy of sharing confuses the two sorts "seq" in <BY-SPEC1>.
DB> So, the usual way is to rename at least one "seq" (the operators are
DB> overloaded):
DB> 
DB> defn SP1
DB>     extension
DB> 	of-spec translation renaming (seq => seq_bool)
DB> 		(spec-fun-inst SEQ par-inst ELEM BOOL renaming (elem => bool))
DB> 	of-spec translation renaming (seq => seq_nat)
DB> 		(spec-fun-inst SEQ par-inst ELEM NAT renaming (elem => nat))
DB> 	<BY-SPEC1>
DB> 
DB> But sometimes, we need to share specifications or SYMBOLs which are
DB> at some level different. A characteristic example is :
DB> 
DB> defn ELEM1 translation renaming (elem => el1) ELEM
DB> defn ELEM2 translation renaming (elem => el2) ELEM
DB> 
DB> defn SP2
DB>   spec-fun of-spec-name ELEM1 			-- already this is painful !
DB> 	   of-spec-name ELEM2
DB>     extension
DB> 	of-spec translation renaming (seq => seq_el1)
DB> 		(spec-fun-inst SEQ par-inst ELEM ELEM1 renaming (elem => el1))
DB> 	of-spec translation renaming (seq => seq_el2)
DB> 		(spec-fun-inst SEQ par-inst ELEM ELEM2 renaming (elem => el2))
DB> 	<BY-SPEC2>
DB> 
DB> And now, an instantiation of SP2, where the two sub-specifications of
DB> SEQ must be the same. Is such specification legal and/or tractable ?
DB> 
DB> defn SP3
DB>     extension
DB> 	of-spec translation renaming (seq_el1 => seq_nat, seq_el2 => seq_nat)
DB> 		(spec-fun-inst SP2 par-inst ELEM1 NAT renaming (el1 => nat)
DB> 				   par-inst ELEM2 NAT renaming (el2 => nat))
DB> 	<BY-SPEC3>
DB> 
DB> Moreover, this example shows that too simple mechanisms induce
DB> overheads in writing specifications and could definitively discourage
DB> people who want to use parametrized specifications to specify and use a
DB> "mapcar" function on the sequences !
DB>   As alternatives, one can see the proposal for class polymorphism in
DB> Spectrum or the solution of sub-specification sharing using morphism
DB> information in the study note DB-1 (part 3 and 4).

I hope that Michel Bidoit (the main architect of the current proposal
for parametrized specifications) will reply to the above.  It's also
listed as an issue to be discussed in version 0.92.

*** 4.1 Specification Libraries.
 
AT> I still do not know what the intended semantics of linked libraries
AT> (mutually resursive specs) should be. Sorry, i have not worked out any
AT> possible semantics either. Was I supposed to? :-(

Yes!  :-)  Anyway, I've added a bit more - but not worked out the
details yet... 

BKB> * linear and linked libraries
BKB> You (or those discussing in Dagstuhl, I guess) are introducing new stuff
BKB> here. 

The need for mutually-dependent modules was discussed in Munich, see
the minutes.  (BTW, they were sent only to the participants, but as it
was such an important - and successful! - meeting, perhaps we should
forward them to all cofi-language subscribers?)  We agreed to stick to
linear visibility "unless some construct is provided with a clean
semantics where mutual dependency can take place".  The proposed
construct was an attempt to provide such.

BKB> Not that I mind in general; but I find the distinction between 2
BKB> kinds of libraries confusing and, frankly, a little half baked.
BKB> Linked: is it rather "nested"? then "level" would make sense. If we have
BKB> this, then why "linear" as well? Nesting would be rather natural, with path
BKB> names (dot notation??) such that names do only have to be unique for any
BKB> component library at a given level; i guess such a component library would
BKB> then be the "linear" one, but there is one uniform notion of library.

I hadn't intended any nesting, nor separate levels of scope.  Now
simplified and made non-nested.  Any better?

BKB> What is as SML recursive local declaration? I hope not the re-use of an ID
BKB> in a sequence (I am very much against this).

No: let rec VALBIND and ... and VALBIND in EXP end.

BKB> By the way: one way to implement the (good) idea of WWW URLs is to include
BKB> a library FX somewhere (i.e. at some level of nesting) in a library NX such
BKB> that any given coponent has either a natural father from NX or a foster
BKB> father from FX; in fact, this results in a directed graph rather than a
BKB> tree from nesting.

I don't understand what FX and NX are supposed to be, but never mind,
there's no nesting now...

BKB> The sentence "A named SPEC .." is a little hard to read; better would be:
BKB> "'closed', i.e all names referred to *are* available in .. and it *does not
BKB> depend* on ..."

Changed.  Better?

BKB> * SPEC-NAME etc.
BKB> Please reorder AS rules for analogy as in SYMBOL and TYPE in 2.1, i.e.
BKB>         NAME            ::= SPEC-NAME   | SPEC-FUN-NAME
BKB>         SPEC-ENTITY     ::= SPEC        | SPEC-FUN
BKB> 
BKB> Unfortunately, an inconsistency of terminology in the AS now becomes apparent:
BKB> in 2.1, SYMBOLs (e.g. SORT or FUN) have no suffix, whereas TYPEs do (e.g.
BKB> FUN-TYPE). In analogy, we should have
BKB>         NAME            ::= SPEC        | SPEC-FUN
BKB>         ENTITY          ::= SPEC-ENTITY | SPEC-FUN-ENTITY
BKB> (or SPEC-UNIT or SPEC-EXP etc.)
BKB> Alternatively, you could change in 2.1 to
BKB>         SYMBOL          ::= SORT-ID | CONST-ID | FUN-ID ...
BKB>         TYPE            ::= SORT    | CONST    | FUN ...
BKB> and here leave as is.
BKB> I think such analogies should not be dismissed too lightly!!
BKB> Note that you yourself write "a specification *expression* SPEC ...".

To be really consistent, both CONST and VAR would be VALUE-ID, I
suppose... (as in Z!).  Anyway, names serve quite a separate purpose
from symbols in our language, and I found it helpful to reflect this.
Is the new version any improvement?

BKB> Note: the "... SPEC .. is ... unparametrized ..." is dangerously confusing,
BKB> since indeed a SPEC may appear in a SPEC-FUN; I guess it depends on what is
BKB> meant by "parametrized" since in this case the SPEC does not contain free
BKB> occurrences but indeed bound by parameters; so is it parametrized?

No.  (But I don't see the confusion, sorry.)

*** 4.2 Specification Expressions

AT> On: "Note that symbols used as sorts may have internal structure...".
AT> Nothing like this is there so far:
AT> 
AT> SORT ::= sort ID
AT> 
AT> Aha: this was turned into a "To be checked" note now...

See new 2.1.

BKB>* closed
BKB> I am not sure I understand what you mean by local environment here. Can I write
BKB>         union [T: sort] [f: T]
BKB>                         E
BKB> (which I would like to be able to do) or not? In my interpretation the
BKB> local environment E includes T.

No!  Not in mine!  The SPECs in a union are supposed to have complete
signatures, taking into account the symbols declared in the local
environment available to the entire union.  And union should be
commutative (or called something different!).

BKB> * mapping
BKB> I thought our conclusion was that you need either hiding OR exporting but
BKB> not both, and renaming is then defined accordingly.

No - see the minutes (written while your were on vacation... :-).

BKB> The advantage of a SPEC exp with explicit export (over hiding) is that
BKB> extensions can be made in the original spec without affecting the SPEC exp.
BKB> My definitely preferred solution would be one with a much simpler AS
BKB> TRANSLATION     ::= translation MAPPING* SPEC
BKB> MAPPING         ::= RENAMING | EXPORTING
BKB> RENAMING        ::= symbol-to-symbol SYMBOL SYMBOL
BKB> EXPORTING       ::= exporting SYMBOL
BKB> where any unmentioned symbols are hidden. Note that my solution allows for
BKB> free combination; in fact
BKB>         symbol-to-symbol S S <==> exporting S

The problem with your (admittedly nice and simple) version is that to
rename a single symbol, one would have to explicitly export all the
others.  This would be intolerable when instantiating parametrized
specifications, at least.

BKB> To achieve this effect in your case, I guess you would have to rename first
BKB> and then export; this becomes very confusing since you would have to export
BKB> the renamed versions!

Good point.

BKB> I guess one could also have my version of exporting (with optional
BKB> renaming), plus your renaming (with implicit export of the rest) plus
BKB> hiding.
BKB> Perhaps we can come back to this also in connection with a concrete syntax.

No, it is an issue for abstract syntax too.  I've listed it as a point
for discussion in v0.92.

BKB> * union etc.
BKB> I read the first sentence several times and still do not understand.
BKB> I wish we would use definitional trafos, making it clear.

Changed.  Any better?  (What is a trafo?)

BKB> OF-SPECS: What is "importation" 

As in OBJ3, Larch, ASF+SDF, Ada, ... (with various keywords - often "use").

BKB> (dont we reduce everything to union here?)

Not in my understanding (although the minutes might be read that way).

BKB> and why the restriction here to "named" specifications (not reflected in
BKB> the AS; this is good, e.g. instantiations and the like)?

No restriction intended.

BKB> Why do you not write
BKB>         PERSISTENCE     ::= persistent | ()
BKB> This would make it more logical and uniform with FREEDOM; also, when
BKB> composing (requirement) specs from pieces, non-persistency would definitely
BKB> be the more common for me, i.e. the default.

OK, changed.

*** 4.3 Parameterised Specifications

AT> I would allow arbitrary specification expressions as actual paramaters
AT> in parameter instantiations.

OK, changed - still an issue for discussion.

AT> And about the recently added comment: I don't like the suggested way
AT> of fixing a part of the parameter specification. Somehow, the use of a
AT> named specification should not really be distinguishable from the use
AT> of the specification (expression) it names. The suggested convention
AT> breaks this...

It seems useful to insist on the formal parameters being named, to
allow partial instantiations.

BKB> I thought we had restricted ourselves to persistent extension w.r.t. the
BKB> formal parameters? here the default (if we have non-persistent as well,
BKB> which I do not like) MUST be persistent, but this should not burden the
BKB> general case in 4.2.

Changed: the new version only allows persistent parameters, but an
issue for discussion.

BKB> I have no idea what the implications are of having the FREEDOM option here;
BKB> has this been discussed and is there a need for both?

Yes...  E.g., the body of a parametrized specification of LISTS wouod
typically be free.

BKB> I do not understand the second paragraph AT ALL.

Any better now?

BKB> Instantiations: I am strongly opposed to non-positional instantiation as it
BKB> is defined here; I insist on the analogy with function application. 

Why?  It makes partial instantiation quite clumsy, IMHO.  
(May I recall that you previously wanted to forbid parametrized
specifications altogether; I don't see why you feel so strongly about
the details of something you presumably wouldn't want to use in any
case...  Anyway, parametrization is listed as an issue for discussion.)

BKB> Thus
BKB> why not
BKB>         PAR-INST ::= par-inst SPEC
BKB> or
BKB>         PAR-INST ::= par-inst TRANSLATION
BKB> but why the restriction to names here? why not for example an instantiation
BKB> nested in an instantiation? if you want to exclude BASIC-SPEC this can be
BKB> done by a semantic restriction, but is only methodological and would not
BKB> mess up the semantics.

Changed.

BKB> I do not understand the comment about structured sorts.

Example added.

Part III
--------

BKB> * general
BKB> I do not like the term "organisational specs" as it has other obvious
BKB> connotations; why not "architectural spec" as we always said?

Because others found "architectural" misleading too.  How about the
new proposal, "decompositional"?

BKB> I see no reason to have them separated from structuring concepts/constructs
BKB> in a separate part. I would find it better to contrast one and the other in
BKB> chapter 3, i.e. combine 3 and 5. A separate chapter for the Arch specs (as
BKB> now in 6) is fine but I would prefer this under Part II.

Personally, I prefer to keep distinct the sublanguage that does not
prescribe model composition.  What do others think?

BKB> So there are two kinds of structuring: one not affecting the structure of
BKB> models and one imposing a structure on them.
BKB> So why not flat (but structured by composition in SPEC expressions) specs
BKB> and hierarchical specs (i.e. ones where the structuring remains inherently
BKB> so)? I suppose one could also say flat composition (models are "flat"
BKB> afterwards) and hierarchical (de)composition (also of the modesl and the
BKB> development (process). By the way: hierarchical (from my point of view) may
BKB> also mean acyclic directed graph.

"Flat" seems misleading too.  Also, "hierarchical" has a rather
different conventional meaning in connection with algebraic specfications.

*** 6. Organizational Constructs
 
AT> Three comments here , in the decreasing order of importance:
AT> 
AT> First, there seems to be no way to name organizational specs, put them
AT> into libraries etc. I think we need this.

Not added yet.  Please explain why it is important, and indicate the
methodology concerning it.

AT> Second, what about the possibility of nesting the organizational
AT> requirements, by allowing a specification for a unit in an
AT> organizational spec to be an organizational spec. I guess this will be
AT> happenign in the development process, by it seems no harm can be done
AT> by allowing this already here as well.

Added.

AT> Finally, in a similar wya, maybe the bodies of UNIT-FUN-SPEC could be
AT> made organisational as well?

Added.

BKB> I do not like the terminology TASK (just remember all the languages with
BKB> parallel tasks) and ORG, PRODUCT etc. Also: refer to the discussion about
BKB> the NAME suffix in 4.1 above. Why not
BKB>         HIERARCHICAL-SPEC       ::= hierarchical-spec ITEM-DECL* HIERARCHY
BKB>         ITEM-DECL               ::= item-decl ITEM ITEM-SPEC
BKB>         ITEM                    ::= UNIT | UNIT-FUN
BKB>         ...
BKB>         ITEM-SPEC               ::= SPEC | UNIT-FUN-SPEC
BKB>         ...
BKB>         HIERARCHY               ::= UNIT | UNIT-FUN-INST | REDUCT
BKB>         ...

Changed.  Any better?

BKB> Here we have application! Good! so why not in 4.3?

Because here the interfaces don't necessarily have names, nor is
partial application required.

BKB> The connection between chapters 4 and 6 is not clear yet!

You're right, something is missing: when one has a SPEC, possibly
referring to named specs in a library, the idea was to refine it to a
decomposition - but we don't have SPEC ::= LIBRARY in SPEC at all...
Should we add it, do we need it?

*** Abstract syntax

AT> About the way the sytnax for declarations is presented. In my view,
AT> this unnecessarily moves extra requirements to some static semantics
AT> (context conditions) to express the implicit requirements that the
AT> kinds of the symbol(s) being declared fits the kind of the type
AT> provided for it. I guess this is a matter of taste, but I certainly
AT> would prefer this to be expressed in the grammar (as a context-free
AT> condition), e.g.:
AT> 
AT> DECL        ::= SORT-DECL | CONST-DECL | FUN-DECL | PRED-DECL
AT> SORT-DECL   ::= SORT+  SORT-TYPE
AT> CONST-DECL  ::= CONST+ CONST-TYPE
AT> FUN-DECL    ::= FUN+   FUN-TYPE
AT> PRED-DECL   ::= PRED+  PRED-TYPE
AT> 
AT> I know, Bernd or somebody will say something about tools, etc, with
AT> which I have no experience, so i am not pushing too strongly :-)
AT> 
AT> The same applies to the way specification declarations are structured.

OK, I've changed it to the more exact style you suggest.  OK?

Phew...  That's it.  (Congratulations to those who read this far!)