Re: Overloading of functions [clarification needed]

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

>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.

I always assumed that it was possible to use the same symbol for a partial
and a total function, provided that their profiles were different, of
course.
This follows from the fact that we are working with "standard" many-sorted
signatures enriched by the \leq_S subsorting relation, doesn't it?

>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).

This should follow from the definition of \leq_F (that disregards the
totality/partiality of the function symbols involved).
Unfortunately [? --PDM :-)] the formal definition has been dropped in the
summary and it is not clear (at least to me) whether f: s -> s' stands
for f\in TF_{(s,s')}, for f\in PF_{(s,s')} or for 
f\in TF_{(s,s')}\cup PF_{(s,s')}.  

[The formal definition would say the last of these, right? --PDM]

Maybe we could add a clarification?

[OK - how about this:  

  For a subsorted signature, we can define \emph{overloading relations}
  for function and predicate symbols. Let 
  $f_i \in {\TF_{w_i,s_i} \cup \PF_{w_i,s_i}}$ for $i=1,2$; then
  $f_1 \leq_F f_2$ holds if $w_1\leq w_2$, $s_1$ and $s_2$ have a common
  supersort, and $f_1=f_2$.  Similarly for predicate symbols, let
  $p_i \in P_{w_i}$ for $i=1,2$; then $p_1 \leq_P p_2$ 
  holds if $w_1\leq w_2$ and $p_1=p_2$.

--PDM]

>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)...
I don't think so.
If f: s' -> s' is total, then on each (embedding of an) element in s it
yields an element in s', that may happen not to be in s. Thus its
"restriction" to s -> s may be partial.

[Presumably an f: s -> s' would have to be total, though.  --PDM]

Best regards,

Maura