Re: Tentative Language Design Summary version 0.93 [600 lines!]

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

Dear Peter and other X-people,

[I'm forwarding this uncut, despite its length, as it contains many
useful technical observations of relevance to the tentative language
design and semantics.  The main topics are:

* Name
* Subsorting
* Cyclic sections
* Parametrized specifications
* Compound identifiers
* Architectural specifications

--PDM]

Much apology for another week or so of silence: after coming back to
Warsaw, I managed to stay only one day in the office and then some
nasty illness kept me at home, not really being able to work even
there. Things got better, but still i am only able to pay a very brief
visit to the office. Sorry!

So, the comments below are written on the basis of what I read over a
week ago or so, without taking into account anything which might have
came in later. In particular, a completely new version of the
description might have appeared by now [no, not yet - although
Michel's new note on parametrization has appeared, and coming real
soon now should be a new version of the note on subsorting and an
example of the use of architectural specifications - also some
promised reactions from Don, I hope?  --PDM] and my comments are out
of date: please, use your own judgement to what extent they are still
valid... Also, mistakes, typos [I've taken the liberty of changing
some occurrences of "weak" to "week" :-) --PDM] and inaccuracies are
quite likely, but I hope the main points are possible to get out of
what follows...

Anyway, here are some points:

Major issues:
=============

NAME: I still like the name ALCOL most (or dislike it least).

[Have you also seen the proposal of CASL, which several people seem to
actually like? --PDM]

SUBSORTING ETC:

I like the new (w.r.t. to version 0.92) way to present and introduce
subsorts in the definition of X --- this is much more readable now,
and allows one to pretend they do not affect the language if one
wants to use many-sorted case only.

I very much appreciate the study note by 6 authors; this cleared out
some of the doubts I had after reading the language description
version 0.93. In particular I buy the basic ideas: implicit
identification of overloaded symbols according to the subsorting
relation, the lack of extra assumptions on the signatures,
predicative subsort definitions etc.

I must say though that some of the remarks in the note go contrary to
my understanding of the concepts and methodology, for instance the
insistence on the use of the term "refinement" for building a new
specification using an old one --- these however is of no consequence
for the language design.

More importantly, the note gets technically rather involved at places,
and i would hate to have to explain all the intricacies to an average
user of our formalism. I guess one thing which we are not able to
avoid is that the "true" terms and sentences have to be fully-sorted
(have I used the right terminology here?), while the actual syntax
should allow at least for implicit insertion of sorts and subsort
insertions. I think we should strive as much as possible at hiding
this necessity from the user, thus helping the user to read
specifications as s/he writes them. We cannot quite achieve this:
well-formedness of terms and formulae must depend on the context, for
instance, adapting an example from the note, a = b is well formed
under the declarations:
	sorts s1, s2 < s
	const a: s1, b:s2
but is no longer well-formed if we add a declaration
	sort s' > s1, s2
because of the possibility of ambiguous parsing, which may lead to
different semantics.

I'm afraid that examples like this bother me a bit (the need to
consider this particular equation as ill-formed is linked to the fact
that arbitrary injections are allowed as a semantical counterpart of
subsorting relation, rather than for instance just inclusions --- the
latter would lead to the identification of overloaded symbols with
connected profiles, rather than with ordered by subsorting profiles,
as now). Anyway, I think I am prepared to live with this (and explain
this if necessary).

However, what bothers me even more is that the meaning of a formula
may depend on the context. I understand that in the current proposal
this is due to the use of "weak monotonicity" rather than
"monotonicity" as a semantic requirement on the overloaded and related
partial operations (weak monotonicity implies that a function with a
supersort profile may be more defined on the arguments from a subsorts
than the same function with the subsort profile). The arguments for
"weak monotonicity" the authors give (p.11 of the note) do not
convince me. [In fact those same authors have since decided that weak
monotonicity would be better left to an extension language. --PDM]
I think some of them result from the confusion of
internal concepts of the specification formalism (subsorting) and
external, development level concepts (implementation), perhaps common
for OO approaches; but from my point of view, methodologically this is
just wrong. I really can see no need to express "implementations with
capacity constraints" as subsorts.  In the other cases, it is easy and
more appropriate in my view to name the two functions differently, and
express the relationship between them by an axiom. Very, very
informally: I would like to identify two functions with different
profiles only if they really represent the same way of computing
things and indeed may be implemented in the same way; otherwise it
seems wise to name them differently.

