RE: Subsorting in CASL

[tarlecki@mimuw.edu.pl]

[[[ I have sent the text of this message to Till before sending it
to the cofi-semantics --- I'll mark our common conclusions by "TM+AT"
below.

To sum up: our joint view is that the proposal implied by the message
from Till and Lutz will not lead to any modification of CASL design
and the overall meaning of its constructs. However, the idea may lead
to reformulation and nicer presentation of some parts of the semantics
of the language, notably for architectural specifications. This will
be worked out by the authors of the semantics, and more detailed
conclusions will be presented at this list (when some of us are back
from our summer holidays :-).

Best regards,

Andrzej Tarlecki
]]]

Dear Semanticists,

A few comments on what Till and Lutz wrote in their message of 7 Jul
2000 regarding subsorting in CASL (I will not repeat what they wrote,
trying to use below their notation and terminology).

As I wrote in my immediate comments, the message presents quite an
interesting and perhaps worth pursuing idea.  The main question for
this list and for us now though is what it can bring to CASL. Here,
I'm afraid, I view things somewhat differently than what the message
from Till and Lutz seemed to imply.

In the semantics of structured specifications, as far as I can see,
the proposal affects instantiations of generic specifications and
unions of specifications. In both cases, for the user it means that
some stronger well-formedness conditions are imposed: some of the
instances of the use of these constructs cease to be well-formed, but
once a specification is well-formed, it has the same class of models
as in the current semantics.

For instantiations of generic specifications: Till and Lutz propose
that an extra requirement is added to make sure that the construction
such as used now in CASL yields a pushout in enriched-CASL-Sign
category (which implies the current condition that it yields a pushout
in the current CASL-Sign category). This ensures that models may be
amalgamated "along" this pushout. I can only add that I would guess
that the implication in the opposite direction is true as well: if the
construction does not yield a pushout in enriched-CASL-Sign then there
are models over the signatures involved, with common reducts, that
cannot be amalgamated to a CASL model. As Till and Lutz wrote, I would
also guess that this condition is not decidable (Bartek Klin's result
on undecidability of the similar condition for unit expression in
architectural specification can probably be adapted to this case as
well).

On one hand, since I am not a great admirer of instantiations with
arbitrary fitting morphisms, this further restriction would not bother
me either. On the other hand, a very similar problem with undecidable
condition in architectural specifications made us to remove it from
the static semantics (in spite of the existence of a reasonable
"practical approximation" decision procedure) on the grounds of the
principle that static semantics should be decidable.

[[[ TM+AT: a reasonable conclusion at this point is that the static
    semantics of instantiations remains as it is now, with a decidable
    and weaker than suggested by Till and Lutz condition, while the
    tools should implement some reasonable check of the stronger
    condition and issue a warning in case amalgamability of models
    along the instantiation pushout is not established by the
    tool. ]]]

I have more troubles with the consequence of the proposal for unions
of specifications. For me, union has no hint of any constructivity
requirement, so the proposal to impose the requirement of
amalgamability of models here (which again is what Till and Lutz
propose, as far as I can see) cannot really be justified.  A typical
specification that would become ill-formed is something like the
following:

	{sorts a < c, a < b}  and {sorts b < c}

So, the following would also be ill-formed:

	{ {sorts a < c} and {sorts a < b} }  and {sorts b < c}

And here comes a surprise --- the following:

	{sorts a < c} and { {sorts a < b} and {sorts b < c} }

seems to be well-formed under the proposal. (Perhaps it would be
easier if I wrote Int, Rat, Real for a, b, c, respectively --- it
seems strange that some groupings of subsort requirements would be
preferred over others.) Aha: also, since the proposal is not meant to
affect basic specifications, writing the same subsort requirements in
any order and/or grouping within a basic spec would remain okay.

Not only we loose some expected formal properties of union here, the
last example also hints at a certain (intuitive more than technical!)
inconsistency of the proposal with the current CASL design. In the
enriched-CASL-Sign, subsort embeddings have no identity we can write
in CASL syntax --- since there may be more than one embeddings between
two given sorts, we can no longer name them by giving just the source
and target sorts. Again guessing, if I was to design a formalism
around the proposed idea then I would allow/require embeddings to be
named.

