Re: Total and partial functions

[Maura Cerioli <cerioli@disi.unige.it>]

[Dear Till et al.,]

[note: semantic considerations first, language considerations later
(BKB)]

If we are going to allow a non-empty intersection between the sets of
total
and partial function with the same index (at the institution level),
then we
should find another reference (in the chapter by Horst, Till and me in
the
Ifip book the theory is developed under that assumption) or re-develop
the
theory in this more liberal setting. The latter could be done easily (by
somebody else, I definitely wont do it), but it would be boring
(annoying,
too, from my point of view) and sincerely at that point I don't see a
reason
to distinguish between partial and total symbols at the signature level
at
all. Thus *if* we (that is, you or they) are going to modify the
institution,
it would probably better to have just one (indexed) set of function
symbols
and interpret a total declaration as a partial one plus the appropriate
assertion of definedness (that, being atomic should be available in all
possible restrictions).
I'm against changing the institution at this late phase, unless it
proves
strictly necessary.

Otherwise, the change is only at the language level, that is if a symbol
is
declared with the same profile as both total and partial, then only its
total
version appears in the signature, so that, btw, there is no problem with
ambiguity in term formation.
[there is no ambiguity with the present overloading relation either;
both must "overlap with the same semantics", i.e. be the same, i.e. be
total (BKB)]
However, let me remind that when we discussed the possibility of having
the
same function symbol with the same profile both total and partial in the
context of function declaration in basic specs we thought most likely
that
such a double declaration was an error of the user and decided to forbid
it.
[this is a methodological concern, as many others (BKB)]

Now, I think that methodologically is still true that is not probable
that you
want to add a declaration where the only change is from total to partial
within the (hopefully small) basic spec defining the function the first
time. 
Indeed, if you have just given the partial declaration, then the effect
of the
total declaration is equivalent to the axiom Def(f(x1..xn)).
(BTW, it seems much more reasonable to edit the previous declaration if
you
notice that the function should be total, than to let the "wrong"
declaration
stands and then modify it by adding a new declaration, or an axiom).
Vice versa, if you have the total declaration, then the partial
declaration
has no effect at all.

A different issue is what happens at the level of structured
specifications.
Indeed, my methodological objections do not apply to the case of
(possibly
independently developed) subspecifications of a specification term.
For instance, the case of union sounds quite reasonable to me (though
not
exactly a "must" imho).

Thus I suggest that *if* there is a consensus about allowing the
"overloading"
of total and partial functions with the same profile, then we limit it
to the
case of structured specs. 

[Clearly, the case of union or extension by the total declaration are
the
important ones, but do not forget signature morphisms and parametrized
specs.
Anyway, this is a feedback from Higher-Order extension considerations
(which
should be taken seriously), where the exclusion of overloading the same
profile (partial and total) in the FO case would be a nasty anomaly.
Also:
remember the possibility to redeclare the same profile again, which you
may
also consider silly from a methodological point of view. Within the same
spec,
a warning by tools would be OK with me.
So: I am for Tills proposal (BKB)]

Best regards
Maura