At a more technical level, it feels very bad to me that definedness,
equalities and predicates "do not commute with subsort injections".
This makes some specifications look very misleading. For instance, it
bothers me that a specification like:
	enrich ( sort s, const a:s, axiom not D(a) )
	by sort s' > s, axiom D(a)
is consistent! I believe that this might also be very misleading to
the "average" user.

I also believe that replacing weak monotonicity by monotonicity
should lead to a somewhat easier technicalities behind implicit term
expansions etc.

To sum up: I like the current proposal on subsorting, but please
strengthen the "weak monotonicity" requirement so that functions
would be required to "fully commute" with subsort injections.

[This is precisely what will be in the next version! --PDM]

Aha, two small issues around here:
First, I do not like the use of the same symbol cast for subsort
injections and projections. It seems to introduce more ambiguity than
necessary into terms. For instance, given
	sorts s1 < s2 < s3
	const a: s1
cast a s2 may intuitively mean either cast (cast (a qua s1) s3) s2 or
simply cast (a qua s1) s2. I guess this is somehow prevented by a
condition restricting projection and injection casts occuring next to
each other. Since we treat projections and injection quite
differently, I suggest the use of two different symbols here.

And then, I guess I am missing some technicality here, but I do not
like the restriction which seems to prevent an appropriate injection
cast to be inserted before the use of qua. At least for me, this
would be a typical use of sort assertions, to implicitly invoke a
subsort inclusion.

Aha: and I can see no additional harm in allowing declarations of the
subsorting relations (they would be declarations, not axioms!) to be
separated from the declarations of the sorts themselves.

CYCLIC SECTIONS (RECURSIVE SPECIFICATIONS):

I have a number of serious technical doubts here, as I already
mentioned in Dagstuhl. First, the semantics certainly cannot be
defined as naively as the current text hints at: we cannot just start
iterating form the empty specs, since then typically recursive
specifications will turn out ill-formed at the first iteration.  [The
intention was to disregard well-formedness until the iteration had
terminated. --PDM]  A possible solution is to first do a purely
syntactic iteration, computing signatures of specifications only, and
then work with model classes (as constrained by axioms) over the
already fixed signatures.  However, given the constructs as we have
them now, I am not sure if the syntactic iteration would always
terminate and the signatures can in fact be determined: recursion may
lead to infinite signatures, I guess, and perhaps even more
dangerously, given the renaming mechanism for compound identifiers, it
may lead to infinite compound identifiers (which is outside the syntax
as we have it now). Of course, we could try to identify and forbid
such dangerous recursive definitions, but this seems ugly.

Moreover, my guess is that at the semantic level there is very little
to gain form various forms of recursion. In particular, some
intuitive dependencies between specification expressed by axioms
referring to their components would in fact disappear in the semantics.
For instance:
	SP1 = hide a in (enrich SP2 by sort s, const b: s, axiom a=b)
	SP2 = hide b in (enrich SP1 by const a: s, axiom a=b)
Now, the semantics of SP1 and SP2, if any, must be given by dropping
a from SP1 and b from SP2, and any dependency between the two specs
is lost. Well, this is perhaps not a very good example. I guess what
I want to indicate here is that if there is any dependency between
two specifications, then at least their mutually dependent components
must occur in both, and then somehow we are forced to put this
components in a single specification anyway. What would the recursion
be here for then?

I guess my current tendency would be to drop cyclic sections from X
entirely. Can somebody sketch a plausible example where this would
really be needed and sketch the semantics at least for this example?

[I'll try!  I intended to write something on this last week, but the
more urgent issues of subsorting, parametrization, and architectural
specifications took the time... --PDM]

PARAMETERIZED SPECIFICATIONS:

