Let-In; Overloading of functions

[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]

That's not the same as if-then-else or cases, because
        if b then a1 else a2
may be translated into
        (b => a1)/\(not b => a2)
and hence it is the "concrete" representation of a term that already exists
in the language.
(BTW I hope for an if-then-else in the concrete syntax)

[Please send your list of hopes concerning concrete syntax directly to
Bremen and Paris, where final proposals are in preparation!  --PDM]

Thus I look at the two things as different. But maybe it is once again my
personal feelings on the relationship between abstract and concrete syntax
that get in the way.

Maura
________________________________________

Subject: Overloading of functions: Sorry!

Andrzej is (as always) right!
Sorry.
This proves once more that I'm NOT one of the "subsorting people".
Sorry also for the delay, but I was at a meeting....
Maura