Re: Total and partial functions

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

Dear Maura,

> If we are going to allow a non-empty intersection between the sets of
> total
> and partial function with the same index (at the institution level),
> then we
> should find another reference (in the chapter by Horst, Till and me in
> the
> Ifip book the theory is developed under that assumption) or re-develop
> the
> theory in this more liberal setting. The latter could be done easily (by
> somebody else, I definitely wont do it), but it would be boring
> (annoying,
> too, from my point of view) and sincerely at that point I don't see a
> reason
> to distinguish between partial and total symbols at the signature level
> at
> all. Thus *if* we (that is, you or they) are going to modify the
> institution,
> it would probably better to have just one (indexed) set of function
> symbols
> and interpret a total declaration as a partial one plus the appropriate
> assertion of definedness (that, being atomic should be available in all
> possible restrictions).
> I'm against changing the institution at this late phase, unless it
> proves
> strictly necessary.

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

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

One reason for the change is the greater uniformity with the
higher-order
case, where we have to index the symbols with their higher-order
type anyway (i.e. we write f_{w->s} or f_{w->?s}), and where it
would be difficult to motivate the restriction that we have currently
for the first-order case. Moreover, indexing function symbols with
their full type (w->s or w->?s) is also more uniform with the abstract
syntax (which indeed was also chosen this way in order to be
compatible woth HO extensions):

  OP-ITEM         ::= OP-NAME ,..., OP-NAME : OP-TYPE

  OP-TYPE         ::= SOME-SORTS  -> SORT  |  SORT                      
                    | SOME-SORTS  ->? SORT  |  ? SORT              
                    
The other reason is union, see below.

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

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

 
> A different issue is what happens at the level of structured
> specifications.
> Indeed, my methodological objections do not apply to the case of
> (possibly
> independently developed) subspecifications of a specification term.
> For instance, the case of union sounds quite reasonable to me (though
> not
> exactly a "must" imho).
> 
> Thus I suggest that *if* there is a consensus about allowing the
> "overloading"
> of total and partial functions with the same profile, then we limit it
> to the
> case of structured specs. 

Indeed, the case of unions is the most convincing argument for
the change: if we unite a signature containing a total
profile and a signature containing the same profile as partial,
it is a bit strange that the union is undefined (and, btw, this
is the only case where unions can be undefined).

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.

Greetings,
Till