[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
COMMENTS on Tentative Design Summary v0.92 (1200 lines)
COMMENTS on Summary of the CoFI Tentative Language Design
- version 0.92
Edited by 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.
N.B. Many of the language design group PARTICIPANTS have not yet sent
their comments; please do so as soon as possible (especially Michel,
concerning particular points below...). All comments sent to
cofi-language@brics.dk during the next week (16-20 September) will be
forwarded to the subscribers without collation or delay, i.e.,
FEEL FREE TO DISCUSS ANY ISSUES CONCERNING THE LANGUAGE DESIGN,
irrespective of their status in version 0.92. You may expect a new
version, 0.93, on 20 September, with a deadline for reactions on
7 October.
NEW PROPOSAL FOR THE NAME of the first-order common algebraic
language: FOCAL. Please REACT if you feel strongly for or against any
of the current proposals, or have new ones to make.
*** Contributors (thanks!) and their general comments:
TM> From: till@Informatik.Uni-Bremen.DE (Till Mossakowski)
TM> Subject: Comments on CoFI Ver 0.92
DTS> From: Don Sannella <dts@dcs.ed.ac.uk>
DTS> Subject: CoFI language design version 0.92
DTS> Here's my reaction to version 0.92 of the language design. It reads
DTS> pretty well, so my comments are mainly about fairly minor matters.
DTS> I haven't been able to read your note with Maura on subsorting (I
DTS> glanced at it on the net in Cracow, but was unable to get a printout
DTS> to take away, and I have no way to get access to it until after 16th
DTS> Sept) so my comments on this part are less well-informed than they
DTS> should be. I haven't been able to read the previous versions since
DTS> Munich by the way, so my mind is uncluttered by stuff that has been in
DTS> previous versions. I have had a look through the comments on the
DTS> previous versions though.
MWa> From: Michal.Walicki@ii.uib.no (Michal Walicki)
MWa> Subject: Comments: CoFI X, version 0.92
MWa> Page numbers refer to the document version 0.92
AH> From: Anne Haxthausen <ah@it.dtu.dk>
AH> Subject: Comments to tentative CoFI language design, version 0.92
AH> Generally I like the language proposal. You have really made a great
AH> piece of work. Concerning subsorting stuff I find that more
AH> investigations are needed. E.g. what are the consequences for the
AH> typing of terms, when you do not require regularity, etc.
BKB> From: bkb@Informatik.Uni-Bremen.DE (Bernd Krieg-Brueckner)
BKB> Subject: Comments on CoFI Ver 0.92
BKB> [a little edited here]
BKB> There are a number of new ideas that have not been discussed at Munich
BKB> and thus naturally fall under special scrutiny and criticism, perhaps
BKB> because they have not been (or are not yet?) well understood.
BKB> Some appear to be rather ad-hoc.
BKB>
BKB> [some comments on subsorts in 0.92, a proposal prematurely put into the
BKB> design document, are following separately in a note by Till;
BKB> we (i.e. Till Mossakowski,Anne Haxthausen, Olaf Owe, BKB) are working on
BKB> another proposal, as we were asked to do in Munich]
Good! For various reasons, I'm about to split Part I so as to present
the many-sorted basic specs first, followed by separate chapters for
what changes are needed to accommodate subsorts. So you need only
provide your version of the latter, and I'll insert it for comparison.
AT>> Report by PDM of recent discussions with Andrzej Tarlecki;
AT>> Andrzej will correct any serious misunderstandings (as usual :-)
*** MAIN ISSUES FOR DISCUSSION
*** Name:
DTS> Another suggestion is Coala (pronounced like Koala): COmmon
DTS> Algebraic LAnguage. A sublanguage could be called Coala Bare? I
DTS> don't like this much, and I'm neutral with respect to the other
DTS> suggested names.
MWa> In order of preference:
MWa> CLASS Common Language for Algebraic Software Specification
Not bad: "First CLASS", "Higher CLASS", ... but perhaps a bit too OO?
MWa> KOALA instead of COALA: Common Algebraic Language
MWa> ALCOL Algebraic Common Language (too close to Algol?)
AT>> ALCOL is currently my preference - no enthusiasm though.
AH> As most others I do not like ALCOL (it is too close to ALGOL)..
AH> I like "Black CoFI", but we should be aware that the group
AH> of Futatsugi making the Cafe project uses names like "Cafe au lait"
AH> for their products. "CoLa" is also good proposal.
We should get the "Algebraic" in there somehow...
How about FOCAL?
AH> This name is fine.
AH> I have been thinking of CoFICAL for CoFI Common Algebraic Language,
AH> but I am afraid that it would be too difficult to pronounce.
*** Subsorts/embeddings
DTS> Seems okay, as far as I can tell without reading the
DTS> note. My main concern is that the semantics should be as simple as
DTS> possible and that in particular well-formedness should not be too
DTS> difficult to define.
Well-formedness certainly needed clarifying.
MWa> p.13, 2nd paragraph under AS says "...in a sort declaration DETERMINES
MWa> (total,1-1) embedding..." It is unclear whether "determines" means that
MWa> 1. user has to 'define' such an embedding here, or whether
MWa> 2. the system will 'assume' or else
MWa> 3. 'provide automatically' such a definition.
MWa> 2.1.2 suggests that such a definition (axioms) will occur at the
MWa> declaration of terms, so I guess you may mean
MWa> 4. puts an obligation on the user to define embedding
MWa> along with the declaration of terms
MWa> I'd like to see here a more clear statement of what "determines" means.
Something like: "Implicitly declares and asserts properties of"
MWa> Why do you allow extending sorts but not restricting them? (I guess, it
MWa> need not be so unusual that one specifies lists and then, in another
MWa> context, wants to use this specification to specify non-empty lists.) If
MWa> you mean avoiding the circular embeddings, then this can be done by the
MWa> tools - true, not in a modular way but still relatively simply.
Agreed.
MWa> As to modularity:
MWa> Is it user's responsibility to verify that if he declared
MWa> sort: S<T1, S<T2 and then sort: T1<T, T2<T (all with the associated
MWa> embeddings) then the respective compositions of embeddings S->T1->T and
MWa> S->T2->T are equal? In any case, this verification will not be modular!
p.13: "also determines axioms ensuring that any alternative
compositions of embeddings between the same two sorts are equivalent"
MWa> The proposal that "overloading does not carry any semantics" unless stated
MWa> explicitly by some axioms, seems to me clean and fine. The only thing that
MWa> worries me slightly here is the "incompatibility" with the treatement of
MWa> sharing. Of course, these may be seen as separate issues but, from the user
MWa> point of view, they make the language look a bit "inconsistent" - on the
MWa> one hand "same-name same-thing" and, on the other, "names don't affect
MWa> semantics". If so, then one should say explicitly (p.20, last paragraph of
MWa> 4.2) that union of two spes will identify not `two things with the same
MWa> names' but `two things with the same names and exactly the same profiles'.
MWa> (Perhaps, the presentation should make more explicit this distinction
MWa> between simple-names and full-names (including the profiles).)
OK
MWa> I have also a couple of doubts about casts.
Casting doubt seems quite appropriate here :-)
MWa> a. we have: sort: S < T
MWa> c : -> S
MWa> c: -> T
MWa> The two c's are different, and 'cast c T' is defined in both cases. What
MWa> does it do: evaluates c (as c:T) or applies embedding (to c:S)? When, and
MWa> how, does the disambiguation happen? Since embedding of c:S into T need not
MWa> coincide with c:T, the two alternatives may yield different things.
'cast c T' would be ambiguous, hence rejected.
MWa> b. we have: sort: S1 < T, S2 < T
MWa> c : -> S1
MWa> c : -> S2
MWa> What does 'cast (cast c T) S2' do ? Which c are we talking about here? If
MWa> we take c:S2 then nothing happens. But if we take c:S1, do we jump from S1
MWa> to its "sibling" sort S2? In case when the embeddings e1:S1->T and e2:S2->T
MWa> have non-empty intersection and e1(c) =/= e2(c) but e1(c) is in the image
MWa> of e2 (and vice versa), do we get the element from S2 which is mapped onto
MWa> e1(c)? In this case, we might continue and get that
MWa>
MWa> (*) cast(cast (cast (cast c T) S2) T) S1
MWa>
MWa> yields a defined result in S1 which is different from c:S1. (This will be
MWa> so even if the constants in S1 and S2 have different names. e.g. for d:->S1
MWa> and c:->S2, (*) with d will not give back d in S1.)
The intention was that no implicit assertions would be inserted unless
necessary... but it needs clarifying.
*** Compound sorts
DTS> A clear explanation of what they are is urgently
DTS> needed. See below (2.1.1). Apart from this, I think there may be a
DTS> problem with the interaction with hiding/exporting -- see below (4.2).
MWa> I assume that "compund sorts" stand for (names of) parameterized sorts,
MWa> something like 'list[nat]', not for structured sorts, like 'nat x nat'.
MWa> The last paragraph on p.13 does not make it entirely clear.
OK, will improve.
MWa> Except for this, I like the sort names like 'list[nat]'.
*** Predicates instead of sorts in function profiles
DTS> Seems nice provided it is restricted a bit -- see below (2.1.2).
MWa> I have the general problem with distinguishing between the AS of X and
MWa> concrete syntax. Since minimality (wrt. some intended expressive power)
MWa> was abandoned as an issue, I seldom see other reasons for not including
MWa> something. Unfortunately, these somethings look usually as syntactic sugar.
MWa> I do not like languages where the same thing can be said in many ways - I
MWa> think this confuses rather than simplifies. However X has already a lot of
MWa> such duplicates, so why not this one as well?
OK, although perhaps it would be better as an axiom-abbreviation
- think of fun sum: even even -> even, fun sum: odd odd -> even, ...
generating a declaration for each one.
MWa> I think that, at least, the final document (user manual?) should be
MWa> structured according to the distinction between the basic (necessary)
MWa> constructs (the kernel determining the expressivity) and the auxiliary
MWa> abbreviations. 'Predicates in function profiles' can then well find their
MWa> place in the latter.
We'll give the exact expansion there too, I guess.
*** Linked sections of libraries:
DTS> If it gives what you want, fine. This
DTS> isn't at all clear to me, because I haven't seen an example. I
DTS> wouldn't mind leaving it out. Maybe there should be some parts of the
DTS> design that are more tentative than others, and this should be such a
DTS> part; I can't (for example) see the point in thinking about the
DTS> semantics of this feature until there's more confidence that it makes
DTS> sense with respect to the needs that have been expressed.
(Surprisingly) in Munich I found I wasn't the only one in favour of
them. Exercise: try to linearize the modules used to specify a window
system by Guttag and Horning in "Formal Specification as a Design
Tool", Proc. POPL'80, pp. 251-261.
MWa> The notion seems clear but I don't see the reason for it. If I have a
MWa> programming langauge not requiring linear visibility (of declarations) I
MWa> really enjoy this flexibility even if, sometimes, I do declare things in a
MWa> linear manner. Having, on the top of this, some additional construct
MWa> restricting this form to the (sub)sections where things MUST be declared
MWa> linearly, does not seem to me to serve any practical purpose.If X provides
MWa> 'linked' visibility, is not linear visibility an issue to be decided by the
MWa> methodology group?
I guess that linearity has the simpler semantics though.
MWa> Also, it would help to see a brief explanation of the relationships between
MWa> the library-items. Apparently, they do not introduce any semantic barriers
MWa> - they are all treated as one library with names which are globally unique
MWa> (across the sections). So, I can use a name from one section in another
MWa> section, right? Is visibility across the sections linear or 'linked'?
Linear. Should be mentioned.
*** Renaming & hiding
DTS> Renaming: There seems to be a problem with the details of
DTS> renaming/hiding/exporting -- see below (4.2). I think it makes sense
DTS> to have all three constructs.
MWa> Cf. comment on 'predicates in function profiles'. Hiding is certainly a
MWa> nice abbreviation for exporting which releases the user from writing long
MWa> lists of exported symbols.
*** Parameterized specs.
DTS> I would like to see a reason for making any
DTS> non-necessary restrictions that are proposed, e.g. requiring formal
DTS> parameter specs to be named, the business about fixed parts of
DTS> parameters, distinguishing formal parameter specs from other specs,
DTS> requiring actual parameters to be names. I see no reason at all for
DTS> the last two of these. I don't like partial instantiation, at least
DTS> without a clear explanation of whether a partially instantiated
DTS> parametrized spec is a normal spec or a parametrized spec. I prefer
DTS> positional instantiation to instantiation by name.
Michel?
MWa> a. positional notation for actual parameters?
MWa>
MWa> Again, it looks like a question about concrete syntax. Personally, I prefer
MWa> positional notation for actual parameters. I guess one can easily fix
MWa> partial instantiations in this notation by introducing a simple symbol,
MWa> e.g., given a parameterized specification with formal parameters
MWa> By [ A, B, C, D ]
MWa> one could write something like
MWa> By [ A1 by a, _ , _ , D1 by d ] or By [ A1 by a, id , id , D1
MWa> by d ]
MWa> (where 'by a' is the required renaming). This kind of "hole"-notation would
MWa> certainly be needed with positional notation if formal parameters are
MWa> allowed to be SPECs.
Michel?
MWa> b. distinguished definitions of formal-parameter specs?
MWa>
MWa> Definitely not! Formal parameter specs are specs. Why should one bother, at
MWa> the moment of writing a specification, whether it is ever going to be used
MWa> as a formal parameter or not?
MWa> c. actual parameters restricted to names?
MWa>
MWa> Why should they be restricted to names? The credo that "wherever a name
MWa> occurs the actual (named) entity may occur instead" seems to me a very
MWa> clear feature giving the whole language a bit of "uniformity". It may
MWa> happen that one wants to instantiate a parameterized specification by an
MWa> actual parameter occurring only once - in this very instantiation.
MWa> Requiring names and forbidding specs (here or elsewhere in similar
MWa> contexts) might lead to polluting the library with additional, unnecessary
MWa> names.
MWa> d. always persistent parameters?
MWa>
MWa> Now it says (bottom of p.20) that SPEC-FUN is "... the extension implicitly
MWa> required to be persistent". The first sentence of the top paragraph on p.21
MWa> says "Any persistently-extended parts of the SPEC...". This qualification
MWa> is either redundant or else hides something which it is impossible to
MWa> figure out from the present text.
The latter!
MWa> First, some comments on extension:
MWa> 1. In Munich it was decided to use a rather liberal definition of
MWa> persistency - the class of the reducts of the extension must be contained
MWa> in (but not necessarily equal to) the class of the models of the extended
MWa> specification. (It is how I understand the note from the minutes, in
MWa> particular, "no totality requirement".)
MWa> In 4.2, the sentence characterizing 'persistency' is a bit unclear. Does
MWa> "no further properties may be imposed on imported elements" mean that one
MWa> cannot extend persistently a PO spec to a TO spec? This looks like the
MWa> standard definition of persistency and not the one from Munich.
MWa> However, I might have misunderstood the definition from Munich - I simply
MWa> cannot see what a non-persistent extension would be???
Somebody, please clarify this - I'm getting confused too!
MWa> 2. The current AS says:
MWa> EXTENSION ::= extension OF-SPEC* BY-SPEC
MWa> and
MWa> BY-SPEC ::= FREEDOM SPEC
MWa> Do not we allow extensions by mere BASIC-ITEMs? I.e., shouldn't it say
MWa> BY-SPEC ::= FREEDOM SPEC | FREEDOM BASIC-ITEM*
No, we already have SPEC ::= BASIC-SPEC ::= ... BASIC-ITEM*
MWa> (3. A minor point concerning UNION in 4.2. Would it hurt to have
MWa> UNION ::= SPEC SPEC+
MWa> i.e., to allow a union of possibly more than two specifications?)
or maybe simply UNION ::= union SPEC+
MWa> As to the question whether parameters should be required to be persistent
MWa> (assuming that the definition of persistency makes sense): it says now
MWa> (p.20) that "SPEC-FUN is like an extension". Why not "is an extension"? I
MWa> advocated above that we do not require that "the OF-SPECs are here
MWa> restricted to be simply names...". And I think that the concept of
MWa> different modes of parameter passing is well known - it will not hurt to
MWa> have the same modes of passing parameters as the modes of extending specs.
MWa> (especially, if an extension of the language would introduce new modes of
MWa> extending specifications.)
MWa> This generality does not cost anything and it doesn't prevent making the
MWa> default parameter passing persistent.
OK, I now think you're right.
MWa> Finally, the question about duplicate parameters is not addressed at all.
MWa> One should include at least a comment on how (and if) we intend to handle
MWa> specifications parameterized by two formal parameters both of which are,
MWa> e.g., NAT.
Another example would be PAIR[ELEM,ELEM]. Michel, if I recall
correctly we'd have to write PAIR[ELEM1,ELEM2] where ELEM2 is
essentially a translation of ELEM1?
*** Decompositional specs
DTS> Decompositional specs: See below (6). I think libraries of
DTS> decompositional specs are required. I see no reason to separate them
DTS> from libraries of requirements specs. At the moment I see no need for
DTS> a separate language of developments. What would this have in it that
DTS> we don't have already, except a way of saying which decompositional
DTS> specs originate from which requirements specs? This is important of
DTS> course, but maybe it is a matter of methodology and we have decided to
DTS> avoid making decisions about methodology.
MWa> It surprised me that DECOMPOSITION and SPEC are disjoint. In particular, if
MWa> a specification contains at least one DECOMPOSITION unit, it is itself a
MWa> DECOMPOSITION and not SPEC.
MWa> As far as I understand the sparse Part III, one cannot make a decomposition
MWa> unit U and write a specification 'extend U by XX'. I imagine that such a
MWa> specification would make sense - it requires a (separate) implementation
MWa> of U but allows one to extend it non-functionally by XX (it would be
MWa> something like the function from algebras for U to the classes of algebras
MWa> for XX (extending U).) Similarly, a parameterized specification could have
MWa> some parameters which are DECOMPOSITION units while others not (or not
MWa> yet). I imagine that this kind of mixtures of decomposition and other
MWa> (structured) specs do arise in the development when various components are
MWa> refined independently.
Don? Andrzej?
MWa> Unless you want to forbid this kind of things, the alternatives on p.19
MWa> should include
MWa> SPEC ::= ..... | DECOMPOSITION
MWa>
MWa> Does decomposition have to start at the top level? Is something either
MWa> fully decomposed (in the sense 'from the top') or is not decomposed at all?
MWa> Or else, can decomposition units be combined exclusively by means of
MWa> UNIT-FUNC and cannot be treated as legitimate specifications and used in
MWa> other specifications?
MWa> At the present, all the answers are yes; with this suggestion they are not.
MWa> But, perhaps, these are questions for the methodology group?
I think we need a sensible approximation for the tentative design
summary.
MWa> b. libraries of organizational specs?
MWa>
MWa> I assume that "organisational library" means the same as "a library with
MWa> decompositional specifications only".
Yes.
MWa> If decompositions can be combined with (treated as) other (structured)
MWa> specifications, there seem to be reason for providing separate concept of
MWa> organizational libraries.
no reason - otherwise please clarify.
MWa> Also, it seems unclear what the real difference between both would be. One
MWa> may have a DECOMPOSITION component which consists of a PART-DECL*
MWa> COMPOSITION at the top level but where all the UNIT-DECLs below are,
MWa> possibly huge and heavily structured, not-yet decomposed SPECs: one has
MWa> decided only a very general, top structure of the program but the whole
MWa> development (and decomposition) is still ahead.
MWa>
MWa> But I think that, from the methodological and, not least, tools' points of
MWa> view, it may be advantageous to be able to identify both the specs and
MWa> (sections of) libraries which have reached some level of decomposition.
MWa> This, however, is already present in the distinction between SPEC and
MWa> DECOMPOSITION.
MWa>
MWa> c. separate development language?
MWa>
MWa> This is one of the major issues to be discussed. I seem to recall that it
MWa> was raised earlier and postponed or classifed as a methodological issue. In
MWa> any case, such a language, which I think sould also incorporate the part
MWa> for visualizing the library organization and interconnections between
MWa> various specs, is certainly a separate issue and does not belong to X.
*** Abstract syntax:
DTS> Seems okay to me.
AT> Not obvious whether sort-embeddings give sub- or supersorts.
*** Other major issues:
DTS> A not-very-major issue is whether or not we should
DTS> have local/let declarations.
*
*
*
*
*
*** BASIC SPECIFICATIONS
*** 1:
DTS> Constraints can be regarded as special sentences.
But not in this institution, I thought?
DTS> Reachable = term-generated, I believe, so delete one -- otherwise it
DTS> sounds like two alternatives.
OK
*** 1.3
AT>> The signatures should include all the information needed for
AT>> determining parsing and well-formedness of terms.
OK, will now try first presenting many-sorted sublanguage and then
indicate everyhting that needs to be added for subsorts.
*** 1.4
AT>> Terminology: valuation is from variables to values; evaluation is
AT>> a partial function; the evaluation of a term may be undefined.
OK, will adopt.
*** 1.5:
DTS> What about induction corresponding to sort-generation constraints?
Good point!
*** 2:
AH> - page 12, line -2: Appendix 6 should be Appendix A
*** 2.1.1:
DTS> typo: last line of abstract syntax should be removed
OK
DTS> Compound sorts: Need to be explained better. Until you told me in
DTS> Cracow, I had no idea what these are. I think by far the easiest and
DTS> clearest way to explain is to mention an example like set(nat) with a
DTS> disclaimer about concrete syntax.
OK
BKB> Compound Names (I only understand them now)
BKB> Compound Sorts are rather ad-hoc really, especially their use in
BKB> *declarations* where I would only expect IDs (I dont know any language
BKB> that has something similarly complicated).
Well, how about LSL? I don't recall whether Jim Horning discussed
them in his talk at Oslo (I think so) but they're there in the CoFI
Catalogue... LPG has "something similarly complicated". ELAN has a
simple version. (But I don't know of others.)
BKB> Their introduction seems
BKB> to indicate a design problem elsewhere: instantiation or the general
BKB> rule that "same name (coming from different modules) is same thing unless
BKB> otherwise stated"; perhaps we should be self critical and re-introduce
BKB> dot-notation to distinguish in case of ambiguity. Note that dot-notation
BKB> (used in many languages) is a qualification at an applied occurrence
BKB> whereas compound names as proposed here are introduced at defining
BKB> occurrences and complicate the whole name space.
and provide conciseness!
BKB> Compound sorts are really very similar to parametrized sorts and would be
BKB> very much confused with these if they were introduced in an extension
BKB> (which is something many of us are waiting for); so they look like a
BKB> poor mans parametrized sorts, but are not really.
Michel?
AT>> I'd like to have compound names for functions and predicates, as
AT>> well as sorts. Then we get distinct names for the sorting function
AT>> when instantiating with various order predicates, e.g.,
AT>> sort[\leq], sort[\geq].
Fine by me! So maybe:
ID ::= id SIMPLE-ID ID*
I suggest that then translations should map IDs to IDs, rather than
the 0.92 rather clumsy abstract syntax for RENAMING.
*** 2.1.2:
DTS> Why not CONST -> CONST-SYMB by analogy with FUN-SYMB and PRED-SYMB?
OK
DTS> Predicates in function types: I think this is good except that it
DTS> should be restricted to two cases: (1) unary predicates and (2) n-ary
DTS> predicates when the function concerned is n-ary. This is actually the
DTS> way I read it but you said that you intended to allow n-ary predicates
DTS> for n>1 when the function concerned is more than n-ary; this seems to
DTS> invite confusing specs.
AT>> Ditto
DTS> I suggest the following changes to the
DTS> wording for clarification:
DTS>
DTS> 1st line: A *unary* predicate symbol ...
DTS>
DTS> 4th line: taken to be partial *with argument sorts being the argument
DTS> sorts of the corresponding predicates, and* an axiom is provided
OK - but probably best to require separate declaration, so purely an
abbreviation for an axiom (we presumably don't allow multiple
declarations of the same function with the same profile).
*** 2.2.1
AH> Instead of VAR-TYPE ::= var-type SORT
AH> I propose VAR-TYPE ::= var-type SORT_OR_PRED
AH> (It should be possible to use predicative subtypes in quantifications as
AH> it is in function profiles.)
AH> Similar questions pop of at other places, where SORT is appearing, e.g.
AH> in MEMBERSHIP.
AH> Actually, I would have prefered the possibility of defining
AH> predicative subtypes and using these anywhere, where types are allowed,
AH> instead of the current use of predicates.
This would be following Z, which allows set values to be used
everywhere the underlying types are allowed, I think. Do we want
this? It is certainly nice and uniform!
*** 2.2.3 Atomic Formulae
AH> I think that the rule for well-formedness of equations should be stronger:
AH>
AH> t1 = t2 is well-formed, if t1 and t2 are well-formed and
AH> there exists a least upper bound of sort(t1) and sort(t2) in the partial
AH> order induced by the sort embeddings.
AH>
AH> Example:
AH> sorts s1, s2
AH> sortembedding s1, s2 < s3
AH> sortembedding s1, s2 < s4
AH> const a : s1, b : s2
AH>
AH> The equation a = b is not well-formed,
AH> as s1 and s2 do not have a least upper bound.
AH> The two possible insertions of implicit coercions would have given
AH> two equations
AH> s1_s3(a) = s2_s3(b)
AH> s1_s4(a) = s2_s4(b)
AH> which might have different values.
Agreed!
* membership formula:
DTS> Maybe we should allow a unary predicate in
DTS> place of the sort? I'm not sure -- I'm thinking of the use of
DTS> predicates in types of functions. If we allow predicates to be used
DTS> as if they are sorts then perhaps we should try to take this further.
DTS> The meaning of t in P would be the same as P(t) , I guess.
Possibly.
TM> Sections 2.1.1, 2.2.3 and 2.2.4
TM> -------------------------------
TM>
TM> 1. What is the "sort of a term", a notion which is
TM> used in the definition of atomic formulas (2.2.3) ?
TM> In general, a term can have many different sorts, and there needn't
TM> to be a least or greatest sort.
TM> Look at the following example from Goguen and Meseguer,
TM> rewritten in the abstract syntax:
TM>
TM> basic-spec
TM> sort-decl B
TM> sort-decl A C sort-embedding B
TM> const-decl a total : -> A const-embedding b total : -> B
TM> const-decl b total : -> B
TM> const-decl c total : -> C const-embedding b total : -> B
Actually, only intending to allow embeddings between overloaded
symbols.
TM> Here, the term b has no greatest sort. In the dual example
TM> (sort-decl A C sort-decl B sort-embedding A C)
TM> the term b has no least sort.
TM>
TM> Of course, that a term has no unique sort is "harmlessly
TM> ambigous" from a semantical point of view, but it is
TM> not harmless at all when using "the sort of a term"
TM> in the definition of well-formedness of atomic formulas!
Agreed! Mea culpa!
TM> For regular signatures, Goguen and Meseguer (TCS 105, p. 252)
TM> define the least sort parse of a term.
TM> I assume in the sequel that this is meant by "the sort of a term"
TM> (even though CoFI signatures seem not have an ordering on
TM> the sorts at all. However, from the abstract syntax of a specification,
TM> such an ordering could be derived).
Not wanting to impose conditions such as regularity.
TM> 2. In the above example, equality is not transitive:
TM> from a=b and b=c, a=c does not follow, since a=c is not well-formed!
TM> This may be o.k., I just want to make it explicit.
TM> In the Goguen and Meseguer approach, the problem is solved by
TM> requiring the sorts of the terms of an equation only
TM> to be in the same connected component, thus a=c becomes well-formed.
a=b is really a=cast A b, whereas a=c could only be sorted as
cast B a=cast B c, exploiting implicit casts/projections.
Equality at a particular sort should be transitive, I think.
TM> In general, I feel that in the definition of equations,
TM> membership formulas and casts, it should only be required
TM> that the sorts and least sort parses of terms are in
TM> the same connected component. This view is also supported
TM> by the papers of Goguen, Meseguer, and Han Yan, while
TM> I don't know of any papers supporting the narrower notion
TM> of well-formedness (and proving that this yields an institution,
TM> see 3. below!)
Do you think that implicit casts/projections are needed? desirable?
TM> I know that in the Goguen and Meseguer approach, there is
TM> the problem for non-cohrent signatures that satisfaction is not
TM> preserved by model isomorphism, but this is not the case in the current
TM> setting (sort injections), if satisfaction of equations between
TM> terms with least sort parses in the same connected component
TM> is defined in an appropriate way.
Masybe also when the sorts of the terms have a least upper bound?
TM> I can offer to work this out in more detail, if wanted.
Please clarify first why implicit casts/projections are needed.
TM> Requiring coherence rules out the example, but coherence is not
TM> preserved by pushouts.
nor by innocent-looking extensions!
TM> 3. Why do you forbid to introduce subsorts of already declared
TM> sorts? For flat specs, sorts always can be reordered (just begin
TM> with the smaller sorts and then proceed to the bigger ones).
TM> Is it to forbide extensions like the following?
TM>
TM> extension of-spec ()
TM> basic-spec
TM> sort-decl pos
TM> sort-decl nat sort-embedding pos
TM> const-decl 0 total : -> nat
TM> fun-decl succ total : nat -> pos
TM> negation membership 0 pos
TM> ()
TM> basic-spec
TM> sort-decl pos zero
TM> sort-decl nat sort-embedding pos zero
TM> const-decl 0 total : -> zero
TM> const-decl 0 total : -> nat const-embedding 0 total : -> zero
TM> fun-decl succ total : nat -> pos
TM>
TM> But this extension is not ruled out:
TM> from the second paragraph above 4.3, I infer that I am allowed
TM> to introduce the sort and constant symbols once more in the extension.
TM> If this is not true, the paragraph should be made more precise.
It was not intended to be allowed.
TM> The problem with this extension is: the axiom
TM>
TM> negation membership 0 pos
TM>
TM> cannot be translated to the extended signature, since the
TM> least sort parse of 0 in the extended signature is zero,
TM> and zero is not included in pos, so the axiom is not well-formed
TM> in the extended signature.
TM>
TM> Han Yan examines these membership formulas (=sort constraints)
TM> in his PhD thesis and proves that they are (part of) an institution.
TM> But therefore, he defines
TM>
TM> membership t s
TM>
TM> to be well-formed if s and the least sort parse of t are in the same
TM> connected component.
TM> If the notion of well-formedness is defined to be narrower
TM> than this, then I guess that signature morphisms have
TM> to be restricted to those preserving regularity,
TM> and may be this condition is implied by forbiding to
TM> introduce new subsorts and forbiding to re-introduce
TM> sorts in extensions.
TM> But forbiding these two removes a useful facility from the language.
How useful is it to introduce zero and pos above? Wouldn't it be just
as easy to use predicates?
*** 2.3:
DTS> There is an alternative to forbidding variables of the specified
DTS> sorts: in the terms generating a sort s, one could forbid variables of
DTS> the sort s but allow variables of the other sorts that are being
DTS> constrained at the same time. This allows mutually generated sorts.
DTS> I'm not sure which of these I like more/less; both seem like fairly
DTS> gratuitous generalizations of the case of constraining just one sort.
Andrzej?
*** 2.6
AT>> Why is a TYPE-DEFN-SCHEMA called a schema? Just a TYPE-DEFN?
OK by me.
AT>> Perhaps better to put CONST together with CONSTRUCT.
OK
*** STRUCTURED SPECIFICATIONS
*** 3:
DTS> The parameters may have fixed parts ...: I have yet to be convinced
DTS> that this is a good thing.
The idea was merely to allow e.g. NAT occurring in a formal parameter
to be renamed during instantiation.
DTS> Next paragraph: the semantics of a structured spec is simply
DTS> *a signature Sigma together with* a class of ordinary, unstructured
DTS> models *over Sigma*.
OK
*** 4.1
TM> LIBRARY-SECTION ::= LINEAR-LIBRARY | LINKED-LIBRARY
TM> has to be changed to
TM> LIBRARY-SECTION ::= LINEAR-SECTION | LINKED-SECTION
DTS> Typo in abstract syntax, 2nd line: LINEAR-SECTION, LINKED-SECTION
DTS> (also in appendix)
Thanks.
TM> What is the meaning of the following linked library:
TM> library linked-section
TM> spec-defn funny
TM> translation
TM> renaming sort-map S T sort-map T S
TM> funny
TM>
TM> Of course, S and T do not occur in funny literally,
TM> but since we do not know the value of funny in advance,
TM> I don't see any rule which could forbid writing a specification like this.
Starting from funny being the empty-spec, the syntactic fixed-point
would quickly converge either to the empty-spec, or to an error,
depending on whether symbols in renamings have to exist or not.
*** 4.2:
DTS> The first sentence is unclear. How about: ... they are required to be
DTS> `closed' except that references are allowed to symbols in the local
DTS> environment.
OK
DTS> Renaming/hiding/exporting: This seems confused. In the case of
DTS> renaming, are we thinking of derive or translate (ASL terminology)? I
DTS> thought we were thinking of translate, and then probably the signature
DTS> morphism used should be required to be injective. If this assumption
DTS> is correct, then: it's true that a signature morphism is required in
DTS> each case, but in the case of hiding and exporting the direction is
DTS> the opposite of that required for renaming. And anyway, in the case
DTS> of hiding and exporting, it's clear that there will be symbols that
DTS> aren't mentioned -- that's the whole point! -- and the signature
DTS> morphism shouldn't be "completed" in either case.
AT>> Ditto
The conclusion seems to be here that we should have one construct for
translation, involving renaming only (identity on unmentioned symbols)
and another construct for derive (both exporting or hiding allowed).
An option would be to allow exported symbols to be renamed.
DTS> For clarity here and elsewhere, I think the text should mention the
DTS> direction of the signature morphism. I think the following is a
DTS> complete list.
DTS> renaming: what-we-have -> what-we-want
DTS> hiding/export: what-we-want -> what-we-have (always inclusion)
DTS> instantiation of param specs: formal -> actual
DTS> reduct in decomp specs: what-we-want -> what-we-have
OK
DTS> Hiding/exporting: If there is a compound sort like set(nat), what
DTS> happens when one hides just nat? Or when one exports just nat? Can
DTS> one hide/export just set? (I guess not.)
My understanding was that hiding nat would hide set(nat), but not vice
versa. Michel?
DTS> PERSISTENCE, FREEDOM: It might be clearer (not sure) to replace
DTS> PERSISTENCE in OF-SPEC by persistent?, and similarly with FREEDOM in
DTS> BY-SPEC.
OK
AH> It should be possible to distinguish between overloaded symbols
AH> in renamings, hidings and exportations, e.g. by using the following syntax:
AH>
AH> CONST_MAP ::= const-map CONST DISAMBIGUATED_CONST
AH> FUN_SYMB_MAP ::= fun-symb-map DISAMBIGUATED_FUN
AH> PRED_SYMB_MAP ::= pred-symb-map DISAMBIGUATED_PRED
AH> SYMB ::= SORT | DISAMBIGUATED_CONST | DISAMBIGUATED_FUN | DISAMBIGUATED_PRED
AH> DISAMBIGUATED_CONST ::= disambiguated_const CONST CONST_TYPE?
AH> DISAMBIGUATED_FUN ::= disambiguated_fun FUN_SYMB FUN_TYPE?
AH> DISAMBIGUATED_PRED ::= disambiguated_pred PRED_SYMB PRED_TYPE?
I see that this is more general, but would it be used? Also, it
suggests generalizing function embeddings to allow declaration that a
function embeds another function of a different name, whereas just
translating (compound) IDs automatically preserves overloading.
BKB> Of course I know what an import, a union or an extension are.
BKB> My point here is that these concepts are not defined and their colloquial
BKB> meaning may be confusing.
BKB> All I personally want is to be able to compose a requirement specification
BKB> piece by piece. If I cannot do this with a union (since I have to repeat
BKB> the resp. signature), can I do it in an extension?
Yes.
AT>> "free" should mean free rather than freely-generated, since the
AT>> generatedness can be specified separately.
OK (I guess).
*** 4.3:
DTS> Extension is implicitly required to be persistent: I don't recall this
DTS> decision. It rules out two things that are normally given as reasons
DTS> for wanting parametrized specs:
DTS> 1. abbreviating common patterns of use of spec-building operations
DTS> (these will not always be persistent)
DTS> 2. Larch-style traits abbreviating properties to be imposed on
DTS> existing operations, such as associativity
AT>> Ditto
OK, I'll put the option back in.
DTS> Persistently-extended parts of the parameter are regarded as fixed: It
DTS> isn't quite clear what "persistently-extended parts" means. Which
DTS> spec-building operations preserve the property of being a
DTS> persistently-extended part? E.g. hiding, renaming? Presumably not
DTS> non-persistent extension. If renaming is one such, then why is
DTS> renaming the thing that is forbidden in instantiation?
In fact Michel proposed a separate construct, but I was hoping to be
able to economise...
DTS> Do we really want partial instantiation? What kind of thing is a
DTS> partially-instantiated spec function? A spec or a spec function?
The distinction isn't context-free.
DTS> This point must at least be mentioned. It seems to me that we can
DTS> always use total instantiation:
DTS> fun F(X) = G(A,X)
DTS> rather than
DTS> spec/fun? F = G(A)
Michel's proposal was (I think) to write e.g.
fun G(X,Y) = ...
fun F(X) = ...G(B for Y)...
fun H(Y) = ...G(A for X)...
allowing the partially-instantiated G to be extended etc., but
insisting on the remaining parameter(s) being mentioned in the
declarations of F and H.
With positional parameters one writes instead of the above:
fun G(X,Y) = ...
fun F(X) = ...G(X,B)...
fun H(Y) = ...G(A,Y)...
The difference doesn't seem that big. Positional parameters seem to
have a simpler syntax and semantics, but have pragmatic drawbacks
(e.g., when one realizes that a further parameter should be abstracted
from an existing function body). I'll try and make the AS so that we
can change this easily.
DTS> The situation is *not* analogous to that of functional programming
DTS> languages: because of the decision not to extend to higher-order,
DTS> there has to be a rigid distinction between functions and
DTS> non-functions.
In the semantics, certainly; but the context-free syntax need not make the
distinction explicit.
*** DECOMPOSITIONAL SPECIFICATIONS
AH> I would prefer the term "architectural specifications" rather than
AH> "decompositional specifications". Why do you not like the former?
It appears that it was (badly) misleading for those working with
reactive systems.
AH> Other alternatives may be
AH> "architectural decomposition (specification)" or
AH> "architectural structure (specification)"
AH> [Bernd: I think that these specifications correspond to
AH> Jan Peleska's architecture decomposition trees]
If so, we might change back.
AT>> "Decompositional" seems OK.
All: please react if you have arguments or strong feelings concerning
this terminology.
BKB> II / III
BKB> Structured and decompositional specs still need a lot of work and are
BKB> definitely not in shape to be made public. They do not interrelate at all.
I agree. Somehow the decompositional specs seem half-way towards a
development language.
BKB> Eventually, we will need instantiations of specifications that depend on
BKB> previous (algebra) parameters in a decompositional spec, as specs for subsequent
BKB> parameters. How can I get this? (it was promised in Munich)
Only in an extension, as far as I recall
BKB> Andrzej claims these are isomorphic to certain param specs (as now in II).
BKB> So why not define some kind of implicit coercion?
BKB> I am expecting Andrzej to make a proposal here (after some discussions we had).
Fine.
BKB> Just to keep the record accurate: I (and others) claimed we do not need
BKB> parametrized specs (i.e. specs parametrized by specs) if we have
BKB> specs parametrized by algebras.
BKB> Now we do not have these (yet?) ...
We need parametrized specs as such, for various reasons - the major
one for me being that we are trying to make our language resemble
previously-USED languages. In Munich it seemed that we might indeed
get something like parametrized specs as a special case of something
more general (the abstract syntax of Saturday afternoon); on Sunday
and at Dagstuhl it became clearer that while this might be done in the
semantics, the constructs should be kept separate in the syntax.
BKB> I still do not understand II and especially III, sorry (i was not at Dagstuhl;
BKB> but what about all those who havent even been at Munich?
BKB> [=> Michel: could I get some examples, especially for III, even if they are
BKB> with you preferred "working" concrete syntax??]
I think that Michel's original note on Structuring is adequate.
BKB> Definitely, DECOMPOSITIONS must be in the library somewhere; where else
BKB> can they manifest themselves??
During development?
*** 5:
DTS> In the first paragraph I think it is clearer to replace
DTS> development of such models -> task of developing such models
OK
*** 6.
DTS> Typo in abstract syntax for UNIT-FUN-DECL: SPEC+ is missing
AH> Is the syntax for UNIT-FUN-DECL right? I would have expected formal
AH> parameters.
Thanks. Sorry.
DTS> I agree with Andrzej that there should be a way to name
DTS> decompositional specs. One argument is that designs and realizations
DTS> of specs are at least as important as units of reuse as requirements
DTS> specs are, probably much more important.
DTS>
DTS> We can choose to have a single heterogeneous library (so declarations
DTS> of requirements specs mixed with declarations of decompositional
DTS> specs) or separate libraries, perhaps even requiring the requirements
DTS> phase to be complete before the decompositional phase starts. I think
DTS> allowing a mixture is harmless and simpler; any restriction is a
DTS> matter for methodology. So all we need to do is to add
DTS> LIBRARY-ITEM ::= ... | DECOMP-DEFN
DTS> DECOMP-DEFN ::= decomp-defn DECOMP-NAME DECOMPOSITION
DTS> DECOMP-NAME ::= ID
DTS>
DTS> The fact that this is a long forward reference (from 4.1 to 6) and the
DTS> fact that libraries are then not merely about requirements specs
DTS> suggests that libraries should perhaps come in a separate section,
DTS> after decompositional specs.
OK, I plan to try this in the next version.
DTS> By the way, shouldn't the abstract syntax indicate what the main
DTS> (top-level) phrase class is? I guess it should be LIBRARY.
OK
DTS> Finally, what about local or let declarations? E.g. (concrete syntax)
DTS> SPEC ::= ... | let LIBRARY in SPEC
DTS> (and similarly for SPEC-FUN and DECOMPOSITION) and/or
DTS> LIBRARY-SECTION ::= ... | local LIBRARY in LIBRARY-SECTION
I'd expect libraries to be implemented as separately-parsed text
files. Allowing libraries nested in SPEC etc. might hinder this.
What other languages allow this? - apart from ML, of course... :-)
BKB> -------------
BKB>
BKB> what we should achieve:
BKB>
BKB> - separate the library issue (to include structured and decompositional specs),
BKB> perhaps at the end in a separate chapter (Peter agrees here)
BKB>
BKB> - tie decompositional specs in with structured specs; this is very
BKB> important. Note that (structured) specs are used to "type" the algebras. I
BKB> still claim I need some form of spec parameterised by algebra for this,
BKB> particularly in the case of dependent parameterised decompositional specs
BKB> (i.e. Pi-specs); consider the example of ELEM first (where the actual param
BKB> is an algebra) and then LIST of ELEM (where ELEM is now an algebra!);
BKB> consider also the eventual extensions to higher-order.
Your concern for the extensions to higher-order is of course valid.
But I personally wouldn't like it to make the first-order language
more complex and less acceptable to the community.
BKB> I understand this kind of spec was deleted in Dagstuhl; however, Andrzej
BKB> claimed in Munich (and still agrees) that there is a kind of "coercion"
BKB> (i.e. isomorphism) from LIST of ELEM, i.e. a spec parameterised by algebra,
BKB> to a structured spec. Of course, such a spec has to fulfill certain
BKB> conditions, I suppose persistent extension w.r.t. the parameter is (the
BKB> only?) one.
BKB> We should achieve this, ie. the use of a parametrized (structured) spec
BKB> that has an algebra as an actual parameter, with the corresp. "coercion"
BKB> inserted implicitly.
We still need parametrized specs that do not name algebras explicitly
at all, I think.
BKB> - I reacted (too) strongly to the *named* parameter association in
BKB> parametrized structured specs. The reason is that I would very much like
BKB> both parametrizations to be similar. For example when using LIST as above,
BKB> I would like to have a syntax like LIST(ELEM) just as for decompositional
BKB> specs.
It isn't clear to me that this is in itself a good thing.
BKB> I would also like to treat partial parametrization as a case of
BKB> higher-order (which it is after all); I see no reason why not. I do know
BKB> that the issue is the fitting morphisms, and how to write as little as
BKB> possible. But please: let us have a language with few concepts that the
BKB> user can find in several instances perhaps and reuse his intuition (perhaps
BKB> I feel so strongly because of the Ada monster experience, and rightly
BKB> so!!).
As above: Your concern for the extensions to higher-order is of course
valid. But I personally wouldn't like it to make the first-order
language more complex and less acceptable to the community.
BKB> - I do not understand the issue about the "fixed parameters" at all. I know
BKB> that one wants to use NAT and not have to mention it in an actual
BKB> instantiation. But this means either
BKB> - NAT is visible in the environment of the definition, is *used* in the
BKB> parametrized spec under consideration and thus is either automatically
BKB> made available in the context of instantiation (transitive import) or
BKB> a requirement is made, that it is visible (this can be checked)
BKB> - NAT is an instantiation, say LIST(NAT), where NAT is a previous
BKB> formal parameter; I just realize that this is not possible since
BKB> formal parameters are only names.
Michel?
BKB> - I do not like compound sorts; see comments above. We should find a better
BKB> solution.
To me they seem a neat and simple way of linking the names of
functions and predicates to the sorts in their profiles - clearly
inspired by higher-order frameworks, but with a first-order semantics.
---- --------------------------------------------
\ / | Peter D Mosses <pdmosses@brics.dk> |
CoFI | Common Framework Initiative - Coordinator |
/ \ | WWW URL: http://www.brics.dk/Projects/CoFI |
---- --------------------------------------------