[CoFI] if then else (again?)

[bkb@informatik.uni-bremen.de]

[BKB: this comment of mine was submitted to Peter some time ago in the
last rush for the present version; however, I submitted it by fax, thus
it has not been in the files.
It is now probably too late; comment only, if you are really unsatisfied
with the present proposal "t1 when b else t2".]

Dear Peter, 
I was perhaps a bit rushed when approving the if then else. I do not
mind it, but I would like to draw attention to an old proposal of mine
inspired by functional languages which I find much better; the two could
coexist. I suggest to make the status of whatever if proposal similar to
that of, say, morphisms, i.e. last minute. Many people have not have
time to REACT to this, even if they did not want to make own comments.
The problem with your if then else may be nesting, at least for the
transformation to normal formulae.  regards and in a rush and in
vacation  
Bernd
--------------------------

Conditionals

The idea is to use cascaded conditional equations only, as an extension
of the "if" construct; also in operation definitions. This is simpler as
a general "if then else" construct, but sufficiently powerful (?), cf.
functional languages such as Haskell. The notation is also quite close
to conventional mathematical notation using a large brace.

max(n, m)       = n if n >= m
                        = m if n <= m

fib n
        = 0                              if n = 0
        = 1                              if n = 1
        = fib(n-1)+fib(n-2)      if n > 1

The semantics is given by repeated insertion of the left-hand-side, and
conjunction. The "otherwise" clause is a conjunction of the negations of
the preceding conditions. It always comes last and is optional.

Similarly, the construct can be used for operation definitions:

fac: (n: Nat) -> Nat    = 1                     if n = 0
                                                = n*fac(n-1)   
otherwise

Syntax
(this syntax would have to be adapted to the present CASL syntax)
 
CondEquation    ::=     Term CondRhs+ CatchAllOption .        
--  
CondRhs                 ::=     EqOp Term IF Formula .
CatchAllOption  ::=     EqOp Term OTHERWISE     |       empty.
--
(similarly CondRhs on the right hand side of an OP-DEFN)

If there is an ambiguity (lookahead) problem w.r.t. the usual "if", the
use of CondEquation could be restricted to the outermost level of
formulae, i.e. not in nested formulae after "if". 

--------------------------- end of proposal
-- 
________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner    courier mail only:
FB3 Mathematik und Informatik      MZH 8071, FB3
Universitaet Bremen                Universitaet Bremen
Postfach 330 440                   Bibliothekstr. 1
D-28334 Bremen                     D-28359 Bremen

Telefon: (+49) 421-218-3660        telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE       privat:  (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb
http://www.uni-bremen.de/~sppraum