Re: Instantiations with partial and total functions

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear Peter,

on 27 Nov 2000, you wrote to this list:

> > 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.
>
> That sounds reasonable - although I guess that translations which
> introduce new subsort relations are still allowed, and may also lead
> to imposing additional properties?

The only way to introduce new subsort relations via a translation
is to identify sorts, as e.g. in

  sorts s<t; u<v with t |-> u
  
Here, we get s<v by transitivity, since t is identified with u.
This is allowed and will be allowed by our recent proposal.

Greetings,
Till
-----------------------------------------------------------------------------
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
-----------------------------------------------------------------------------