[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: rrrs-authors@mc.lcs.mit.edu*Subject*: Order of evaluation (again)*From*: Christian Queinnec <Christian.Queinnec@inria.fr>*Date*: Mon, 10 May 93 15:25:06 +0200*Reply-To*: 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.

- Prev by Date:
**Topes - no substitution model** - Next by Date:
**DYNAMIC-WIND vs. multi-processing** - Prev by thread:
**Topes - no substitution model** - Next by thread:
**DYNAMIC-WIND vs. multi-processing** - Index(es):