Re: Parametrization (The end ?)

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

Dear Colleagues,

First, let me use this opportunity to bring a very sad news:
==============================================================================
Prof. ANTONI KRECZMAR, whom some of you might know as an excellent
scientist and a wonderful person, died on 23 October, aged only 51.
To us here in Warsaw, he was our teacher from the university days, and
then a colleague and a very good friend.  We will miss him a lot!
==============================================================================


CoFI:

My apology for the rather late response, way beyond the deadline for
reactions to Michel's note.  Therefore I will try to make this as
brief as possible [In fact Andrzej sent me a draft of this message
last Monday, (almost) meeting the deadline. He then spent extra time
to take account of my comments on it and to condense it.  --PDM]
skipping my sincere appreciation for the work Michel done in
presenting and justifying parameterised specifications, and going
directly to the main point at which my views differ from what is in
his note.  [Recall that Andrzej expressed his views on compound
identifiers and some other details in a message on 15 October. --PDM]

In a word: I do not see the need to introduce formal parameter
specifications as a separate kind of specifications, and I do not see
the need to introduce some special formal rules into the language we
design to separate fixed and non-fixed parts of a parameter
specification. What may (and perhaps should) happen is that the
valuable analysis of possible intentions of the user and consequent
conditions on expected instantiations Michel presents in his note can
be viewed as methodological desiderata for the way parameterised
specifications are to be used, and/or perhaps should find their way
into the syntax of the formalism as some annotations --- which then
would be disregarded by its formal, semantic description.

This would mean that as far as the formal design of the language is
concerned, in the part dealing with parameterised specifications, we
could stay basically with what v0.93 described --- and try to
formulate some extra methodological guidelines along the lines Michel
suggested (but without changing the design of the formalism as such).
For instance we could say that if a parameter specification
(NAMED-ELEM of Michel's note) is built as a persistent enrichment of a
named specification (NAME) then it is expected that no instantiation
of a parameterised specification with this parameter specification
(STACK2[Named-ELEM]) should change the named part (NAME) of the
parameter.

However, this would only be viewed as a methodological indication, not
as a formal requirement. After all, even in the example Michel used,
why should we (or the user) really insist that NAME is fixed?  For
instance, COMPOUND-NAMES-ARE-NICE, and we may want to instantiate NAME
to some specification of compound names...

The above indicates that I am not really convinced by Michel that such
an explicit insistence on the NAME being fixed is necessary at the
level of requirements specifications. (In my view the only situation
when something like this might be needed would be when we want to
specify a construct which works for an arbitrary but fixed realization
of NAME. But this brings us into the realm of architectural specs, and
this is a separate matter --- there will be a message from me
responding to Peter's note, b.t.w...)

My (I guess I should stress *MY* very strongly, as in *my fault* :-)
specific technical problem with this part of Michel's proposal is that
I felt completely lost in the technical details of the final proposal,
in particular I was not able to understand and follow "the intended
restrictions on well-formedness" which I think contain the technical
essence of the proposal. I could not quite follow the formulations, I
could not see all their consequences, and it seemed to me that some
further, perhaps even more fundamental, conditions were missing to
make the meaning of instantiations completely consistent with what a
naive user might expect.  

[Sorry, but that was entirely *MY* fault: Michel sent me a draft of
his proposal, with an attribute grammar defining the intended
restrictions much more accurately --- but I found it quite hard to
follow, and proposed the less formal presentation that appears in his
note.  We were, however, quite careful in pointing out that this was
only a rough indication of the intended restrictions... --PDM]

I do know though that the simple intuition and the semantics of
parameterised specifications and their instantiations can be well
described without this conditions (in fact, exactly as Michel does in
the beginning: the intuition and semantics for instantiations he
suggests there works without any extra conditions being imposed on the
fitting morphism).

There is also a meta-methodological disadvantage of the proposal which
I felt was important: a deliberate loss of referential transparency
(the semantics of a specification depends on whether some of its parts
got named in the process of building the specification or not). For me,
this kind of intuition attached to whether something got named or not
belongs only to the methodological, not to the formal definition
level.

[Michel proposed using names for simplicity.  An alternative would be
to provide a structuring construct (frozen SPEC, say) whose only
impact on semantics would be to make ill-formed those instantiations
involving translation of the frozen parts of parameters.  This hasn't
been worked out, but it would at least provide referential
transparency.  As such freezing would have no effect on the algebraic
semantics at all, the only difference between this construct and a
corresponding annotation is the effect on well-formedness.  --PDM]

With best regards,

Andrzej

[One further issue on this topic, before we close it: one of
pedantics!  My dictionary (Concise Oxford, 1976) is quite definite
that the *only* correct spelling of the verb formed from `parameter'
is `parametrize' - which corresponds closely to how I would pronounce
it.  However, many of you seem to prefer `parameterize', or even
`parameterise'.  Is there a justification for such spellings?  If not,
I would like us to stick to `parametrize' in approved CoFI documents.
--PDM]