Re: Total and partial functions

[Peter Mosses <mosses@csl.sri.com>]

[answer by Peter, but also by Andrzej at the end]

Dear Till and Maura,

Maura> If we are going to allow a non-empty intersection between the sets
Maura> of total and partial function with the same index (at the
Maura> institution level) [...] it would probably better to have
Maura> just one (indexed) set of function symbols and interpret a total
Maura> declaration as a partial one plus the appropriate assertion of
Maura> definedness (that, being atomic should be available in all possible
Maura> restrictions). 

So long as the language still allows operations to be declared as
total or partial, the user perhaps need not worry too much about just
*how* the semantics ensures that models provide the expected
interpretations.

Maura> I'm against changing the institution at this late
Maura> phase, unless it proves strictly necessary.

I intend to install the draft of the CASL Summary v1.0 on 1 October,
in accordance with the revised schedule.  So I'm a priori inclined to
share Maura's sentiments...

Till> The changes to the institution would be
Till> 1. allow the sets TF_{w,s} and PF_{w,s} to have non-empty intersection
Till>    (i.e. a function can be both total and partial for the same
Till>      profile)
Till> 2. Replace the indexing of function symbols in fully-qualified terms:
Till>    Instead of f_{w,s}, write f_{w->s} or f_{w->?s}

...with f_{w->s} or f_{w->?s} always being in the overloading
relation, presumably.

Till> These changes are a bit tedious but easy (I volunteer for doing them,
Till> both in the semantics and in our book chapter).

...and in the Summary as well, perhaps?  :-)

Till> One reason for the change is the greater uniformity with the
Till> higher-order
Till> case, where we have to index the symbols with their higher-order
Till> type anyway (i.e. we write f_{w->s} or f_{w->?s}), and where it
Till> would be difficult to motivate the restriction that we have currently
Till> for the first-order case. [...]

Correct me if I'm wrong, but I'd expect that w->s would be a SUBTYPE
of w->?s in a proper HO extension of CASL.  If so, this seems to
support the argument for allowing a function constant to be overloaded
by declaration both as total and partial in the same basic spec.
[yes (BKB)]

CASL allows e.g. the declaration of 0:Nat and 0:Int (and the
unqualified use of 0, provided Nat<Int).  The usefulness of 0:Int
shows up (only?) when one wants to hide Nat but reveal 0.  Perhaps in
a HO extension of CASL, one might hide the total function types; then
one may indeed find it useful that the same functions can have partial
types with the same profiles.

Maura> Otherwise, the change is only at the language level, that is if a
Maura> symbol is declared with the same profile as both total and partial,
Maura> then only its total version appears in the signature, so that, btw,
Maura> there is no problem with ambiguity in term formation.

Till> I do not like this possibility, because it would complicate the
Till> semantics of unions (a union of a signature containing a total
Till> profile and a signature containing the same profile as partial
Till> would contain just the total profile. So we do not have a set-theoretic
Till> union of the underlying symbols. 

It seems that there are 3 candidates for an institution catering for
total and partial declarations ops f:w->s; f:w->?s :

1. allow the sets TF_{w,s} and PF_{w,s} to have non-empty intersection
2. always remove elements of TF_{w,s} from PF_{w,s}
3. use only PF_{w,s} plus definedness assertions

Presumably 1-3 are equivalent institutions, and therefore the CASL
users need not worry about the choice, which might be left to those
writing the CASL semantics.

However, in the CASL Summary we do try to *explain* CASL by saying how
CASL declarations expand to signatures, etc.  So (unfortunately) the
choice is still pertinent to the Summary of the language design...

I now plan to follow 1. above in the DRAFT of the CASL Summary v1.0.
Perhaps further discussion of the issues here is best left until
the 14 days after that DRAFT appears.

Thanks for the input, even though it was almost too late...

Best regards,

-- Peter
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-5067
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/

(*) on leave from DAIMI & BRICS, University of Aarhus, DK
    also affiliated to CS Department, Stanford University
_________________________________________________________

From: Andrzej Tarlecki <tarlecki@mimuw.edu.pl>
Subject: Re: Total and partial functions


> I would not limit the change to the case of structured specs,
> since this would be too complicated. After all, the change
> I propose does not complicate anything. It is just a bit tedious
> to change the documents.

Wouldn't we also have to start talking about overloading much earlier
now, before subsorted concepts are introduced, to cater for the
overloading between partial and total functions with the same profile?

Best,

Andrzej