See below for some minor technical questions, but in general I do not
care much.

I have no opinion about whether "positional" or "by names" convention
for attaching actual to formal parameters should be used. Perhaps this
can be postponed even to a concrete syntax? It should be stressed that
this is different from the syntax for UNIT-FUN-INST (instantiation of
parameterised components to components in architectural
specifications, see sect.8) where there is no choice, and we are
bound to positional notation since no names for formal parameters are
provided, only their specifications.

COMPOUND IDENTIFIERS:

I guess the idea is simple enough, in spite of a number of technical
decisions and constraints that still have to be discussed (see some
points below, for instance --- I *hope* all these can be resolved
somehow). If we stick to the decision to rely on the simple ASL-style
sharing strategy (sharing by name plus profile) then this seems to be
the simplest mechanism to avoid constant use of explicit renaming in
many practical examples, I think.

ARCHITECTURAL SPECIFICATIONS:

I think the way things are stated there now makes some sense, and
allows some basic cases to be expressed as required.

****** WHAT FOLLOWS IS NOT A COMMENT DIRECTLY ON THE LANGUAGE SUMMARY,
BUT YET ANOTHER ?DELICATE? ATTEMPT TO CHANGE IT TO WHAT I WOULD LIKE
EVEN MORE, AS FOR EXAMPLE CALLED FOR BY BERND A FEW WEEKS AGO. SORRY,
I CANNOT QUITE RESIST :-) IF YOU FEEL THIS IS NOT WORTH DISCUSSING
ANY MORE, SKIP TO THE NEXT SEQUENCE OF FEW ASTERISKS...

If you read on here, let me state once more that the result only
approaches my favourite solution, and I believe it does not allow the
user to express some of the rather typical dependencies in the most
natural way (see a simple example from Bernd's message last week ---
has somebody undertaken to express something like this in the current
X?).  Just to remind you: we (at least Don, Bernd and me) have been
proposing from the very beginning that individual algebras (okay, we
give up their explicit definitions from scratch, in form of some
"abstract programs" or whatever they were called when they were voted
out of the formalism) be present in X; currently they only sneaked in
as names of units in architectural specifications.  Then it should be
only natural to introduce specifications paramaterised by algebras.
Those specifications parameterised by algebras could be coerced to
parameterised specifications (specifications parameterised by
specifications, perhaps furthermore with an independent pushout-style
instantiation mechanism). Just as current parameterised specifications
of X, these would be considerably less expressive than a full
lambda-abstraction style parameterised specifications in ASL-style. On
the other hand, those specifications parameterised by algebras could
also be easily coerced to specifications of parameterised components,
as they are now present in architectural specifications. Finally, of
course, we still should be able to instantiate specifications
parameterised by algebras by providing an actual parameter (which, in
the absence of any explicit algebra definition language, could only be
some other algebra name declared to fit some specifications, or an
algebra expression built as COMPs in architectural specs now).

However, I would not like to allow for direct coercions in the
opposite directions (between parameterised specifications,
specifications parameterised by algebras and specifications of
parameterised components in an arbitrary direction) on the basis of
trying o keep distinct concepts distinct.

For instance, trying to recall what I sketched at the meeting in
Munich:

Specifications parameterised by algebras would be introduced by:

ALG-PAR-SPEC ::= alg-par-spec SPEC+ BY-SPEC

and earlier adding:

LIBRARY-ITEM ::= ... | ALG-PAR-SPEC-DEFN
ALG-PAR-SPEC-DEFN ::= alg-par-spec ALG-PAR-SPEC-ID ALG-PAR-SPEC
ALG-PAR-SPEC-ID ::= SIMPLE-ID

The idea is that
	alg-par-spec (SP1 ... SPn) BY-SPEC
defines a function that takes algebras A1, ..., An in model classes
of SP1, ..., SPn, respectively, and maps them to the class of all
algebras that model
	extension (of-spec SP1 ... of-spec SPn) BY-SPEC
and in addition expand A1, ..., An (I guess a semantics could be
given without the use of extension and an explicit reference to
reducts of the resulting models).

