Comments on v0.96 Section 1-4.2

[cerioli@disi.unige.it (Maura Cerioli)]

This message comments on Basic Specs BUT Datatypes.

I basically agree with Andrzej's (and Michel's) "comments on v.0.96",
points 1-7. I would like to remark some more about points 2 and 5 of that
message and add two more proposals for changes.

[I'll be commenting myself on Andrzej's message later this afternoon.
To save time/messages, I've taken the liberty of adding my reactions
- qua editor of the Summary - directly to Maura's message.  --PDM]

=================
Distinction between constant/non-zeroary-functions (point 2).
First of all, if the distinction is made, then I strongly second Andrzej that
- there must be a uniformity between partial and total constants
- the treatment must uniformly spread at each level from the institution
  up (with CONST-NAME...)
In order to fix my mind if I *want* to have the distinction in the abstract
syntax, I first need to know if having one category in the AS entails that
we have one notation for declaration and application in the concrete syntax
as well.
Indeed, I'm definitely sure that I want to be able to write terms like "c"
if c is declared as a constant, and I refuse to be forced to write "c()" at
the concrete level.
Therefore, if the abstract and  concrete syntaxes are going to be
isomorphic, then I want to have the distinction, if we simply require (as I
think it's standard) that each term on the concrete syntax can be
uniquely mapped to a term on the abstract syntax (allowing, in
particular, several concrete constructs to be translated into the same
abstract one), possibly using the context to disambiguate the mapping, then
I prefer to have no distinction between constants and functions at the
abstract level.

[My only motivation for making the change in v0.96 was to facilitate
the extension to Higher-Order CASL.  I agree with you and Andrzej in
all other respects (on this issue, anyway :-). --PDM]

Actually, the point if we are/aren't going to have a 1-1 correspondence
between AS, concrete syntax and/or internal representation of Casl
expressions has been rised before, in the discussion (never solved) between
Bernd and me, and is relevant for other points as well, like the
definition of SYMB-MAP (point 7 in Andrzej's message) that has been (imho)
worsened, wrt the previous version, dropping the different categories
SORT-MAP... with the unique (if I correctly understood) motivation that it
simplifies the parsed terms (IF AS is used as syntax for the internal
representation, that is).

[Actually, I found spelling out these context-free differences quite
boring, so I was happy to follow Bernd's proposal there.  Moreover,
there should be some uniformity between SYMB-MAP and NAME-MAP in the
AS, right? - but with so many different categories of -NAME now, the
AS grammar for NAME-MAP in the style you propose would really be quite
tedious, IMHO.  --PDM] 

=================
ISO-DECLs
I share with Andrzej both the memory that in Paris we chose to have that
the unique way to introduce a cycle was using an ISO-DECL construct (I
don't know if in Lille the decision was unmade, but it is reflected also in
the annotated version for the semantics group at page 18, sec 4.1) and the
proposal of changing the decision now to have an error if a cycle is
introduced by a subsort-decl, but simply a warning if this happens by
making unions and the like.

=================
Term construction
Since name, argument sorts and result sort determines if a function
(constant) is declared as partial or total, I prefer not to have this
information in the qualified application construct.
Thus I propose to change
FUN-DECL ::= fun-decl FUN-NAME+ TOTALITY FUN-TYPE
(CONST-DECL ::= const-decl CONST-NAME+ TOTALITY CONST-TYPE)
TOTALITY::= total | partial
FUN-TYPE::= SORT* SORT
(FUN-TYPE::= SORT+ SORT)
(CONST-TYPE::= SORT)

(In brackets the version if we have a distinction between functions and
constants)
In this way the "totality" attribute disappears from the application.

[Sounds fine.  One should note that this does *not* prevent the use of
various styles of arrows when indicating the FUN-TYPE of an
APPLICATION in *concrete* syntax.  --PDM]

=================
Let-in ???
I think that in Paris we decided to have in (that is: to propositively add
it to) the new summary a construct to have shortcuts for long terms to be
used in axioms, something like
  let t=f(hgfhf(jjj,yuyt,sdfdsf,........) in
  t=g(t,t)=>p(t,f(t))
whose semantics is expected to be "to add to the local environment a
partial constant t of the expected sort and the axiom t=.... and use it to
evaluate the axiom, discharging then the constant".

I didn't find any trace of this in the summary.
Is this because
a) my memory is not anymore as it used to be ;-)
b) some different decision was made afterward,
c) we leave it to the concrete syntax (...?...I dislike to have a concrete
construct that cannot be mapped into any abstract one, as we don't have
local declarations in basic items)
d) I simply missed it?

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

Best Regards
Maura