partial and order sorted algebra

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

[This is the ONLY reaction to the Tentative Design Proposal that I've
received so far!  Please note that although the deadline for comments
to be considered at the meeting is not until noon on 5 July, reactions
that are to be discussed on this list in advance of the meeting should
be sent AS SOON AS POSSIBLE THIS WEEK - especially since some of us
will be away from e-mail at AMAST next week.  -PDM]

Dear CoFIholics,

As most of you know, Ive left Oxford and am now at UCSD, and so am no
longer a European, but I would still like to see the CoFI project
succeed, and am willing to put a little time into it.

Maybe it is too late for this, but I cant help wonder why you are
leaning towards partial algebra instead of order sorted algebra?  To
me (you wont be surprised to hear), the advantages of OSA are so
obvious: you get the convenience of total algebra, the same rich
theoretical superstructure (initiality, Birkhoff, Tarski-McKinsey,
etc.), the ability to express all partial functions (including all
partial recursive functions), plus lots of other neat things, like
error definition and recovery, coercions, and sort constraints.

Are any of you maybe worried about partial recursive functions whose
domains cant be defined equationally?  This is actually easy in OSA:
first define the ADT of values (e.g., the naturals), then overload all
operations on an "error" supersort; then define the function on the
supersort.  Now when it terminates, it will automatically have its
value in the subsort; and when it doesnt, it wont (there will be an
infinite number of terms of the supersort that it is equal to, but
none of them will be a data term).

The key to the more exciting uses of OSA is retracts, and the main
theorem is that they give a consistent extension of the original
theory.  But then one can play some very nice games in the retract
theory, like writing rules that match the retracts to do error
recovery and automatic coercions.  Of course, retracts were introduced
to allow OSA terms like pop(pop(S)) to be well-formed [under the
signature with pop: Nestack->Stack, Nestack < Stack, S: Nestack, no
error supersorts].  They are total functions from the supersort to the
subsort, with a retract equation.

[Sorry, but I still don't see how applying a retract to a value
*not* in the subsort can give a defined value in the subsort.  E.g.,
if the retract is r: Stack->Nestack, the value of r(empty) worries me.
-PDM]

Ordinary OSA doesnt have higher order functions, but I would argue it
is better to have the base language first order, and then get the
higher order power from the module system; I claim to have shown (by
example, not theorem) that OBJ style modules really do give you
everything you would want from higher order functions, with greater
flexibility and reusability, all in a first order setting.

Have people on the CoFI language team looked at "An Oxford survey of
order sorted algebra" and "Higher order functions considered
unnecessary for higher order programming"?  The former gives some
examples of error handling, coercions (e.g., automatic coercion
between cartesian and polar coordinates), and other things, in OBJ3.
The latter contains the parameterized programming examples.

Peter Mosses sent me a message on his proposal to combine order sorted
and partial algebra; it is attractive and politically correct, but i
worry that it may not be so easy to get Birkhoff results, what with
explicit inclusions and retracts.  [That proposal has *not* yet been
sent to cofi-language, pending conclusion of discussions with Maura
Cerioli on the pros and cons of different ways of solving the problem
with treating subsorts as predicates - an issue raised in the "Note on
basic concepts and constructs", section 2.1.2. -PDM]  But my main
problem is that most everything you want can be done with ordinary
OSA, and I just cant see any advantage to having two ways of doing
things.

Peter has a complaint that an OSA spec and its semantics are more
complicated than you might think; I no longer recall the details of a
long discussion we had about this [I can probably find my archives, if
needed :-) -PDM] but maybe I can get away with considering it a matter
of how you want to look at a theory.  If you want to be pedantic, you
should consider the spec to be a theory inclusion, from the given
theory to its retract completion; but i think you could also just
consider the given theory to be an abbreviation for the completion.
Then I think (if im not forgetting some subtle point) the models are
just the models of the retract theory.  And of course (see below) you
can enrich the retract theory with some other clever equations.

Anyway, it seems a big loss not to have error messages, handling,
coercions, etc.; to me, the main problem with partiality is that it
does not allow this kind of thing; and moving instead to Scott's
bottom, strictness, domains, etc., is rather complicated and not so
algebraic.

Below I include some OBJ code for automatic coercion between cartesian
and polar coordinates, from the "Oxford Survey": some functions are
defined on one representation and others on the other; but you can
write any term you like, and OBJ will automatically change
representations for you, just the right way!

I might add that this paper also works out how to do overwriting
(which is overloading with a really different semantics) using what we
called signatures of non-monotonicities.  And it has some
(executable!) examples of sort constraints, e.g., a bounded stack.

With all best wishes to all my old friends,

Joseph

