Overloading of functions [clarification needed]

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

Just another brief comment on V 0.96:

Section 3.1, p. 11 introduces the overloading relation for functions and
predicate symbols; it does not make clear whether overloading between
partial and total functions from the signature is allowed. We think it
should be, so perhaps this should be indicated explicitly.

Example:

sort s s'
s < s'
f: s  -> s      (partial or total)
f: s' -> s'     (partial or total)
a: s

In this signature, one would like, we think, the term f(a) to be
well-formed independently from partiality or totality of the two
declarations of f (and this requires that the two declarations of f are
compatible).

BTW, as far as we understand the semantics conditions, if f: s' -> s' is
total, then f: s -> s HAS TO BE TOTAL as well (semantically of course, it
doesn't have to be declared as such). Maybe this should be indicated in the
summary as well (in the last item in sect. 3.2)...

BTW' (from Andrzej), I don't really like the name "overloading relation"
here: to me overloading is something when two different functions are named
by the same identifier. Here we talk about something opposite in a sense:
when two functions with the same identifier but different profiles are to
be in fact the same. So, something like "compatibility relation" would be
perhaps more adequate in my view.

Best regards,

Andrzej and Michel