Re: [CoFI] Comments on CASL v0.99 DRAFT

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,
 
here are some more comments:
on attributes, institution independence, if-then-else/case,
and empty carriers.

[Many thanks to Till for finding time for this during the Easter
holidays!  --PDM


Attributes
----------
>forall x:List;y,z:NeList . x ++ (y ++ z) = (x ++ y) ++ z
>
>is well-formed, while
>
>forall x,y:List;z:NeList . x ++ (y ++ z) = (x ++ y) ++ z
>
>is not.
>I do not know what OBJ3 does here.
>
>[I've mislaid my copy of "Introducing OBJ3" - could someone
> please check this detail and let me know?  --PDM]
 
Of course I have looked this up in "Introducing OBJ3", but
that manual is not precise enough. It says that retracts are added
in case that the result sort is not included in the argument sorts
- but this is not the case here. And the question is different:
not whether there are retracts, but what are the sorts of
the variables?
I think one has to look at the (behaviour of the) OBJ3 system.

 
Institution independence
------------------------
>[Should there perhaps be something more explicit about
> "institutions with syntax"? --PDM]
 
Perhaps it would be appropriate to add something in Chapter 1, p.2,
where the ingredients of a "basic specification framework" are
explained.
One should add:
* a universe QID of qualified identifiers
* a set of qualified identifiers |\Sigma|\subseteq QID,
  for each signature \Sigma,
Formal details of this notion of "institution with identifiers"
will follow (I think Don and Andrzej's original name
"institution with syntax" is not adequate here, since we have deleted
their component specifying syntax of sentences. All what
remains are (qualified) identifiers.)

 
If-then-else
------------
I support Peter's suggestion of if-then-else.
It does not introduce any complications to the semantics,
as far as I can see. After all, in higher-order logic,
the distinction between formulae and terms is much weaker,
and semantics of higher-order logic in this respect
is no more complicated than semantics of first-order logic.
And Peter's expansion semantics shows that we are very
close to what is already there in CASL.
 
> It is difficult to give a semantics of the case construct. "case" is in
> fact a group of axioms, and we support the use of axioms. The effect of
> case can be achieved by means of annotations around a group of axioms, 
e.g.
> to indicate completeness.
I think that for free types, a case construct should have a rather
straightforward semantics. But are there any need for such a construct?
 

Empty carriers
--------------
Horst Reichel came up with an example specification using empty
carriers. Namely:
 
spec Graph =
sorts nodes, edges
ops   source,target : edges -> nodes
end
 
Now Graph should cover also the special case of discrete graphs,
i.e. no edges. Thus the corresponding carrier is empty.

Bernd and Don have argued that one should represent graphs
as sets, as in
 
spec GraphAsSet =
Sets with set,function,domain,codomain then
type graph ::= g(egdes,nodes:set; source,target:function)
axioms domain(source) = edges
       codomain(source) = nodes
       domain(target) = edges
       codomain(target) = nodes
end
 
This may be useful when one wants to pass a graph as a parameter
to an operation. But consider the case where some software system
is parameterized over some system graph (showing for example
the built-in transformations that are allowed). This system
graph could very well be treated as an algebra, instead as
an element of an algebra, with the benefit that operations
working with the system graph can directly work on its nodes
and egdes, rather than with some set-internalised form, e.g.
 
        apply_trafo : edges * object -> object
 
 
My proposal to include empty carriers is the following:
 
We have two kinds of sorts, normal sorts, and
possibly-empty carrier-sorts. Suggestion for concrete syntax:
 
spec Graph =
sort nodes
sort | {} edges
ops   source,target : edges -> nodes
end

[Till has also suggested "sort with {} ...".  Further suggestions for
concrete syntax are welcome... --PDM]
 
This declares nodes as normal sort, and edges as possibly
empty sort (concrete syntax may be changed, of course).
The semantics is straightforward: collect all sorts into
the signature as usual, use possibly-empty-carrier-semantics
for all sorts, but add an implicit axiom
 
        exists x:s.true
 
for all normal sorts s. (In the present version of CASL,
this implicit axiom is there for *all* sorts, destroying
initial semantics if there are no ground terms.)
 
To avoid all the tricky problems with global (and also
local) variables, they are only allowed for variables of
normal sorts (with the semantics as before). 
Variables of possibly empty sorts can only be introduced
through universal (or existential) quantification. Since
these variables will be rather the exception, the restriction
is not so harsh.

[So after alternating each version between allowing empty sorts and
forbidding them, we may end up with a nice compromise!  --PDM]
 
Greetings,
Till