We could also think here about various operations on ALG-PAR-SPECs
directly (for instance pre- and postcomposing them with reducts along
signature morphisms --- but some of them may conflict with the later
use of the results for coercing into parameterised specifications with
pushout-style semantics of instantiation).

Then we would have a different clause for parameterised specifications:

PAR-SPEC ::= make-par-spec ALG-PAR-SPEC

The idea here is of course that such a parameterised specification
semantically denotes a function which given a class of models (which
is a subclass of the class of models of a specification of algebra
parameters for ALG-PAR-SPEC) yields as a result the union of the image
of the function ALG-PAR-SPEC denotes on the given model class. I
believe that now
	make-par-spec (alg-par-spec (SP1 ... SPn) BY-SPEC)
has exactly the same semantics as
	par-spec ( () SP1 ... () SPn ) BY-SPEC
and an appropriate shorthand for this expression can be provided by
the concrete syntax of X (or even as an alternative form in the
abstract syntax). Note that I have assumed no persistency requirement
here: persistency of
	make-par-spec ALG-PAR-SPEC
would mean that the function defined by ALG-PAR-SPEC yields non-empty
sets on all arguments.

Now, how the functions on classes of models (with fixed signatures,
of course) is used to define the semantics of instantiation is a
different matter. For instance, if we want, the pushout semantics may
be used, since so far we have preserved the property that the
arguments are always included in the results.

Furthermore, we would need an extension to the ways specifications
are defined:

SPEC ::= ... | ALG-PAR-SPEC-INST
ALG-PAR-SPEC-INST ::= alg-par-spec-inst ALG-PAR-SPEC-NAME COMP+

The semantics is obvious, I hope. Note that we refer here to COMPs as
defined in architectural specifications, since they already provide a
rather rich language for defining algebras using units (algebras
and parameterised components) present in the unit environment.
Implicitly this means that in X as proposed now, instantiation of
such specifications parameterised by algebras may only happen in
architectural specifications (in the specifications of units).

To make this work smoothly, I would allow explicit parameter names in
specifications of parameterised units in architectural specifications,
using the following new clause:

UNIT-FUN-SPEC ::= unit-fun-spec PARAM+ UNIT-SPEC
PARAM ::= param UNIT-NAME SPEC
(I would allow here visibility of parameter unit names from left to
right for parameter unit specifications.)

The coercion form specifications parameterised by algebras to
specifications of parameterised units may be now easily expressed:
given:
	APS = alg-par-spec (SP1 ... SPn) BY-SPEC
we can form
	unit-fun-spec ( (param X1 SP1) ... (param Xn SPn))
		alg-par-spec-inst APS (X1 ... Xn)
and an appropriate equivalent "derived form" may be provided by
either the abstract or concrete syntax of X.

Aha, it should also be only natural then to allow references to
algebra components in specifications, by means of "dot notation", as
advocated by Don and me, and despised by so many others :-) but as
seen above, the other concepts may be introduced without it, at the
price of having to use disjoint specifications for various algebra
parameters and always include the parameters in the results, if
everybody insists.

****** NOW BACK TO THE COMMENTS ON THE CURRENT LANGUAGE SUMMARY

Less important things:
======================

--- p.7 and then p.12, about constraints: do we need constraints in
their full generality, with a signature morphism component? Certainly
the constraints that the language constructs allow one to express do
not contain this component. If I recall right, we need this component
only to translate constraints as sentences along non-injective
signature morphisms (I had an example showing this ages ago ---
perhaps in the context of order-sorted signatures some further
complications arise even when translating constraints along injective
morphisms). Anyway, this seems peripheral enough for the design of the
language that perhaps should be even reduced to some small footnote,
and constraints may be left without the explicit fitting morphism.

