Partial and total function symbols

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

Dear friends,

during the work on the basic datatypes and the CASL tool set,
the following problem has been discoverd:

Currently, it is not allowed to 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. Consider e.g.

spec ExtEuclidianRing [op delta: Elem ->? Nat] given Nat =
   TheBody
end

Now section 6.2.2 of the summary defines the instantiation

  ExtEuclidianRing[Int fit Elem |-> Int, delta |-> abs]

to be the same as

  { TheBody with Elem |-> Int, delta |-> abs } and Int
  
The problem is now that the left summand of this union
contains abs:Int->?Nat, while the right summand contains
abs:Int->Nat.  

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

As a consequence,

  { TheBody with Elem |-> Int, delta |-> abs } and Int

and with it also

  ExtEuclidianRing[Int fit Elem |-> Int, delta |-> abs]

would be ill-formed. Since this is a bad consequence, we suggest to
replace (v1.0.1-DRAFT) Sect. 6.1.3 Unions:

  The signature of the union is obtained by the ordinary union of the
  Sigma_i.  ...  The union is ill-formed when the same name is
  declared both as a total and as a partial operation with the same
  profile.
  
with:

  The signature of the union is obtained by the ordinary union of the
  Sigma_i.  ...  If the same name is declared both as a total and as a 
  partial operation with the same profile (in different signatures),
  the operation becomes total in the union.

There is a further problem with the outcome of the Berlin discussion.
Namely, it is not possible to use the symbol map {f:s->?s |-> f:s->s} 
to make a partial function symbol total (this has its reason in
the institution-independent semantics, and also is methodologically
justified by the rule that translations should really only rename
things, while making a partial operation symbol total is more than that).

Therefore, we suggest to add a sentence to sect. 6.1.1 Translations:

  If a partial operation symbol is renamed into a total one,
  this is only well-formed in case that the resulting operation
  symbol is already total due to another component of the renaming.
  
Note that with the new behaviour of unions, one can now make
a partial operation symbol total by just taking the union with 
a specification containing the total operation symbol.

Perhaps it would be methodolgically cleaner to allow such things
even within extensions. This would require a clarification 
in section 2.1.2.1, Operation Types:

  If an operation is declared both as total and as partial with
  the same profile, the resulting signature only contains the total 
  operation.

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

-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------