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

[pdmosses@brics.dk]

[I'm currently trying to write a paper on the relationship between
CASL and CafeOBJ.  The deadline is this Saturday...  If anyone would
have time and interest to look through a draft tomorrow (Friday)
afternoon, please let me know!  Familiarity with CafeOBJ is NOT
essential.  --PDM] 

I wrote: 

> [The deadline for comments is hereby extended by one week, to:
> 
>   12 noon on WEDNESDAY 15 APRIL, 1998
> 
>  I'd originally hoped that the minutes of the Language Design meeting,
>  summarizing the discussions and proposals from Lisbon, would have been
>  sent to this list before the original deadline, but this has not
>  happened.  Moreover, many of us have just started the Easter holidays
>  - perhaps also with time to take one last look through the CASL design
>  and formulate any "last wishes" for (minor) improvements?  

When I wrote that this morning, I was definitely NOT intending to take
advantage of the suggestion myself!  However (and with many apologies
for the lateness):

> From: Christine.Choppy@lri.fr
> Date: Mon, 15 Jul 1996 15:33:04 +0200
> ...
>           Minutes of the CFI Language Group meeting, Munich, July, 1996
>           =============================================================

Although the minutes from this Munich meeting were sent only to the
participants and not to the Language Design mailing list, the
conclusions were all embodied in the subsequent version of the
Language Summary, and many of the arguments that supported them were
later incorporated in the Language Rationale.  But the basis for the
following decision now appears to me to be rather too weak:

> - if-then-else / cases:
> -----------------------
> are not features of the language. "if boolean-term then t1 else t2" is
> excluded because we do not have booleans built into the common language.
> "if formula then t1 else t2" is excluded because it would mean to allow
> formulae within terms, which would complicate the abstract syntax of the
> language (formulae occur only in the axioms).  In any case one can
> express "t = ...if formula then t1 else t2..." by conditional axioms.
> One might consider if-then-else as a special case of the "case" construct.
> 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.

The (only) point that I find really difficult to justify is this: 

> "if formula then t1 else t2" is excluded because it would mean to allow
> formulae within terms, which would complicate the abstract syntax of the
> language (formulae occur only in the axioms). 

It seems to me now that the complication of the abstract (and
concrete) syntax given by adding such a construct would actually be
very slight.  Moreover, the interpretation of this term is clear
enough, and the appearance of a formula inside a term wouldn't give
any significant complication in the formal semantics, it seems.

Of course, the weakness of part of the rationale cannot by itself
motivate adding a construct to the language at this late stage.
Several participants in the Language Design task group have, however,
previously expressed their dissatisfaction with the omission of an
if-then-else construct. (In fact they might like to have a cases
construct too, but that still seems to be semantically much more
problematic.  Please review the arguments there too!)

>From a methodological point of view, the usefulness of the (admittedly
minor) abbreviation obtainable by use of if-then-else is particularly
evident from some CafeOBJ specifications of an ATM (cash dispenser),
which have numerous axioms of the following form:

  account(U, add(U',N,A)) = add(N,init-account(U)) if U==U' .
  account(U, add(U',N,A)) = account(U,A) if U=/=U' .

CafeOBJ has only total operations, and the "if" construct takes a
formula and a Bool-valued term.  In CASL we would write analogously:

  account(U, add(U',N,A)) = add(N,init-account(U)) if U=U';
  account(U, add(U',N,A)) = account(U,A) if not U=U'

(perhaps using existential equality in the presence of partiality).

Using if-then-else, one could write instead:

  account(U, add(U',N,A)) = 
    if U=U' then add(N,init-account(U)) else account(U,A)

thus avoiding the repetition of the term `account(U, add(U',N,A))'
and of the condition (U=U').

>From a tools point of view, the if-then-else formulation might not be
quite so convenient as the original conditional equations - but it is
rather straightforward to expand out the if-then-else, when needed.

The addition to the CASL Summary might be as follows:

  ...

  Conditional Terms

  ! TERM        ::=  ... | CONDITIONAL
  ! CONDITIONAL ::= conditional FORMULA TERM TERM

  A conditional term is written:

      if F then T1 else T2

  It is well-sorted for a type when both T1 and T2 are well-sorted for
  that type and F is a well-formed formula.  The enclosing atomic
  formula `A[if F then T1 else T2]' then expands to:

      (F => A[T1]) /\ (not F => A[T2])

  Different occurrences are expanded from left to right (although the
  order of expansion does not affect the semantics).

  ...

An alternative concrete syntax might be considered:

      T1 when F else T2

E.g.:

  account(U, add(U',N,A)) = 
    add(N,init-account(U)) when U=U' else account(U,A)

This would avoid some parsing problems that might arise due to a
double role for the keyword "if".  Note however that 

      T1 when F1 else T2 when F2 else T3 

should be implicitly grouped to the right:

      T1 when F1 else (T2 when F2 else T3)
 
Finally, let me note that almost all the previous messages and notes
on this topic addressed the issue of having if-then-else as an
operation on a built-in Bool sort (the exception was from Genova).
I'm worried that we perhaps ended up throwing the baby conditional out
with the built-in Bool bath-water!
 
Normally, I'd consult (at least) with the coordinator of the Langauge
Design before submitting any proposal that challenges a decision made
at the Munich meeting.  But I'm afraid that he's away from his e-mail
until after Easter.  Hence this rather hasty message, which has NOT
yet been checked - let alone supported - by any other participants of
the Language Design task group.  [And the moderator of this mailing
list always has difficulty with suppressing his own messages! --PDM]

Best regards

Peter
_________________________________________________________________
=========   Peter D. MOSSES              Associate Professor, PhD
==== ====   BRICS                        mailto:pdmosses@brics.dk
=========   Dept. of Computer Science    == pdmosses@daimi.aau.dk
==== ====   University of Aarhus         http://www.brics.dk/~pdm
==== ====   Ny Munkegade, bldg. 540      Telephone: +45 8942 3364 
==== ====   DK-8000 Aarhus C, Denmark    Telefax:   +45 8942 3255