Re: Partial OSA

[Joseph Goguen <goguen@cs.ucsd.edu>]

[This is the last message before I leave for Munich.  Forwarding of
messages to this list may be a bit slow next week, but please keep
writing and sending them, as the issues are important, I think!  -PDM]

Oh oh, it looks like those partial to partial algebra have some misconceptions
about order sorted algebra.  Let me start with Maura's list of things that 
subsorts are good for:

1. representing the domains of partial functions.  No, it is not restricted to
functions whose domains can be statically built (==> decidable); as explained
in my previous message, use of an error supersort for nontermination lets you
define any partial recursive function whatsoever.  And no, there is no problem
with domains that are not products of subsorts.  That is, you do not need sort
constraints for defining partial recursive functions.  And moreover, sort
constraints are not restricted to products of subsorts.  For example, in an
early paper we defined the domain for composition in categories with the
equation \partial_1(f) =  \partial_2(g).

2. representing unary predicates.  As noted above, one can also represent
n-ary predicates.

3. simulating quantification qualified by unary predicates.

BUT there are MANY more uses for OSA!  Those retract terms ARE NOT JUNK!!!
They are cute, informative, interesting and useful!  For example, they are the
basis for error handling and multiple representations (see the example in
earlier message).

Of course another advantage of OSA is that all the theory has been worked out.
And it is not that hard to teach; the technical papers take a pretty hard line
view, but an easier pedagogical approach can be found in my book "Algebraic
Semantics for Imperative Programs, with Grant Malcolm, just published by MIT
Press.  It works well in undergraduate classes.

Cheers,

Joseph