[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Two proposals for additions to CASL
Dear All,
[REMINDER: the deadline for comments on the current CASL design
(v0.96) is on MONDAY 12 MAY! This is a STRICT DEADLINE. Any
comments or proposals after that date should address the version to
be submitted to IFIP WG 1.3 (v0.97), which is to appear on 14 May.
--PDM]
Let me put forward in this message two proposals for additions
(changes?) to the current CASL v.0.96, which emerged in a discussion
with Michel here in Paris. We claim no originality, of course, similar
ideas have been discussed, so let me just try to formulate them and
motivate as specifically as possible.
**********************************************************************
PROPOSAL 1. Add to the current data type declarations a possibility to
require reachability (generation by constructors) of the sorts
introduced.
**********************************************************************
After the recent changes we have removed any trace of a free
interpretation of datatype declarations, leaving them entirely as
abbreviations for a bunch of sort, constructor and selector
declarations with axioms linking constructors and selectors. This is
fine, and quite convenient both when the freeness is and when it is
not required (since the extra freeness requirements may be easily
imposed when a bunch of datatype declarations, perhaps together with
some extra axioms, are used as an extension).
However, a very typical situation is also when we want to indicate
that the data type declared is generated by the constructors provided,
without necessarily imposing freeness. There are many typical examples
around where one defines constructors of a data type without fixing
(perhaps: without fixing yet) the details of their mutual relationship
imposing at once the generation requirement. To indicate what I mean,
I add a trivial example of this situation at the end of this message
in appendix A :-); further examples, indicating other sources of such
a need as well, may be found for instance in Michel's thesis.
Admittingly, currently this is expressible by adding an explicit
sort-generation constraint after data type declarations --- but this
is really somewhat clumsy when the data types are complex, and we
believe that the schema is used often enough, perhaps even more
frequently than its "open" version without generation constraint, to
deserve its own abbreviation.
Of course, as discussed earlier for sort-generation constraints, we
need now to be able to declare a number of sorts with their generators
together, so it seems appropriate to go back to the earlier
type-definition-group concept (without explicit axioms in them
though). This would still expand to a bunch of declarations as before,
but now with an extra axiom stating the appropriate sort-generation
constraint.
To sum up, here is a possible way to realise the above idea:
BASIC-ITEM ::= ... | DATATYPE-GROUP
(removing DATATYPE-DECL as a case for BASIC-ITEM)
DATATYPE-GROUP ::= datatype-group OPENNESS? DATATYPE-DECL+
OPENNESS ::= open
and leaving DATATYPE-DECLs as they were. I hope that the intended
meaning is obvious: open datatype groups would not impose the
sort-generation requirement, so that the set of constructors may be
further extended later on; non-open groups would impose the
sort-generation constraint thus fixing the set of constructors for the
sorts declared.
Of course the abstract syntax chosen and the names used above are a
bit ad hoc, so any better proposals would be welcome.
NB: It is perhaps worth noting that in the context of first-order
logic axioms, freeness does not in general impose reachability, see
appendix B.
**********************************************************************
PROPOSAL 2. Generalise sort-generating constraints as now given in CASL.
**********************************************************************
This is somewhat related to the previous proposal: I cheated a bit
above, since in fact the sort-generation constraint that is expected
from a datatype definition group in general cannot be now expressed in
the CASL language. The problem is that in the presence of subsorts,
and hence subsort embeddings and projections, we are not able to name
in CASL all the operations that occur in the many-sorted signature to
which an order-sorted signature expands: subsort embeddings and
projections remain anonymous.
It is however easy to come up with examples (for a trivial case, see
appendix C) where at least subsort embeddings are needed to express
the sort-generation requirement one might want.
The most general form such a new sort-generation constraints might
have therefore is:
SORT-GEN ::= sort-gen SORT+ GENERATOR*
GENERATOR ::= EMBEDDING | PROJECTION | FUN-SYMB
EMBEDDING ::= embedding SORT SORT
PROJECTION ::= projection SORT SORT
I hope that the meaning is clear: a SORT-GEN as above expands to a
sort-generation constraint in the many-sorted institution with the
corresponding function symbols given either by their names or as
implicitly named subsort projections and embeddings.
I believe that some generalisation in this direction is necessary, so
I put the above forward.
Of course, one might wonder now about some exact details:
i) are projections necessary in the above?
I have not checked all the details, but I believe the answer is
negative: any sort-generation constraint with a projection seems to be
equivalent to the same sort-generation constraint with this projection
and its target (sub-sort) removed. Can somebody from the subsorting
group check that this is in fact true? Then the PROJECTION case for
the GENERATORs might be removed.
ii) do we have to indicate both the source (sub)sort and the target
(super)sort for embeddings?
If the SORT-GEN constraints a single sort only then indicating its
subsort would be sufficient here. However, if there are two sorts with
a common subsort constrained simultaneously, and we want to have
embedding from this subsort to one but not the other of the
constrained sorts as a generator, then I do not think we can do
without an explicit indication of the target. A possible slight
modification of the syntax to cater for both possibilities might be:
EMBEDDING ::= embedding SORT SORT?
where in the case the target sort is not given, all subsort embeddings
from the given SORT to the sorts being constrained are taken (similar
modification for PROJECTION is possible as well, if PROJECTIONs would
remain).
NB. It seems also true that an equivalent sort-generation constraint
in the form available so far can be expressed but at the expense of
introducing either extra function symbols or overloading some of the
once which are already in the signature --- this seems clumsy enough
that it is not worthwhile to follow, I think. Hence the above
proposal.
NB'. I presume that the meaning of sort-generation constraints is
given according to our general claim for sentences in Sect.3.3: that
they (and hence their semantics as well) are reduced to the "ordinary
many-sorted sentences for the associated many-sorted signature".
**********************************************************************
This seems enough (too much? :-) for one message!
With very best regards,
Andrzej (and Michel --- good things here are from both of us, the
mistakes and bad ideas are mine!)
==============================================================================
Appendix A: a trivial example to motivate proposal 1:
---------------------------------------------
sort ELEM
datatype declaration BUNCH = empty | add ELEM BUNCH
predicate is-in : ELEM BUNCH
variables e, e': ELEM, B, B': BUNCH
axioms not is-in(e, empty)
is-in(add(e',B)) iff (e=e' or is-in(e,B))
function union: BUNCH BUNCH -> BUNCH
axioms union(empty, B) = B
union (add(e,B),B') = add(e,union(B,B'))
---------------------------------------------
Now, an obvious property one would like to get:
is-in(e,union(B,B')) iff is-in(e,B) or is-in(e,B')
does not follow without induction, so we do need to impose the
appropriate generation constraint on BUNCH (intuitively expected here
anyway, in our view) to get what we want.
Of course, there is no intention to impose freeness in the above
example (this would limit the class of models to lists, essentially).
==============================================================================
Appendix B: freeness does not in general impose reachability,
so
free (datatype-group datatype-decls;
axioms)
may have a different semantics than
free (datatype-group open datatype-decls;
axioms).
For instance:
free (datatype-group open sort N = 0 | suc (N);
exists-uniquely x:N. suc(x)=x )
specifies up to isomorphism the model with the carrier that consists
of 0, suc(0), suc(suc(0)), ..., some-omega = suc(some-omega), which is
not reachable.
==============================================================================
Appendix C: a trivial example of a data type with a subsort:
---------------------------------------------
sort POSITIVE-NUMBERS
datatype group NUMBERS = POSITIVE-NUMBERS | minus (NUMBERS)
---------------------------------------------
The implicit sort-generation constraint should require that each
NUMBER is either (an embedding of) a POSITIVE-NUMBER, or is built from
such by (a few applications of) the unary minus operation. As far as I
can see this is not currently expressible in CASL as a SORT-GEN
without some tricks.
==============================================================================