Then, given a signature $\Sigma=(S,TF,PF,P)$, a $\Sigma$-constraint
might simply consist of a set of sorts $S''\subseteq S$ and operations
$TF''\subseteq TF$ and $PF''\subseteq PF$, with the obvious semantics:
the carriers of the sorts in $S''$ are generated by the operations
$TF''$ and $PF''$ from the carriers of the other sorts (those in the
arities of the operations in $TF''$ and $PF''$). This requires a
footnote that a slightly more general form of constraints, including a
morphism fitting $\Sigma$ into a current signature, is required to
ensure the correct translation of constraints along arbitrary
signature morphisms; this is not needed for the semantics of our
X formalism though.

--- p. 11, sec.1.2: notation on models: I do not like the notation
|s^A| for the carriers, and $f_A$ for the operations. What I use is
$|A|_s$ and $f_A$ (which conveniently gives a notation for the
many-sorted carrier of the algebra as $|A|$). Neither notation is very
uniform -- perhaps we should consequently use something like $s_A$ and
$f_A$; or $s^A$ and $f^A$?

--- p. 14, sec.2.1: some small issues related to structured
identifiers do not seem well-justified to me. First, why do we
require that identifiers that are components of compound identifiers
are to be necessarily declared around? I might want to use a naming
mechanism (similar to that of a 2-level grammar) to facilitate some
renaming of entire specifications, even if I choose no specific sort
or symbol to play the role of a "leading parameter". For instance, I
might want something like
	SPEC = sorts s1(version), s2(version)
	       function f(version) : s1(version) -> s2(version)
	       axioms ...
and then
	SPEC1 = SPEC rename (map version to one)
	SPEC2 = SPEC rename (map version to two)
etc. I can see no reason to exclude this, once we have compound
identifiers.

Also here: it is not clear to me what exactly this formulation
excludes: I understand that in  sets(elem)  elem is required to be
declared around, but not sets. What about sets(sets(elem))?
sets(elem) and elem must be declared around? I certainly want to be
able to write a spec of sets(elem) then use it to produce
sets(sets(elem)) and perhaps eliminate sets(elem), so as to work with
elements and families of their sets only (I believe it would be
possible to find algorithms working over such a data type...).

Finally, about translation and hiding: I am not sure what exactly is
said here. First, about translation: renamings seem to be allowed to
map (compound) identifiers to (compound) identifiers. I understand that
this is to extend somehow naturally to arbitrary compound identifiers
including occurrences of of the ones in the domain of the renaming.
So, for instance, mapping elem to nat induces translation of
sets(elem) to sets(nat). What about mapping sets to lists? Is this
allowed in such a context? If so, does this induce then a translation
of sets(elem) to lists(elem)? Then, is mapping of sets to, say,
lists(blah) allowed?

My proposal here (perhaps consistent with the intention of the text)
would be to allow extension of the mappings to compound identifier
only "upwards", thus mapping sets to lists would not induce a
translation of sets(...) to lists(...). Otherwise all kinds of
problems may arise.

Then about hiding: I don't see why hiding an identifier should result
in hiding all the identifiers that contain it -- this is linked to
the requirement discussed above that all the component identifiers
are to be declared around. If anything, i would allow hiding sets as
a shorthand for hiding all compound identifiers which start with sets.

--- p.17, 2.4:
The intended interpretation (of a type definition group) is as a
freely-generated *?persistent?* extension: ...

I do not think we want to allow type definitions to constrain
underlying data types, that are not declared in the given type
definition.

--- p.24, 6.1: Are items from one section to be visible in another
(subsequent --- linear visibility) sections at all? Please mention
something about (linear) visibility of items between sections.

--- p.24, 6.1, the last paragraph, the last sentence: "Each symbol
used in a library item has to be already declared in the local
environment at its point of use". This states the linear visibility
within (basic) specifications. If this is so (I cannot recall if this
really was the decision we reached in Munich and cannot check this
easily when writing this comments at home), the problems I mentioned
above for the treatment of subsorting, with dependency of formulae and
terms on the context become even more explicit. Now, the meaning of
an axiom may depend on the exact position of this axiom in a basic
specification. For instance, if i get things right, the following
specification would be consistent:
	sort s, const a:s, axiom not D(a), sort s' > s, axiom D(a)
Ughhh!

