Partial OSA

[pdmosses@brics.dk (Peter D. Mosses)]

First of all, many thanks to Maura for the preceding message, which is a
fair review of our recent discussions on possible solutions for the problem
of sorts becoming subsorts in extensions.  Here is some more motivation,
followed by the tentative details.  Sorry about the length...

Until very recently, I had been inclined to support the proposed CL
treatment of subsorts as predicates - accepting that CL should be based as
much as possible on the well-known notions/dogma of many-sorted algebra.
Moreover, in universal OSA, a subsort is simply interpreted as a subset of
the single universe, and a monadic predicate in CL would be a subset of the
carrier for the argument sort; the conceptual gap between the two didn't
seem so wide.

However, I cannot see how we can explain to users (even imaginary ones :-)
that the only way to have Nat as a subsort of Int is to specify naturals
and integers in the same module (similarly for rationals Rat, etc.) - or
explain why our library of standard specifications consists of some
necessarily-huge modules (having to incorporate all imaginable potential
extensions!).

Either we should admit that we cannot provide subsorts at all in CL (only
some fancy notation for using predicates in functionalities) or we should
give them their proper status as sorts in signatures (with notation for the
corresponding predicates and casts built in, as before).

While pondering this dilemma, it occurred to me that a semantics inspired
by universal OSA might actually *simplify* the proposed CL foundations:
instead of all those functionality-indexed families of interpretations, one
can make do with a *single* interpretation for each symbol!  Moreover, the
presence of *partial* functions might also *simplify* the treatment of
retracts in OSA (see JG's follow-up to my earlier question to this point).
Finally, one might avoid complicated conditions on signatures (which can be
a deterrent to using OSA).

A very tentative proposal is provided below.  Suggestions for improvement
are most welcome!  The only drawbacks of which I am currently aware are:

- An overloaded function f:s'->s and f:s''->s must be interpreted
consistently, i.e. if a:s' = b:s'' then f(a)=f(b) is required to hold...
Personally, I could live with this!  If I want two functions that may
behave differently on the same value, depending on how we classify it in a
sort, I actually prefer to use different function symbols, e.g., f|s',
f|s''.  Likewise for predicates.  But this issue appears to be quite
controversial...

- The technical details concerning morphisms, initiality, etc., have *not*
been worked out, due to lack of time; perhaps it will turn out that they
require complicated conditions.  But in any case, they would need working
out *before* the meeting in Munich for this proposal to be considered at
all seriously.

Please let me or Maura know if you would have time (and inclination) to
help with resolving this problem by e-mail (or at AMAST) next week.

Cheers

Peter Mosses

---------------------------------------------------------------------

A Very Tentative Counter-Proposal for Subsorts in CL
by Peter D. Mosses
Version 0.1

The definitions sketched below are intended as an alternative to the
partial Sigma-structures defined in "A note about basic concepts and
structures" by Egidio Astesiano et al. (see the CoFI Tentative Design
Proposals).  The aim is to circumvent the problem noticed with the proposed
treatment of subsorts as predicates, whereby a module NAT specifying Nat as
a sort unfortunately cannot be extended to a module INT where Nat < Int.
As subsorts are very useful in requirements specifications for conceptual
clarity, it is important that they be provided in a satisfactory way in the
CoFI Common Language.

A basic tenet is that if subsorts are used in the same way as sorts (e.g.
in functionalities, variable declarations) they should be treated as sorts.
Predicates are used for building formulae, which is rather different, in my
opinion.


Basic Concepts
==============
Partial Subsorted Signatures
----------------------------
A partial subsorted signature Sigma = (S, <, Omega, Psi, Pi) consists of

* a set of sorts S;

* a partial order < on S;

* two (not necessarily disjoint!) S* >< S -indexed families Omega and Psi
of total and partial function symbols;

* an S+ -indexed family Pi of predicate symbols.

(Note that no conditions of regularity, coherence, etc., are imposed.  This
may give problems with initiality in equational specifications...  Perhaps
the partial order need not be strict, or it could be a pre-order?)


Partial Subsorted Sigma-structures
----------------------------------
Given a partial subsorted signature Sigma = (S, <, Omega, Psi, Pi) a
partial subsorted Sigma-structure A is a quadruple consisting of:

* a carrier set |A|;

* a subset s^A <= |A| for each s in S, such that
  whenever s_1 < s_2 there is the inclusion s_1^A <= s_2^A;

* a partial function f_A from |A|^n to |A| for each n-ary f in Omega U Psi,
  such that whenever f in Omega(Psi)_{s_1...s_n,s} the restriction of f_A
  to s_1^A >< ... >< s_n^A is a partial (resp. total) function to s^A;

* a predicate P_A <= |A|^n for each n-ary P in Pi.

(Surely that's simpler that the original definitions?)

Terms may be inductively defined as in standard total many-sorted logic,
disregarding the subsort ordering (!) and the distinction between total and
partial function symbols, i.e., the many-sorted signature is (S, Omega U
Psi, Pi).

The idea is to keep the foundations as simple as possible, requiring
inclusions and retracts to be *explicit* in terms.  If desired, term
formation could be relaxed to leave such things implicit.  But perhaps
it'll be easier to define many-sorted sublanguages with the indicated
approach.   It would seem quite natural to leave inclusions implicit at
least.

Basic Constructs
================
Subsort Predicates
------------------
For each s_1 < s_2 the predicate is-s_1 in Pi_{s_2} is provided.

is-s_1(x) yields true iff x in s_1^A.

The notation e.g. (x:s. phi(x)) may be allowed for an anonymous subsort s'
< s such that forall x:s. is-s'(x) <=> phi(x).  Such subsorts may be useful
in indicating the subsets on which partial functions become total; but they
do not affect well-sortedness of terms, as the anonymous subsort is to be
replaced by the supersort when obtaining a signature from a specification.

Terms
-----
For each s_1 < s_2 the inclusion function in^{s_2} in Omega_{s1,s2} and the
retract on^{s_1} in Omega_(s2,s1} are provided.  The interpretation
in^{s_2}_A is the identity inclusion, and that of on^{s_1}_A is identity on
s_1^A and otherwise undefined.  (Both functions could be written as cast^s,
if desired.)

Abbreviations
-------------
Terms may be abbreviated in the specification language by omitting
inclusions and retracts: when the sort of an argument is s_1 and the sort
expected by the function is s_2, the insertion of in^{s_2} is implied when
s_1 < s_2, and of on^{s_2} when s_2 < s_1.  In the case of ambiguity
arising due to overloaded functions, the term is illegal (but can be made
legal by inserting explicit inclusions or retracts).

An alternative formulation allowing the same abbreviations would be to
generalize the argument and result sorts of all function symbols to the
largest sorts including them (more precisely: to all combinations of
maximal sorts including them, assuming such unusual orderings on sorts are
allowed), so that only inclusions would need inserting.

Note that if a top sort is provided, term formation is unrestricted.
Having several maximal incomparable sorts approximates many-sortedness.

In any case, the problem with iterations of pop disappears (as in OBJ):
pop(pop(s)) abbreviates pop(on^{nestack}(pop(s))).  But here, we have
simply not(defined(on^{nestack}(empty))).

That's it.  PDM has *not* yet tried to obtain any results about such
partial subsorted structures, e.g., initiality, or conditions for
discretely-sorted specifications to correspond to many-sorted ones...  Such
things would need working out before the Munich meeting for this proposal
to be taken seriously.