Partial OSA

[cerioli@disi.unige.it (Maura Cerioli)]

(PDM= Peter Mosses, MC=Maura Cerioli, JG=Joseph Goguen)

Trying to summarize some discussions about subsorting between PDM and me
(MC), I'll present first the statement of the problem as I understand it
and then my personal point of view (Peter, you could add yours too, so we
will have the complete fresco). [OK, but in a separate message. -PDM]
Although this message is later than JG's email on OSA and OBJ, it has been
thought before (and it represents a discussion that has taken place during
last week mostly); thus it is in by means an answer to JG.

The starting point has been pointed out by PDM:
if a data type with principal sort s has been defined, then it cannot be
painlessly extended to a larger data type s' with s<s' within the currently
suggested implementation of subsorting, as s is declared as a sort, while
subsorts of s' should be predicates.

This is caused by the fact that subsorting is based on the idea that sorts
are used to classify the elements of a universe, while in many-sorted
(partial or total) first-order logic sorts are used to denote separate
universes whose intersection is not interesting to discuss.
Thus, using predicates to classify the elements within a sort, we can
simulate each order-sorted specification provided that we know in the
beginning the maximal sorts of the order, but we cannot, in some sense,
change our mind in the middle of the specification process: a sort cannot
become a subsort.

Therefore the implementation of subsorting we agreed on, using predicates,
is not flexible enough for dealing with extensions.
This leads to reconsider the problem of order-sorted representation in CL.

In principle the possibilities are 3:
1) We give up this extension capability and let the subsorting
   approach as it is at the moment.
2) We change the implementation of subsort declaration in CL
   to the injection/retraction style.
3) We completely change the semantics for CL, introducing directly
   an order on sorts.
The first doesn't seem so appealing for order-sorted users, so let us
consider the others.

2 In my previous notes I suggested an implementation of subsorting
  where each subsort is actually a sort, with an embedding (that is a
  total injective function) from the subsort to the supsort.
  The problems with this approach is that the problems for well-sortedness
  of terms known in standard osa are present here as well.
  But adding retracts, that are partial inverses of the embeddings and
  can be strong-equationally specified, we get the same expressive
  power of order-sorted with retracts, without having the junk generated
  by the application of a retract to elements outside the subsort in
  the model carriers.

  Some problems could arise (as well as in any order-sorted approach) for
  the definition of parser, if the embedding and retraction
  mechanism is left implicit.
  But we would have subsorts as *real* sorts in the signature,
  with the capability of extending them, stating the functionality for
  partial functions (PDM noticed that [taking the interpretation proposed
  in the Note on Basic Concepts and Constructs] the declaration nat < int,
  minus:nat*nat-o->nat, minus:int*int-->int expands to
  is_nat predicate on int, minus:int*int-->int confusing the two
  incarnations of minus and losing the information about the typing
  for the minus on nat).

  Notice, however, that the model class of this expansion would allow
  also models where subsorts are *isomorphic* to subsets of the
  supersorts and not directly included.
  I, personally, don't see any problem in this approach, that is much more
  coherent with the disregarding of actual data representation in many-sorted
  frameworks and with the implementation of programming languages, where
  subtypes can have different binary representations (think of integer and
  real in Pascal, for instance).

