Total and partial functions

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear friends,

Anne, Bernd and I are currently rewriting the study note about higher
order CASL, and I found the following detail in the CASL desgin
which looks very special and strange from the HO perspective
(although it could be implemented in the HO extension without
problems):

A function symbol may not be defined as total and partial for
the same profile.

I think the reasoning behind this restriction was the following:
If we declare a function symbol to be both total and partial for
the same profile, then we cannot use the unqualfied symbol in terms.
But this is wrong! Indeeed, the two profiles get into the overloading
relation, making the two interpretations the same (i.e. the partial
function is interpreted in the same way as the total function,
and therefore it is total as well). According to the rules for
equivalent expansions, the function symbol may be used unqualified
in terms.

Moreover, the above restriction is the only reason why a union
in CASL may be undefined. By removing this restriction, unions
would be always defined.

Greetings,
Till

[wholeheartedly supported by BKB]