[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Partial vs. total function symbols

[[[ Dear Semanticists,

What follows is an updated and re-thought proposal for a change in the
semantics to resolve the issue of partial vs. total funtions symbols
with the same profile. The solution proposed below seems fine to a few
people (Lutz Schroeder, Till Mossakowski, Bartek Klin, me) who
discussed it recently. It does, however, influence some corners of the
langauge design, so final approval will be needed from the language
design group. I hereby ask for comments on the semantic aspect of this
proposal, and unless some major objections are raised by the end of
this week, I will ask Lutz and Till to forward this to the langauge
design group as a recommendation from the semantics group for changes
in the related aspects of the design.

Best regards,

Andrzej Tarlecki
]]]

Dear friends,

we are still grappling with the implications of `making partial
symbols total'. Bartek Klin has pointed out to us that there are
several snags attached to our recent proposal of changing the symbol
functor to include two copies of all total symbols; it appears
presently that there are the following alternative solutions:

1) Disallow all methods of making partial symbols total,
   including things like "a:?s then a:s", and leave everything else 
   unchanged :-(   

2) Allow extensions like "a:?s then a:s". To accomodate this (under
   the `old' symbol functor), drop the assumption that extensions always 
   produce signature inclusions, requiring instead that they yield 
   injective signature morphisms. 

(In both cases, the semantics of instantiations would have to be changed
as suggested in the previous proposal; i.e. one would use final lifts
of set-theoretic unions, so that instantiations may be defined even
when the circumscription "<body> with <fitting> and <argument>" used
in the summary is undefined due to non-finality of the translation.)

3) Modify the symbol functor by removing all ?'s from the
   qualifications.  Consequently, the syntax of symbol maps is
   changed: Disallow the use of ->? in symbol maps, and take -> to
   mean whichever symbol (partial or total) is present in the
   signature. "a:?s then a:s" (and even "a:?s and a:s") can now be
   allowed without further modifications of the semantics.

We strongly favor 3). This solution does, of course, carry the
disadvantage that partial function symbols are treated syntactically
different in their definition and in symbol maps, but

-- A satisfactory way is provided of imposing totality on partial
   function symbols via extensions: Under the modified symbol functor,
   the signature morphism accociated to "a:?s then a:s" is an inclusion.

-- Partial symbols can be mapped to total ones by fitting morphisms
   (but not, of course, vice versa) without any further ado.

-- The expansion of instantiations to "<body> with <fitting> and
   <argument>" in the summary remains correct.

-- No artificial restrictions have to be imposed on symbol maps in
   translations to ensure finality (i.e. we do not have to explain to
   the user why "a:?s |-> a:s" is or is not forbidden). Translations
   are simply defined as final lifts; partiality or totality of a
   symbol is determined accordingly (i.e. a symbol is total in the
   result iff it is a renamed total symbol). Thus, renaming a partial
   to a total symbol (which is methodologically unsound) is
   automatically precluded (unless the partial symbol is identified
   with an existing total symbol).

-- This solution properly reflects the fact that totality should be
   regarded as an attribute of function symbols rather than as a
   part of their profile; this makes much of the logic behind renamings
   and instantiations more transparent.


Greetings,

Lutz and Till
-- 
-----------------------------------------------------------------------------
Lutz Schroeder                  Phone +49-421-218-4683
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen           
lschrode@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen 
http://www.informatik.uni-bremen.de/~lschrode
-----------------------------------------------------------------------------