--- p.26, 6.3: parameterised specifications.

Why the fitting morphisms is required to be injective? I believe
there would be some practical examples where non-injective morphisms
occur naturally.

There is nothing here about the intended meaning of instantiations of
parameterised specifications. I understand that this is given by the
classical pushout approach, modulo the extra tricks of renamings
extending to compound identifiers.

I am happy to see that "partial instantiations" and "fixed parts of
parameters" disappeared in this version of the proposal. In my view
the former may be always expressed using the current full
instantiation mechanism without extra trouble, and the latter may be
deferred to some methodological directives.

Minor comments:
===============

--- p.2, abstract: remove "full": in "full first-order formulae" (it
does not seem sensible to describe formulae as full; you might want to
say "formulae of full first-order logic", but I do not see much value
in stressing this "fullness").

--- p.12, some typos and inaccuracies in the presentation of
constraints: Full stop after the italicized "sort-generation
constraints" is missing. The assumption that $\Sigma'$ is a
subsignature of $\Sigma$ is inappropriate and should be omitted, the
two signatures are linked by $\sigma$ (not by $sigma$, as at the end
of the paragraph). I would end the last sentence on p.12 as follows:
"...and possibly variables of sorts in $S'$ but not in $S''$."

--- p.15, VAR ::= ID
I guess, VAR ::= SIMPLE-ID here? If ID really is meant for some
reason, then the rules about closure of identifiers should be
changed, to allow parameterization by variables as well...

--- p.16, 2.2.4:
"A term $t$ is said to expand..." rather than "A term is said to expand..."

--- p.16, 2.3:
I do not understand the role of operation profiles in sort generation
constraints in the context of the restriction that "the constraint is
only well-formed if each function symbol has a unique declared type".
I would allow overloaded function symbols here provided that the
optional otherwise profiles are used to disambiguate this.

Also, a comment at p. 21, in 4.4 seems to contradict the requirement
of uniqueness as stated here.

--- p.17: definition rather than definition.

--- p.19, 1st paragraph: s and s' should be s_2 and s_1, respectively.

--- p.19: "Self-inclusions and..." rather than "Note that
self-inclusions and..." :-)

--- p.20, at the bottom: "...up to this equivalence." rather than "up
to equivalence.".

--- p.23, "It is also useful to name parts of specifications.": this
seems to suggest that "incomplete parts of specifications" may be
names, which is not the case, is it?

--- p.24, 6.1: in the grammar rules, LINEAR-LIBRARY and
CYCLIC-LIBRARY should be called LINEAR-SECTION and CYCLIC-SECTION,
respectively.

--- p.24, 6.1: SPEC-NAMEs and PAR-SPEC-NAMEs should be SIMPLE-IDs,
not arbitrary (possibly compound) identifiers, right?

--- p.24, 6.1: "whereas in a cyclic sections, the names of the
specifications defined later in that section" should be reformulated
to allow for direct recursion as well (so not only "defined later" but
also "defined now").

--- p.25, about renamings: it seems worthwhile to state explicitly
that ID-MAPs must be "injective" (an identifier may occur on
the left side of a pair in an ID-MAP at most once plus some extra
consistency conditions related to the use of compound identifiers here).

--- p.25, "identifier" should be "identifier"

--- p.30, Is the category SYMB ever used?

--- p.30. The way of defining the syntax for terms seems strange, at
least to a typical SML person... I would define it as follows:

TERM ::= VAR | APPLICATION | SORTED-TERM
SORTED-TERM ::= sorted-term TERM SORT
APPLICATION ::= application FUN-SYMB TERM*

I can see no need for a special category of unsorted-terms, and no
harm in allowing multiple sort assertions following each other. But
maybe this interacts in some subtle way with the constraints imposed
by the subsorting mechanisms?

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

This seems to be all...

Looking forward to see you in Edinburgh!

[Likewise, and many many thanks for providing such perceptive and
useful comments under difficult circumstances!  They will be extremely
helpful to me when producing the next, and hopefully final draft,
version of the language summary.  --PDM]

Best regards,

Andrzej