[[[ TM+AT: while the latter point would be valid only if one really
    intended to make enriched-CASL-Sign available to the user of the
    formalism, the unexpected consequences for union presented above
    are indeed quite disturbing. The proposal by Till and Lutz can be
    modified so that it does not affect union at all, and so no extra
    condition would be imposed here. ]]]

There is very little about architectural specifications in the text of
the message from Till and Lutz, so I am not sure what kind of
consequences they have in mind. One interpretation would be that quite
the same conditions as for structured specifications are imposed on
the corresponding constructs on units in architectural
specifications. This would be too naive though, as certainly some
sharing analysis would have to be added. I am not sure to what extent
the formulation of amalgamability conditions via enriched CASL
signatures would still remain simpler than what we have now. For the
user though, my guess would be that very little (if anything) would be
changed --- there still would be some proof obligations to ensure that
the constructions on models are well-defined in the given
specification context.

[[[ TM+AT: No change to the overall design of architectural
    specifications was intended --- the proposal concerned the exact
    way the semantics as adopted after the last meeting would be
    formulated, and there indeed enriched-CASL-Sign may prove useful
    to formulate an abstract institution-independent semantics, to be
    further supported by "cell conditions" as their specific
    realization in this specific institution. ]]]

Finally, let me go through the advantages Till and Lutz list:

* amalgamation and preservation of conservativity along instantiations
  for instantiations of generic (structured) specification: this
  indeed would hold, but more by the force of an explicit (probably
  undecidable) condition to impose this, than by some miracle.

  [[[ TM+AT: within the current design similar effect may be achieved
      by considering the extra condition explicitly when needed, and
      having tools to issue warnings whenever it cannot be discharged
      by the tool. ]]]

* Craig interpolation: we would gain a bit here (since the easiest
  counterexamples to Craig interpolation in CASL are based on pushouts
  that do not admit amalgamation in general, so would be excluded
  here) but we still would be far from having it for the language
  (Tomek Borzyszkowski's example still works, so we have to limit
  attention to morphisms injective on sorts, and probably exclude
  generation constraints). BTW: I cannot see why we would have to
  resort to enriched-CASL-Sign in the "standard
  institution-independent proof calculi"; in the worst case,
  enriched-CASL-Sign would only be used in the completeness proof.

  [[[ TM+AT: informally, it seems that in the "enriched-subsorted
      institution", Craig interpolation would hold, roughly, to the
      same extend to which it holds in the many sorted institution.

      Unfortunately, there is little hope for completeness of proof
      calculi for full CASL (for instance, because of the use of
      freeness and generation constraints), so any such completeness
      claim or any effective proof technique would be applicable to
      some part of the language only. It is indeed likely that this
      parts would exclude "strange" instantiations of generic
      specifications --- but this is independent from the core of the
      language design. ]]]

* institution independence of the static analysis for architectural
  specifications: I cannot quite see that this would bring any
  immediate benefits over what can be done now. This perhaps offers
  just a nicer formulation of what we have --- will have :-( --- in
  the current terminology. In fact, by considering sharing maps in the
  analysis of the conditions to ensure that unit amalgamation and
  translation taken are defined, we effectively deal with multiple
  subsort embeddings already (and indeed require that they all are
  proved to coincide).

  [[[ TM+AT: as concluded above, the proposed idea might indeed be
      useful to reformulate the presentation of the semantics of
      architectural specifications. We will check this and use as
      appropriate in the next release of the semantics (soon!). But
      this will not affect the design of this part of the language,
      nor the overall meaning of architectural specifications. ]]]

JOINT CONCLUSION (TM+AT): The proposal by Till and Lutz should not
lead to any modification of the current design and overall semantics
of CASL constructs. The consequences for union are disturbing enough
that no modification is acceptable here. As for the instantiation of
generic specifications: tool designers can decide how strong a
condition should be checked here, although we definitely would like to
see a warning that instantiation does not necessarily admit model
amalgamation. As for architectural specifications: the proposal does
not affect their design visible to the user, but will perhaps affect
the details of the formulation of their semantics.

With best regards,

Andrzej Tarlecki