[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Comments on CASL 0.98
[Many thanks to Till for the detailed comments and careful discussion
of the various issues below!
N.B.:
Deadline for comments to be considered at the Amsterdam Meeting
of the Language Design Task Group:
12 noon on Tuesday, 23 September 1997.
--PDM]
Contents:
* Miscellaneous points
* Issue: empty carriers
* Issue: institution-independence
*** Miscellaneous points
p. 3, footnote 7:
This works only if false is an atomic formula, but
true and false are missing in the listing of atomic formulas.
p. 11, sentence in boldface in the middle:
It could be added:
... are *semantically* equivalent ..., *see 1.4 (satisfaction)*.
p. 15, first \item:
t' is the application of a *trivial* embedding to t
p. 15, third \item:
\leq_F has to be replaced by ~_F
(and similar \leq_P below)
p. 15, second paragraph:
Equivalence between fully-qualified atomic formulas
is the least *equivalence* ...
p. 22, instantiation of generics:
When proving cocompleteness of the signature category
of CASL, I encountered some technical complexity
with the treatment of the name space, that leads to
the following example:
PAR =
sorts s1, s2
ops f:s1->s1
f:s2->s2
BODY = PAR +
sorts s
s1,s2 < s
ops f:s->s
ACTUAL =
sorts s1, s2
ops g:s1->s1
h:s2->s2
Now consider a fitting morphism mapping the sorts identically,
mapping f:s1->s1 to g:s1->s1 and f:s2->s2 to h:s2->s2.
Then the pushout is BODY again, while the normal instantiation
rule would yield
RESULT =
sorts s1, s2, s
s1,s2 < s
ops f:s->s
g:s1->s1
h:s2->s2
but the induced symbol map from ACTUAL to RESULT is
not a signature morphism, since it does not preserve
the overloading relation ~_F!
Thus, the instantiation should be undefined in this case.
(Btw, Maura pointed out to me that this difficulty does
not arise with her proposal of having user defined
overloading relations. Also, the pushout construction
is technically simpler then. But I think we can live
with the above phenomenon.)
p. 23, first paragraph
"... the translation determined by fitting arguments
to parameters applies to the compoment ID+ of
the compound identifier as well."
But only if this translation can be determined
unambigously for unqualified ids. Otherwise,
the instantiation is undefined.
(See S-6, p. 72, Doubt 6.5)
p. 28, first paragraph
Why is linear visibility relativized with an "e.g."?
Do we have places with non-linear visibility at
the global level?
And in which cases is overriding forbidden, in which
not?
p. 29, 10.2, first paragraph
It is not possible to define the semantics of a DOWNLOAD
by a replacement of all references by the corresponding
specifications, because naming a specification has
a semantics: the local environment becomes empty.
(Andrzej has shown examples where the difference
becomes clear.)
p. 29, URL
The structure of DIRECTORY also is insignificant, ins't it?
*** Issue: Empty carriers
p. 44, Points for discussion, 1st item
Let me sum up some arguments pro and contra empty carriers:
Contra empty carriers:
- The interaction of empty carriers with global variable
declarations causes problems. There are two possibilities:
1. Either, we quantify over all
globally declared variables, then
var x:elem, s:stack
...
is_empty(empty)
behaves in a funny way,
or
2. we quantify only over the variables occurring
freely in the axiom.
This leads to a counter-intuitive semantical
consequence relation:
var x:s
foo(x)=a
foo(x)=b
does not have a=b, but only forall x:s.a=b as a consequence.
Is there a counter-intuitive example of more practical relevance?
- The embedding of CASL into FOL/HOL (for the purpose of
re-using theorem provers) becomes a bit more complex
when allowing empty carriers,
since typical FOL/HOL-theorem provers allow to derive
exists x:s. x=x
which semantically means that carriers have to be non-empty.
On the other hand, there are good translations of
FOL-with-empty-carriers to FOL-without-empty carriers
(see the study note "Overload resolution and theorem
proving for CASL").
Only the restriction to the conditional fragments becomes
a bit problematic (see below), since then the model
translation is not isomorphic. But for theorem proving
purposes, this seems to be not so harmful, mainly
surjectivity of the model translation is required.
Pro empty carriers:
- The fragment of CASL allowing initial and free models
is more easily described when empty carriers are allowed.
In particular, when empty carriers are forbidden,
then the specification
ELEM =
sorts elem
is no longer part of this fragment. But we need ELEM
as a parameter specification for generic extensions
or architectural specifications. We certainly do not
need the inital model of ELEM. But the fragment of CASL
allowing initial and free models does not contain ELEM.
So singling out this fragment as a sublanguage is
much less useful.
But of course, when empty carriers are forbidden,
one can still single out the conditional fragement of CASL,
and use conditional term rewriting or paramodulation tools
for it.
- The translation of other specification languages (or sublanguages)
that - have only conditional axioms, but
- allow empty carriers,
to CASL becomes more complex when empty carriers are forbidden.
It is sensible that the target of this translation should be the
conditional fragment of CASL (in order to be able to use tools
designed for this fragment). Probably such a translation
from a specification language L to the conditional fragment
of CASL would proceed as follows:
- An L-signature is translated to CASL by adding some unary predicate
for each sort, and axioms which state that operations
preserve this predicate
- An L-axiom is translated trivially
- A CASL-model of a translated signature is mapped to an L-model
by restricting carriers to the predicates (thus, also
empty carriers may be obtained).
Now it seems to be impossible to have a 1-1-representation
of models: The conditional fragment of CASL is not strong
enough to exclude additional junk outside the unary predicates.
But it would be desirable to have an isomorphic representation of
models in order to have a neat representation of the in-the-large
concepts (at least I do not know of any research showing
how this is done for model representations which are not isos,
while for iso model representations this basically is
only the problem of translating the in-the-large concepts).
So from my point of view, the main trade-off is:
where do we want to have the easier, and where the more complex
translations?
In my eyes, a complex translation from CASL to FOL/HOL for
theorem proving purposes is not so harmful as a complex
translation from other specification languages to CASL.
So I am (slightly) in favour of allowing empty carriers.
*** Issue: Institution-independence
p. 44, Points for discussion, 4th item
>Can the treatment of compound identifiers be adjusted to
>permit a fully institution independent treatment of
>structuring constructs?
There is no fully institution independent treatment of
structuring constructs! All what we can do is to design
a notion of "institution-with-syntax" which allows
an "institution-with-syntax"-independent treatment
of *most* of the structuring constructs.
We have to find a way between the following extremes:
a) Compared with institutions, institutions-with-syntax
have few (in extreme: no) additional concepts, but much
of the treatment of structuring concepts remains
institution-with-syntax dependent.
(This is what we have currently.)
b) Much of the treatment of structuring concepts is really
institution-with-syntax independent, but institutions-
with-syntax have to be much like (in extreme: isomorphic
to) the CASL institution.
Two reasonable ways between these extremes are the following:
1) Use Andrzej's and Don's notion of institution-with-syntax,
together with a notion of signature extension (unfortunately,
it does not suffice to take signature inclusions as extensions,
because we really need signature fragments).
Furthermore, the notion of "translation of a signature extension
along a signature morphism" (p. 51 and 71f. of S-6) which yields
the result of an instantiation of a generic specification,
has to be added as a primitive notion.
2) Instead of having the notion of "translation of a signature
extension along a signature morphism" as primitive,
introduce a notion of sort and of profile. Note that
this makes institutions-of-syntax a bit more CASL-like,
but most institutions will have sorts and profiles
(whatever they look like) and signature morphisms
preserving profiles.
Then notion of "translation of a signature
extension along a signature morphism" becomes a derived notion.
Now the consequences for compound ids:
The interaction of compound ids with subsorting has, in
either case, to be encoded into the notion of signature
(otherwise we need an ugly thing like "institution-with-subsorting").
So in section 6, we have some institution-with-syntax dependent
treatment of compound ids. However, this is very local
(just redefine what a signature is).
The instantiation of generics (and, as a consequence, the
interaction of this with compound ids) is institution-with-syntax
dependent for 1) and independent for 2).
Again, in case 1), the institution-with-syntax dependence
can be localized, namely it appears only in the definition
of "translation of a signature extension along a signature morphism".
I will provide formal details on cofi-semantics (but before
doing this, I would like to get some feedback about the
possibilities 1) and 2)!).
Greetings,
Till