Re: Overloading of functions [clarification needed]

[Tarlecki <tarlecki@lsv.ens-cachan.fr>]

A quick reaction, since my understanding seems to depart considerably
from what one of the authors of the subsorting proposal is saying:

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

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

I thought that the compatibility condition in this case would spell
out the requirement that the following two fully annotated terms are
strongly equal for any valuation of x into the carrier of sort s:

	(f:s'->s')(emb_{s<s'}(x:s)) =s= e_{s<s'}((f:s->s)(x:s))

If f: s' -> s' is total then (the left hand side is always defined, so
the right hand side is always defined, and consequently) (f:s->s)(x:s)
is always defined, i.e., f is a total function (it might be declared
as partial, but in fact it is defined on each value of its indicated
argument sort). This means that the Sigma^\sharp algebras where
f:s'->s' maps some (embedding of an) element in s to an element in s'
that is not an (embedding of an) element in s are not "order-sorted"
models we consider at all!

PLease, correct me if the above is wrong!

An alternative might be to require:

	proj_{s'>s}((f:s'->s')(emb_{s<s'}(x:s))) =s= (f:s->s)(x:s)

which would imply the interpretation suggested by what Maura wrote.

However, then I do not understand the notion of well-formedness of a
term. Namely, in the context of the above signature, I would think
that f(a) is a well-formed term (both, for sort s and for sort s').

But then, with the alternative (latter) interpretation of
"compatibility", the meaning of f(a) (well, definedness of its value)
would depend on the result sort considered, and this seems rather
unexpected...

*** Maura and/or others from the subsorting group:
***	Please, indicate my misunderstanding or confirm my comments,
***	as this seems essential for any understanding of subsorting
***	in CASL at all! 

[Perhaps Maura was thinking of the projection of f(a) onto the 
 subsort s?  I share your understanding here, Andrzej.  --PDM]

Best regards,

Andrzej

PS: as far as "overloading relation" between function names is
concerned, it seems that my understanding was consistent with what
Maura wrote (although I don't think we are working with "standard"
many-sorted signatures wnrich by subsorting, since we are splitting
function names into total and partial function names), so it's just a
matter of rephrasing the description in the summary. I think what
Peter proposed makes this clear enough.