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

["Don Sannella" <dts@dcs.ed.ac.uk>]

[The deadline for comments has just been extended for a few hours, at
 Bernd's request.  --PDM]

Sorry, it's empty carriers time again :-(

I didn't want to send any more mail on this topic but I can't let the
last line of Peter's comment on my message pass without a rejoinder.

[OK - but this is definitely the last message on THIS topic!  I trust
 that Bernd has been following the discussion, and will let us know
 his conclusion concerning the CASL treatment of empty sorts.  --PDM] 

I wrote:
> I think I remember Peter arguing at some point in the past that we
> couldn't use lambda notation because there might be people in the
> intended audience to whom it would be unfamiliar.  This audience needs
> empty carriers? 
> 
> [Lambda notation has crept in anyway, in connection with arch specs.
>  But right: my personal view is that it'd be nice if CASL specs could
>  be understood by programmers who have never even heard of lambda
>  notation.  And since you ask: I personally think that this same
>  audience may indeed need specs of graphs, and that they may feel a bit
>  disappointed with CASL if discrete graphs can't be specified.  --PDM]

Discrete graphs can of course perfectly well be specified, either
using sets as Till says in a previous message, or along the following
lines (apologies for use of non-CASL syntax).  This particular spec is
for directed graphs with at most one edge from one node to another.

  sort node
  type edge = mkedge(source:node,target:node)
  sort graph
  ops empty : graph
      addnode : node * graph -> graph
      addedge : edge * graph -> graph
      ... etc. etc. ...
  pred path : node * node * graph
  axioms ...

So what Peter means, presumably, is that some PARTICULAR WAY of
specifying discrete graphs can't be expressed in CASL.  Even this is
false, I think, if you are willing to put up with a bit of clumsiness,
by simply adding constants nonedge:edge, nonnode:node and relativizing
quantifiers to ignore them.  So in Peter's comment above, replace
  "they may feel a bit disappointed with CASL if discrete graphs can't
  be specified"
by
  "they may feel a bit disappointed with CASL if one particular
  specification of discrete graphs can't be expressed without a bit of
  hackery"
and then think whether the argument is quite so convincing.

There are lots of other ways of specifying graphs that can't be
expressed in CASL, for example anything at all involving state and/or
objects.  Yes, I know that there will be extensions to cope with this.
The point is that there is a decision to be made about what goes in
CASL and what doesn't, and I think simplicity and familiarity are
important factors.

Finally, if we really really need empty sorts then let's just allow
all sorts to be empty and deal with the well-known problems that this
causes.

Regards, Don