Comments on V0.93

[Michel.Bidoit@ens.fr (Michel Bidoit)]

[Michel sent this to me last week, but I delayed forwarding it because
it referred to his new note on Parametrization, which wasn't ready at
the time. --PDM]

Main issues for the discussion:

Name: I am in favour of FOCAL (First-Order Common Algebraic specification
Language ?)

Subsorts: The last two study notes sound convincing. I must confess I will
leave this issue to the specialists and rely on them :-)

[Subsorting was still a topic of intense discussion between "the
specialists" all last week.  A definitive note, reporting the
conclusions, is currently being prepared.  The main change from the
proposal in v0.93 is that partial restriction is to be deferred to
extension languages.  It is to be replaced by ordinary restriction,
making it unnecessary to consider a definedness ordering on expansions.
--PDM]

Compound identifiers: See my proposal in the note on parametrized
specifications. 

Cyclic sections of libraries: I understand the need for this, although I
have never encountered this situation in all (huge) examples I have been
involved with. This point is not so easy to grasp. I would suggest to defer
it in a small section at the end, once all the main stuff have been
explained (sometimes it is better not to explain everything at once,
cf. subsorts).

Parametrization: Let me hope that my note answers most questions and solves
most doubts...

Architectural specifications: I am strongly in favour of architectural
terminology. As soon as I will have time I will quote in an e-mail some
sentences by Garland (one of the popes on this issue) pointing out that
architectural is right in our context (even if other concepts, not taken
into account by our architectural specs, are also in the architectural
business).

local/let: I believe a construct of the form:
   let t = "complex term" in sentence
is necessary to allow the user to write more concise axioms (in the case
the same complex, huge subterm occurs more than once in the formula).
Easy to add ?

PART I

1.3 Sentences: I like very much the idea of having sort-generation
constraints as sentences. However, the current explanation is a bit obscure
or at least not so intuitive. I would suggest to explain first what is a
sort-generation constraint at the naive level (just (S, TF, PF) and what
does it mean for a Sigma-algebra to be finitely generated w.r.t. this
constraint, assuming (S, TF, PF) included in Sigma), and only then to
explain how to reflect this in an institution way... At first reading I was
not able to understand the last paragraph of Section 1.3...

2.1 Declaration of Symbols: The explanations on "redeclares" are unclear for
me. Should be deferred to Section 5 once environments are introduced ?

2.1.3. Predicates: What are predicates with no arguments good for ???

2.2.2. Logical connectives: What is the role of TRUTH ::= true | false ???

2.2.4. Terms: I am a bit worried by the explanations provided. Here is my
view on this (disregarding subsorting).

I believe that at the semantic level, we always consider a function symbol
together with its profile; in other words, any function symbol is
qualified by the corresponding profile and therefore made unique in the
signature (no overloading anymore). At the semantic level a (well-formed)
term is obtained by composition of the qualified function symbols. Hence
the sort of any well-formed term is clear, and I do not see the distinction
between a well-formed term and a well-sorted term ?

When parsing expressions intended to denote terms, the problem is to
recognize the function symbols involved together with their profile. In
case of overloading (several identical function symbols with distinct
profiles), parsing may be ambiguous. Ambiguity can also have other causes,
e.g. due to mixfix syntax etc. Hence usually (at least with mixfix syntax),
it is not possible to go from an expression to a "potential term", by this
I mean a composition of function symbols disregarding the profiles, perhaps
this is what is called an unsorted term (?), and then from this
potential term to a well-formed term. Both tasks must be done
simultaneously, checking of course that at the end there is only one
correct parsing of the expression into a well-formed term.

I understand that the explanations given are a preliminary for
subsorting... Perhaps more explanations even in the absence of subsorting
are necessary. 

2.3 Sort Generation:

The possibility to disambiguate function symbols by their profile is
necessary not only here, but in any case the user has to refer to symbols
(cf. RENAMING, DERIVATION, RESTRICTION, FITTING-MORPHISM). See a previous
remark by AH on this issue. This exists in LSL and PLUSS, at least.

2.4. Type Definition Group:

So far I was convinced that a TYPE-DEFN-GROUP was an abbreviation for a
specification. It was unclear for me how to ensure otherwise the intended
semantics of a TYPE-DEFN-GROUP. However, now sort-generation constraints are
sentences, hence it may well be the case that considering a TYPE-DEFN-GROUP
as an abbreviation for some BASIC-ITEM+ is enough. Is my interpretation
correct ?

[My understanding is that this would not capture the "no confusion"
part, where constructs are to be distinct unless there identity
follows from the axioms. --PDM]

PART II

6.2 Specification Expressions:

For RENAMING, HIDING, REVEALING, (and now FITTING-MORPHISM), referring to a
function symbol by its ID may be ambiguous. Hence in some case
qualification by the profile is necessary (see remark above in 2.3).

Moreover, as soon as one consider that function symbols are qualified by
their profile, then a renaming of a sort entails a renaming of all function
symbols having this sort in their profile (the same for predicates of
course). W.r.t. DERIVATION, if one hides a sort, then all function symbols
having this sort in their profile are hidden as well, since the global
final result must be a signature. The user merely describes the useful part
of the signature morphisms involved, which must then be "completed" into
true signature morphisms. More explanations are required here, I am afraid.

Michel