Order of evaluation (again)

[Christian Queinnec <Christian.Queinnec@inria.fr>]

We don't want to start again a religious war on the order of
evaluation but we think that if R5RS is to specify that the evaluation
order is unspecified then this can be better defined if we change the
Answer domain of the denotation into Answer* (sequences of Answers).
The denotation will then associate to a program the list of results it
can yield and not just one result. We propose hereafter to get rid of
the permute/unpermute trick that do not highlight some fine details on
the semantics of application.  For instance, it will be clear that the
following program may loop or stop, the semantics will not impose that
it loops forever nor it imposes that it always stops:
 
(define (F)
  (define (G)
    (call/cc (lambda (k) (+ (k 1) (k 2)))) )
  (if (= (G) (G))
      (F)
      'stop ) )

The price to pay is to deal with Answer* and not Answer (independently
of what is exactly Answer). The denotation of the application is, in
natural language, the following. Given the application (e0 e1 ... en),
choose one term, say ei0, its evaluation yields vi0, THEN choose
another ei1 yielding vi1 ... THEN choose(!) the last term ein yielding
vin, reorder all values (vi0 .. vin) into (v0 .. vn) and apply v0 on
the others.  Observe that the choice of the evaluation order any
remaining terms belongs to the continuation and is left unspecified
until needed. For instance and in the following program, if nothing
was displayed before the continuation k was reified then to invoke k
may print 1 then 2 or 2 then 1. This order is unspecified (although
most compilers chose it already). And if k is invoked again the order
might change.

        (f (call/cc (lambda (k) ...))
           (display 1)
           (display 2) )

The denotation of the application builds all possible paths then
chooses, in an implementation dependent way, one of these paths. This
is more functional and precise than the permute/unpermute trick.
A toy implementation follows to show that it is not so big a denotation.

;;; Forall cuts the list L in all possible ways and applies F on the
;;; three obtained parts. All results are gathered.
;;; forall : ((a list * a * a list) -> b list) * (a list) -> b list
(define (forall f l)
  ;; (assume (pair? l))
  (let loop ((before '())
             (e (car l))
             (after (cdr l)) )
    (append (f before e after)
            (if (pair? after)
                (loop (append before (list e))
                      (car after)
                      (cdr after) ) 
                '() ) ) ) )

;;; Invoke Q on V* cut into two parts, the first N items and the rest.
(define (cut n v* q)
  (let accumulate ((left '())
                   (n n)
                   (right v*) )
    (if (> n 0)
        (accumulate (cons (car right) left)
                    (- n 1)
                    (cdr right) )
        (q (reverse left) right) ) ) )

;;; The denotation of an application. E+ represents all the terms of an
;;; application. As usual R is the lexical environment, K the continuation
;;; and S the store.
(define (meaning-application e+)
  (lambda (r k s)
    ((possible-paths (map meaning e+))
     r 
     (lambda (v* s)
       ((car v*) (cdr v*) k s) )
     s ) ) )

;;; Denotation of a whole program
(define (whole-program-meaning e)
  (define (oneof answer*)
    "implementation dependent" )
  (oneof (meaning e)) )

;;; Takes a list of denotations, builds all possible ways to interleave 
;;; them and returns the list of all possible answers.
;;; possible-path : meaning list -> env * cont * store -> Answer list
(define (possible-paths m+)
  (lambda (r k s)
    (if (pair? (cdr m+))
        (forall (lambda (<m m m>)
                  (m r
                     (lambda (v ss)
                       ((possible-paths (append <m m>))
                        r 
                        (lambda (v* sss)
                          (cut (length <m)
                               v* 
                               (lambda (<v v>)
                                 (k (append <v (list v) v>) sss) ) ) )
                        ss ) )
                     s ) )
                m+ )
        ((car m+) r 
                  (lambda (v ss) (k (list v) ss))
                  s ) ) ) )

Any comments ?
        
        Sophie Anglade & Christian Queinnec.