*************************************************************************
Joseph A. Goguen, Dept. Computer Science and Engineering, University of
California at San Diego, 9500 Gilman Drive, La Jolla CA 92093-0114, USA

email: goguen@cs.ucsd.edu
       jgoguen@ucsd.edu

www:  http://www.comlab.ox.ac.uk/oucl/people/joseph.goguen.html
      http://www-cse.ucsd.edu/users/goguen    [nothing here yet!]

phone: (619) 534-4197 [my office]; -1246 [CSE dept]; -7029 [CSE fax]; 
       (619) 822-0702 [secy: Lisa Bodecker]

office: 3131 Applied Math & Physics Bldg.


******************************************************************************
  ***> coercions for points in Cartesian and Polar coordinates
  ***  requires PosFLOAT with builtin subsorts Angle < PosFloat < Float

  in PosFLOAT

  *** notation for squaring
  obj SQ is pr FLOAT .
    var F : Float .
    op _**2 : Float -> Float [prec 2] .
    eq F **2 = F * F .
  endo

  *** points and operations on points
  obj POINT is pr SQ .
    sorts Point Cart NzPolar Origin Polar .
    subsorts Cart Polar < Point .
    subsort NzPolar Origin < Polar .
    op <_,_> : Float Float -> Cart .
    op x_ : Cart -> Float .
    op y_ : Cart -> Float .
    vars X Y : Float .
    eq x < X, Y > = X .
    eq y < X, Y > = Y .

    op [_,_] : PosFloat Angle -> NzPolar .
    op origin : -> Origin .
    op rho_ : Polar -> Float .
    op theta_ : NzPolar -> Angle .
    var Rh : PosFloat .  var Th : Angle .
    eq rho [ Rh, Th ] = Rh .
    eq theta [ Rh, Th ] = Th .
    eq rho(origin) = 0 .

    cq r:Cart>NzPolar(< X, Y >) = [sqrt(X **2 + Y **2),atan(Y / X)] if X > 0 .
    cq r:Cart>NzPolar(< X, Y >) = [sqrt(X **2 + Y **2),pi + atan(Y / X)] if X < 0 .
    cq r:Cart>Polar(< X, Y >) = [sqrt(X **2 + Y **2),atan(Y / X)] if X > 0 .
    cq r:Cart>Polar(< X, Y >) = [sqrt(X **2 + Y **2),pi + atan(Y / X)] if X < 0 .
    cq r:Cart>NzPolar(< 0, Y >) = [ Y, pi / 2 ] if Y > 0 .
    cq r:Cart>Polar(< 0, Y >)   = [ Y, pi / 2 ] if Y > 0 .
    cq r:Cart>NzPolar(< 0, Y >) = [ - Y, (3 * pi) / 2 ] if Y < 0 .
    cq r:Cart>Polar(< 0, Y >)   = [ - Y, (3 * pi) / 2 ] if Y < 0 .
    eq r:Cart>Polar(< 0, 0 >)   = origin .
    eq r:Polar>Cart([ Rh, Th ]) = < Rh * cos(Th), Rh * sin(Th) > .
    eq r:Origin>Cart(origin) = < 0, 0 > .

    op d : Cart Cart -> Float .
    op _+_ : Cart Cart -> Cart .
    var X1 Y1 X2 Y2 : Float .
    eq d(< X1, Y1 >, < X2, Y2 >) = sqrt((X2 - X1)**2 + (Y2 - Y1)**2).
    eq < X1, Y1 > + < X2, Y2 > = < X1 + X2, Y1 + Y2 > .
  endo

  obj TEST is pr POINT .
    ops p1, p2, p3 : -> Polar .
    eq p1 = [ 1, pi ] .
    eq p2 = [ 2, - pi ] .
    eq p3 = [ 1, - pi ] .
  endo

  red x p1 .
  red y p1 .
  red d(p1,p2) .
  red p1 + p2 .
  red rho(p1 + p2) .
  red theta(p1 + p2) .
  red d(p1,p3) .
  red p1 + p3 .
  red rho(p1 + p3) .
  red theta(p1 + p3) .

  obj SCALARM is pr TEST .
    op _*_ : Float Polar -> Polar .
    op _*_ : Float Cart -> Cart .
    vars F X Y : Float .  var Rh : PosFloat .  var Th : Angle .
    eq F * < X, Y > = < F * X, F * Y > .
    cq F * [ Rh, Th ] = [ F * Rh, Th ] if F > 0 .
    cq F * [ Rh, Th ] = [ - F * Rh, pi + Th ] if F < 0 .
    eq 0 * [ Rh, Th ] = origin .
    eq F * origin = origin .
  endo

  red 2 * origin .
  red (2 * origin).Cart .
  red 2 * p1 .
  red (2 *(p1 + p2)).Cart .

[[All this runs!]]