[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Subsorting in CASL
[[[ Dear Semanticists,
I forward below a message from Till Mossakowski suggesting a proposal
for an essentially new view of the semantics of CASL in some of its
technically difficult aspects. My immediate feeling, without studying
it in any detail, is that this is a very interesting proposal for
further interesting work and research at the moment. Whether we can
still adopt it for the semantics of CASL at the time when the dealine
for having it completely finished has passed a few times is another
question... All comments welcome!
Best regards,
Andrzej Tarlecki ]]]
Dear friends,
we (Lutz and Till) have spent some further thoughts on the
pushout problem, and we have come to an interesting proposal.
Remember that subsorting in CASL has severe drawbacks:
- the amalgamation property fails
- related with this, the semantics group has resigned from formulating
a static sharing analysis for architectural specifications
- also related with this is the failure of preservation
of conservative or definitional extensions along
instantiations
- the Craig interpolation property fails, which means
that standard institution-independet proof calculi
for structured specifications are not applicable
The main cause of these problems is that the subsorting
relations is interpreted via injections (and not via
subset inclusions) in the semantics.
However, the restriction to subset inclusions is
not the only way out: another way would be to
enrich the subsort relation, in order to capture
the fact that there can be *different* injections
between two given sorts.
We thus propose to work (in the semantics!) with an embedding
of signature categories:
CASL-Sign -------> enriched-CASL-Sign
where CASL-Sign is the usual category of CASL signatures,
and enriched-CASL-Sign is the category of CASL signatures
with the pre-order of sorts replaced by a category of sorts.
In the semantics, unions and pushouts would have to be taken
in enriched-CASL-Sign (which comes with a model theory
satisfying the amalgamation property), but it would be
required that the result again is *within* CASL-Sign,
that is, we get a standard CASL signature.
Thus, in the summary, the notion of signature would not
have to be changed. The only change would be to make
unions and instantiations (pushouts) a bit more restrictive.
E.g. the standard example for a pushout without amalgamation
spec sp [sorts s,t] = sorts s<t end
spec sp' = sp[sorts s<t] end
would not be legal anymore.
The restriction conditions can be fully understood only
in the enriched-CASL-Sign setting. A disadvantage also
is that they are probably undecidable. However, we have the
impression that there is an approximation algorithm
(that may output "don't know") which is sufficient to
resolve all practical examples. We think that this slight
drawback of this proposal is outweighted by the massive advantages:
- amalgamation holds
- the static sharing analysis for architectural specifications
can be formulated in an institution independent way,
assuming that the institution has some rather simple
amalgamability condition
- conservative or definitional extensions are preserved along
instantiations
- the Craig interpolation property probably holds, which means
that standard institution-independet proof calculi
for structured specifications are applicable
(one has to work in enriched-CASL-Sign here,
since the occuring pushouts will no longer stay
in CASL-Sign; however, in the light of the usual
encoding of subsorted into many-sorted logic
this is very natural)
We apologize that this proposal comes at a very late stage;
however, since it solves so many problems, we think it
is worth to consider it. We will write a study note
containing the technical details.
Greetings,
Till and Lutz
Technical disgression:
The category enriched-CASL-Sign is just CASL-Sign with
the sort system not being a pre-order but a category.
enriched-CASL-Sign is the right category to form
pushouts for a subsorts-as-injection semantics.
There is a left adjoint to the embedding of
CASL-Sign into enriched-CASL-Sign, it just collapses
hom-sets to one point (the result is a thin category,
which is just a pre-order). Pushouts in CASL-Sign are just
the collapsing of pushouts in enriched-CASL-Sign
(since left adjoints preserve colimits).
However, this collapsing destroys amalgamation.
Thus, instead of applying the collapsing, we just
have to *require* that the pushout in enriched-CASL-Sign
is already collapsed, i.e. is a pre-order.
This requirement is an elegant formulation of
the complicated cell conditions in the architectural
semantics from July 99. Of course, since Bartek Klin
showed these cell conditions to be undecidable,
also the requirement of the pushout in enriched-CASL-Sign
to be collapsed probably will be undecidable.
Thus, there is an undecidable condition in the
static semantics. However, the condition is
still practically decidable by restricting the
composition depth of cells to a certain value,
and output "don't know" in the case that the
algorithm has to check compositions of cells
beyond this composition depth (which practically
will never occur).
enriched-CASL-Sign leads to an institution with symbols
as follows: each object and each morphism in the category
of sorts leads to an own symbol.
The semantics of CASL would be best formulated within
enriched-CASL-Sign. The semantics of basic specs
can stay as it is. Only for the semantics of structured
and architectural specs, the signatures have to be embedded
from CASL-Sign into enriched-CASL-Sign.
The institution independent semantics of structured
specifications would have to be modified as follows:
the category of signatures comes along with a subcategory
of "admissble" signatures. The semantics only works
with admissible signatures. Unions and pushouts are
undefined if the result is not admissible.
The institution independent semantics of architectural
specifications would require that for a *final* union
Sigma_1 \cup Sigma_2, given a Sigma_1-model M_1
and a Sigma_2-model M_2 agreeing on the set of common
symbols of Sigma_1 and Sigma_2, an amalgamation
exists. (Probably for the exact formulation, one
would need to construct the intersection Sigma_1 \cap Sigma_2
and require that if M_1 and M_2 have a common
Sigma_1 \cap Sigma_2-reduct, then they are amalgamable.
Even better, by the finality of the union,
the diagram
Sigma_1 \cap Sigma_2 ------> Sigma_1
| |
| |
\/ \/
Sigma_2 ------------> Sigma_1 \cup Sigma_2
would become a pushout. Then, all what we need
is the classical amalgamation property.
(In CASL-Sign, finality of the union
just means that no new overloading relations
are generated, which, apart from the cell conditions,
is just the remaining condition which is there in the
architectural semantics from July 99.
In enreiched-CASL-Sign, finality of a union
additionally means that all commuting diagrams
of sort injections can be derived from commuting
diagrams in the united specifications.)
-----------------------------------------------------------------------------
Till Mossakowski Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen till@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------