Re: partial and order sorted algebra

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

In reply to:

.......

  [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]

Peter, thanks for your question; I dont think the answer is written down
anywhere -- it's part of OSA folklore -- but I'm glad to have the chance to
write it.

First, retract terms like r(empty) are very important as parts of error
messages and hence error handling.  For example, retract terms are crucial to
the multiple representation example in my original message.  But your worry is
do they somehow get in the way?

The street-smart wise-guy short answers is: forget it; if you dont bother them
then they wont bother you.

The more pedantic, precise answers is this: let T be a given OSA theory and
let T^ be ist retract extension.  then the inclusion T -> T^ gi9ves rise to a
forgetful functor U: Alg(T^) -> Alg(T), which forgets just the terms you dont
like.  Also, U has a left adjoint F which freely adds these terms to any given
T-model, including the initial T-model I; and F(I) is an initial T^-model.
What this means is that you can safety forget these terms if you dont need
them since there is a nice initial model without them, and you can use them if
you want them, since there is a nice initial model with them.  In short, see
the short answer.

(I hope Ive answered your actual question, and not a different one!)

[Yes, thank you!  -PDM]

Joseph