Instantiations with partial and total functions

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

Dear friends,

Bartek Klin and Lutz Schroeder have encountered the following
problem (Bartek during the development of CATS, Lutz during
the checking of the basic datatypes):

With the current semantics, it is not allowed to map a
partial function symbol in the formal parameter 
to a total function symbol in the actual parameter within
an instantiation of a parameterized specification.
We feel that this is bad, since CASL treats total functions
as special partial functions in general (signature morphisms
may map partial function symbols to total function symbols).
A 'real life' example from the basic datatypes is
the degree function in euclidian rings: This function is partial
in the general case, i.e. undefined on 0, but is often 
instantiated with total functions, e.g. the absolute value
function on integers.)

Let me explain why the current semantics has such a behaviour.
First, let me note that a renaming may not map a partial
function symbol to a total one. This is because the 
semantics of translations is defined using so-called final 
lifts, see S-10.
Now a signature morphism mapping a partial to a total function
symbol is not final with the current symbol functor.

Now the behaviour of an instantiation is defined in terms
of translation and union in the summary. The semantics just
mimicks this. However, since the translation of a partial
function symbol to a total one leads to an ill-formed
translation (see above), also the instantiation is undefined
(although the fitting morphism can be constructed without 
problems).

There is the following suggestion to solve the problem:

Define the semantics of instantiations by using a set-theoretic
renaming and union, and then use a final lift of the two
resulting morphisms. This solves the problem.
A slight drawback is that the semantics of instantiations no 
longer  is definable in terms of union and translation as in 
the summary.
However, only when a partial function symbol is mapped to a 
total one, the instantiation is defined, while the circumscription
with union and translation is not defined. In all other cases,
the circumpscription in the summary works. Anyway, the difference
only concerns definedness, if the semantics of the circumscription
is defined, it is always the same as the semantics of the 
instantiation.
   
There is another problem with the failure of the translation
of a partial to a total function to be defined:
In Berlin (see the Minutes of Berlin meeting, 13.04.2000 on
cofi-langaue) it has been discussed wether it should be allowed 
to unite signatures containing both the same function symbol, 
but one as a partial and one as a total symbol.
This was rejected there:

     Bernd Krieg-Brueckner raised objections on methodological
     grounds. Moreover, as he pointed out later, it is relatively
     easy to achieve a similar effect by simply translating the
     specification with the partial function declaration by the
     symbol map {f:s->?s |-> f:s->s}. This indeed seems easy
     enough to make the benefits of the change less crucial.

In the light of the above, this does not work.

One possible solution would be to allow (non-final) translations 
of partial into total function symbols. However, this would have 
an important drawback: in the semantics of architectural 
specifications, translations would no longer be extremal epimorphic 
signature morphisms. However, this property is required by the 
new semantics of architectural semantics (see the forthcoming 
study note S-11).

Indeed, the only ways to change a partial function symbol into
a total one seem to be to use union or extension. One can change 
a partial into a total function symbol by uniting or extending 
the specification with a specification containing just the total 
function symbol (and its argument and result sorts).
Methodologically, it is cleaner to use an extension for imposing
additional properties (here: totality) on a specification
than to use a translation.
However, this would need to allow extensions and unions
of partial function symbols with total same-profiled function
symbols. This can be achieved by changing the symbol functor of 
the CASL institution in the following way:
   A partial function symbol f:s->?t in \Sigma leads to a
   symbol f:s->?t in |\Sigma|, while a total function symbol
   f:s->?t in \Sigma leads to both f:s->t and f:s->?t
   in |\Sigma|. |\sigma| always maps partial to partial
   and total to total symbols.
and by allowing extensions of partial function symbols by 
total ones with the same profile in the semantics of basic specs.

The rest of the semantics remains the same.
Anyway, this change of the semantics is very small
and would affect neither the summary nor the CASL institution.
Still, it would make much sense to add a clarification
to the summary.

Greetings,
Till (after discussion with Bartek, Lutz, and Andrzej)