CASL and HO

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

Dear friends,

The following is a contribution to the discussion on functions,
constants, partial constants etc.  I will send another message on one
or two further topics later on.

I see that Till has just sent something that overlaps with what is
below but:

1. I don't see how what he has written fits into my (perhaps flawed!)
   understanding of how HO is normally treated.
2. I wrote the following before I saw his message.

So I am just sending this without commenting on Till's message in the
hope that it won't confuse matters too much.

[Till: perhaps you could send a quick comment on this message?  --PDM]

Another caveat is that I wasn't in Paris so I don't know why what was
in 0.95 was viewed as inadequate.  Apologies if there was something
said there that makes the following pointless.

[Bernd proposed changes - along the lines of those that I implemented
in v0.96, but those were probably not quite what he wanted - in a
message sent to cofi-language on 18 April.  --PDM]

Regards, Don

----------------------------------------------------------------

Here's a grammar for something that I think covers all that we would
want to permit in HO CASL (except polymorphism) including even some
things that we probably don't want such as predicates over predicates.

  b ::= bool | int | ...
  t ::= b | t1*...*tn | t -> t' | t -p-> t' | pred(t)
  decl ::= id:t

(Notation: -> is total function space, -p-> is partial function space,
pred(t) is the space of predicates over t.  b stands for "base type".)

FO is the case where at least the following restrictions are imposed:
1. In t->t', t-p->t' and pred(t):
   neither t nor t' may contain ->, -p->, or pred
   t' may not contain * (i.e. t' must be a base type)
2. In t1*...*tn:
   t1,...,tn may not contain ->, -p->, pred or * (i.e. they must be
   base types)
(The restrictions on where * may appear are not essential; those on
where arrows and pred may appear are essential.)

Now, given this context, there is a question:

QUESTION: How do the types .->b and .-p->b relate to each other and to
the type b, where "." is the 0-tuple of types?

There are various answers.  One is the following:

ANSWER: In a declaration id:t, t is required to contain either -> or
-p-> or pred, so id:b doesn't arise and ->b is different from -p->b.
This is the choice taken in 0.95.  It seems perfectly consistent to
me; in particular, I see no conflict with HO.

There are various alternatives, for example one can allow all three of
.->b, .-p->b and b and distinguish them.  This is what ML does, except
that ML does not contain both -> and -p->.

NOW: I am at a complete loss to see how what is in 0.96 fits into this
and what problem there is with 0.95 that it solves.

[The point was mainly to reorganize the first-order CASL AS grammar so
that the extension to HO would be simpler than with v0.95.  The effect
on the actual language was minimal.  The question being addressed was
how best to specify a simple (context-free) grammar for first order
abstract syntax, with a simple extension to higher-order.  --PDM]

FURTHERMORE: I can see the sense in having partial constants if they
arise as a degenerate case of something that is there already, but
certainly not if they have to be added in as a special case!  Can
anybody point to even one example of a specification where the use of
partial constants was important?  I know that there have been
frameworks where one is required to spell out definedness of
constants, but I never imagined that this was ever regarded as a
useful feature.

[I basically agree.  But the argument in the last sentence above is
beside the point: we are agreed that CASL should provide declarations
of total constants, the only question left is whether to allow also
partial constants.  --PDM]

FINALLY: Requiring the treatment of constants versus parameterless
functions at the level of terms to be the same as at the levels of
generic specs and parametrised units in architectural specs seems
quite unnecessary.  (Emerson: "A foolish consistency is the hobgoblin
of little minds."  As my students and collaborators will tell you,
this makes my mind very small indeed, but even I can live with this
non-uniformity!)  Or is somebody going to suggest that we need partial
functions at those levels too?  And what about taking linear
visibility at the basic spec level because we have it at the
architectural spec level?

[At various levels, we have both constants and functions.  As Andrzej
pointed out in his recent comments on v0.96, the grammar for the AS is
likely to be confusing if one uses a different style at each level.
V0.95 was quite good in this respect; the changes that Bernd proposed
for facilitating extension to HO disturbed this uniformity in v0.96.
I'm now planning to revert the syntax for DECL, TYPE, etc., to more
like what we had in v0.95 - but taking into account the suggestions by
Maura and Till in their recent messages.  This may even simplify the
job of updating the formal semantics to v0.97...  --PDM]