Re: Instantiations with partial and total functions

["Peter D. Mosses" <pdm@daimi.au.dk>]

Till wrote:

> 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?

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

In the CASL Summary (v1.0.1-DRAFT) Sect. 6.1.3 Unions we have:

  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.

The Summary would surely need changing there...

> Still, it would make much sense to add a clarification
> to the summary.

Further clarifications would presumably be needed in the Summary
concerning the analagous changes for extensions, and perhaps also 
as to whether the same name may be declared both as a total and 
as a partial operation with the same profile in the same basic
specification (the current prohibition of the latter looks in any 
case far too implicit...).

I'd like to include all such changes in the (long-)pending final
release of v1.0.1, since I hope that there won't be a need for any
further new version for at least a year.  However, in my opinion these
are real language design changes, and not merely details of the
semantics.  They should therefore be properly explained and discussed
on cofi-language before their adoption.  As they clearly concern a
practical problem that has been discovered with the present design,
wouldn't affect the syntax of the language, and wouldn't invalidate
existing well-formed specifications, I can't imagine any grounds for
objecting to the changes, but I still think we should follow the
proper discussion procedure for changing CASL.

If Till (and Bernd, as Language Design Task Group coordinator) agree
with the above, I suggest that they send a brief message a.s.a.p. to
cofi-language summarizing the need for the changes, and proposing all
the intended amendments to the wording of the Summary.

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

In any case, thanks indeed to Till and the others for their efforts
with identifying and finding a solution to an awkward problem!

-- Peter

=========   ============================================================
==== ====   Peter D. Mosses                     mailto:pdmosses@brics.dk
=========   BRICS & Dept. of Computer Science   [= pdmosses@daimi.au.dk]
==== ====   University of Aarhus                http://www.brics.dk/~pdm
==== ====   Ny Munkegade, bldg. 540             telephone: +45 8942 3285
==== ====   DK-8000 Aarhus C, DENMARK           telefax:   +45 8942 3255