3 There are two approaches to order-sorted: the universal (A) and
  the overloaded (B) depending on the fact that the properties are imposed
  on elements that happen to belong to the carrier of some (sub)sort or
  only to those that (are denoted by a term that) can be deduced of
  that (sub)sort.
  (for a much better presentation of this distinction, see PDM'paper
  in WADT91) [which refers to more original/qualified sources! -PDM]
  A REAL subsorting is based on the idea that each term should
    be evaluated on the same value, if the same values are substituted
    for its variables, disregarding its declared type.
    In other words function symbols (disregardyng their arity) are defined
    as partial on the universe and their interpretation in each carrier
    is the restriction of the common interpretation to the domains.
    Thus if f:s -> s' and f:s_1 -> s_1' are both declared and the same value
    x belongs to both s and s_1, than a unique value f(x) belongs to both
    s' and s_1', interpreting cast(f(x),s') and cast(f(x),s_1').
    In my (MC) opinion, since this is the intuition, this kind of
    subsorting is better represented in homogeneous frameworks, like
    unified algebras, ETL or G-algebras and shouldn't be mixed
    with many-sorted style.
  B This second case is much closer to standard many-sorted approaches;
    actually the model classes are a representative subclass of the model
    classes of standard many-sorted, where the order relation has been
    substituted by explicit injections (see the original paper on OSA).
    The problem here is that if no retracts are allowed, than the use
    is really inconvenient (the well-known problem of
    pop(pop(push(push(..)..) being not well-formed), but to have retracts
    within the theory (not at a meta-level as in standard OSA), partial
    functions (or at least those partial functions representing retracts)
    are needed (or the results of retracting elements not in the subsorts
    introduce lots of junk in the carriers).
    Moreover using retracts the specifications and their use
    is more or less (in my personal opinion) an automatized version
    of error algebras.
    Adding an order on sorts within our logic is possible and probably
    shouldn't cause more problems than the same introduction in total
    order-sorted. But I think that whoever has taught an order-sorted
    language to *real* people (degree students, engineers) with all the
    complications due to regularity and coherence conditions on signature,
    would think twice before trying to teach the same stuff AND, at the same
    time, the problems due to the possible partiality of function symbols.
  C PDM suggests another possibility, in the universal style, that is,
    roughly speaking, an order-sorted language with unsorted semantics.
    Some tentative definitions are appended at the end, but summarizing
    my understanding, signatures are many sorted signatures with an order
    on the sort set.
    The term formation is the standard many-sorted construction
    the order (and the distinction between total and partial) being
    disregarded BUT the semantic structures are unsorted algebras,
    where sorts are interpreted as unary predicates (the order is
    reflected by implication), possible overloading is solved
    in the ``universal'' style (so same-name = same-thing).
    Thus we would have, basically, an order-sorted presentation of
    unsorted structures.
    Some more work is needed before reaching some technical
    conclusion on this new theory.  [PDM claims that the ingredients
    are actually not so new: the notions of universal OSA - but dropping
    coherence/regularity - combined with those of partial functions and
    predicates, treating retracts as genuine partial functions (pace JG!).
    Axel Poigne proposed something analogous at an earlier WADT. -PDM]
    For the moment I could point out that the usual definition of
    initial models as quotients of standard term-algebras doesn't apply
    (actually standard term algebras are many-sorted, while in
    this approach algebras are unsorted).
    But, term-formation following the usual rules, the language is
    much cleaner that the corresponding unsorted theory.

MC's viewpoint
I believe that subsorting is a nice and clever way of representing some
partial functions (not all) and some unary predicates within a framework not
having explicit facilities for them, but that, having both features in CL
we should not encourage users and methodologies using subsorting.
However, I think that we need a subsort construct for people used to it.
But I don't think reasonable to complicate our clean partial theory if this
can be avoided. Therefore I'm strongly in favour of having any
implementation of order-sorted that can satisfy those who like that style
(who is interested should try to state whether (s)he is satisfied by any of
those we have suggested, or, if not, what needs modification), but NOT to
add an order on sorts.

Let me recall that the main (or at least the only known to me) usages of
subsorting are
- representing the domains of partial functions.
  This is restricted to functions whose domains can be statically built
  (==> decidable); moreover, unless product types are added to the signature,
  such function should be unary or their domain should be describable as
  s_1'*s_2*...with s_1' subsort of s_1, while if the domain is a sort of
  dependent type, the definition is much more complex.
  Of course having partial function within CL we don't need this facility.
- representing unary predicates and possibly stating
  that a predicate P on s implies a predicate Q on s (that is the subsort
  Q is a subsort of P)
  But we do have predicates! and implications.
- simulating quantification qualified by unary predicates
  (forall x:P.phi for forall x:s.P(x)==>phi)
  But, as the previous case, we have predicates and full
  first-order logic, so...
That's all folk :-)
Maura

[Please see the following message for the tentative definitions.  -PDM]