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

[Christine.Choppy@irin.univ-nantes.fr (Christine Choppy)]

[This is presumably the final comment on the draft v0.99 CASL Summary
 - although those in other time zones may interpret "12 noon" locally,
 and perhaps still manage to beat the deadline...  --PDM]

Peter D. Mosses proposed:

>   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])

[N.B. This expansion avoids moving F through any quantifiers. --PDM]

>   ...
> 
> 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)
>  

I agree that this construct would shorten the axioms.
I really prefer the

      T1 when F else T2

syntax so that it would be obvious that this should in no case
be confused with the "good old" if-then-else function:
here we are talking of a formula abbreviation.

As before, nested if-then-else may really blur the picture,
there is always this trade-off between a concise notation
and a TOO concise notation (that yields to unreadable things).

[Although the semantics is defined through an expansion, one may
 mentally interpret the conditional in the normal way: if F holds, the
 value is the same as that of T1, otherwise T2.  I don't see the
 problem with readability of nested conditionals in T1 and T2.  --PDM]

Christine.