Re: v0.97 lcoal specicications

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

[Follow-ups from Don Sannella, Maura Cerioli, and PDM appended.  --PDM]

Dear all,

Bernd Krieg-Brueckner wrote:
[..]
> >
> >* LOCAL-BASIC-SPEC is analogous to LOCAL-BASIC-ITEMS (App C v0.95)
> 
> so why have two ways to do it?

I am also surprised to see that we now have two local constructs,
where one is almost an instantiation of the other:

LOCAL-BASIC-SPEC ::=  local-basic-spec BASIC-SPEC BASIC-SPEC
BASIC-ITEM ::= ... | LOCAL-BASIC-SPEC

and

LOCAL-SPEC       ::=  local-spec SPEC SPEC
SPEC ::= ... | LOCAL-SPEC

I don't understand the necessity of having both constructs? It seems
to me that either LOCAL-BASIC-SPEC or LOCAL-SPEC would be sufficient
to express what we want. For example:

BI* (local-basic-spec (basic-spec BI1*) (basic-spec BI2I*)) BI3*

can be expressed as

extend (basic-spec BI*) 
by (local-spec (basic-spec BI1*) (basic-spec BI2*))
   (basic-spec BI3*)

(modulo non-linear visibility!!)

However, I seem to recall that in Lille we (the semantics group) saw
difficulties in giving semantics to LOCAL-BASIC-SPECs in case of
_non-linear visibility_ (no problems in case of linear visibility,
though).

As a consequence it was agreed to have LOCAL-SPECs, as they have similar
expressiveness as LOCAL-BASIC-SPECs, but due to the linearization of
structured specs they don't have the problems associated with non-linear
visibility.

Since we don't have linear visibility of lists of basic items, I would
suggest to remove LOCAL-BASIC-SPECs and keep LOCAL-SPECs.

Greetings,
	Hubert

-- 

  To: cofi-language@brics.dk
  Subject: CASL v0.97: local specifications
  From: Don Sannella <dts@dcs.ed.ac.uk>

Dear friends,

On Mon, 19 May 1997 23:11:55 +0200, Hubert Baumeister questioned the
decision to include both LOCAL-BASIC-SPEC and LOCAL-SPEC.  I agree
with what he says: the former seems to be superfluous if we have the
latter, and there are difficulties with giving semantics to
LOCAL-BASIC-SPEC in the presence of non-linear visibility.  Let me be
a little more precise about this last point.

I'm writing the semantics of basic specifications right now.  The way
that I would like to handle them in the presence of non-linear
visibility is to have a spec denote a triple (Sigma,Phi,Sigma') where
(Sigma,Phi) is a basic spec in the underlying institution and Sigma'
is the visible subsignature of Sigma.  But then I would need to
generate implicit renamings to avoid name clashes, as in:

  local c:int ... in ... end; ...; local c:int ... in ... end

where the two occurrences of c:int must not be confused.

This is possible and indeed the details are spelled out in a paper by
Hennicker, Wirsing and Bidoit in a recent issue of TCS.  But it's
messy and I would much rather avoid it since the same thing is
expressible using LOCAL-SPEC.  Maybe there's another way of
interpreting basic specs which avoids this problem, but I don't know
how.  The problem doesn't arise at all with linear visibility, by the
way.  And if LOCAL-BASIC-SPEC is removed, a spec can denote just a
pair (Sigma,Phi), exactly as the introduction to section 2 suggests.

Best regards, Don

--

[Let me recall my response to Maura's comments on v0.96:  --PDM]

  Date: Sat, 10 May 1997 11:56:38 +0200 (MET DST)
  To: cofi-language@brics.dk
  Subject: Let-In; Overloading of functions
  From: cerioli@disi.unige.it (Maura Cerioli)

>[My notes from the Paris meeting tell me that we concluded (on Sunday
>morning) by agreeing that it was more in line with algebraic
>specifications to introduce a (local) constant and and define it by an
>axiom, cf. the treatment of if-then-else or cases by conditional
>axioms.  If my notes are inaccurate on this point, kindly let me know.
>--PDM]
It's correct, but I understood that
"to introduce a (local) constant and define it by an axiom"
was how we were going to define its semantics not that the construct was
discharged.

We don't have any means to define constants (or functions, as Michel points
out) *local* to a (group of) axiom(s), have we? Thus we cannot introduce
the "let-in" in the concrete syntax for a shortcut of a term on the
abstract syntax.

[In v0.96 - all the changes from v0.95 are highlighted, PLEASE take a
look at them! - we have LOCAL-SPEC ::= local-spec SPEC1 SPEC2, which
can be used to make the (e.g.) definitions of SPEC1 local to SPEC2,
and the latter may be (e.g.) just some axioms extending a spec.  Thus:
  extension 
    ... 
    local-spec (...) (...)
    ...
Andrzej has now proposed to allow also LOCAL-BASIC-ITEMS (App C of v0.95)
to permit the same sort of thing purely within a BASIC-SPEC, but I've
questioned the need for this in my response to his "more serious
comments".  In either case, it seems that one can already express the
locality of some basic items in some axioms, in CASL v0.96.  --PDM]
...

Maura

--

[Personally, I'm in favour of removing LOCAL-BASIC-ITEMS, as I'd like
to keep basic specifications free of (especially nested) scopes
altogether - which, BTW, seems to me an argument in favour of
non-linear visibility, in that one then doesn't have to keep track of
a changing local environment in a basic spec at all!  ANDRZEJ, MAURA:
if you still support the inclusion of LOCAL-BASIC-ITEMS, please say why
- otherwise I'll prepare a minimal Note of Dissent proposing their
removal. --PDM]