[r6rs-discuss] [Formal] Equivalence predicate version of memp

[AndrevanTonder]

On Thu, 28 Sep 2006, Carl Eastlund wrote:

> On 9/28/06, Andre van Tonder <andre at het.brown.edu> wrote:
>> 
>> There is in fact another, more compelling, reason for doing
>> just this.  The current specification of various of the list
>> procedures is ambiguous in the presence of call/cc.  This
>> is the subject of a formal comment I just submitted.
>> 
>> Specifying these procedures via implementation would fix
>> these call/cc ambiguities, ambiguities in the prose, and perhaps
>> some other possibly unknown ambiguities (exceptions come to mind).
>> Any concomitant increase in spec length would therefore be well
>> worth it.
>
> There would still need to be prose explaining how an implementation
> can differ from the code in the specification.

One could simply say

  "the map procedure should be operationally equivalent to ..."

where operational equivalence with respect to the reduction semantics is 
defined as in, e.g., J.C. Mitchell - Foundations of programming languages. 
Essentially, this just states that, with the same store, 
the final value obtained from reduction should be the same when MAP is 
inserted into any context (modulo inherently unspecified order of evaluation 
dependencies) and does not require anything about space usage or the order of 
unobservable intermediate calculations.

This would eliminate ambiguities such as the one observable by the 
following expression (example due to Matthias Radestock):

   (let ((result
          (let ()
            (define executed-k #f)
            (define cont #f)
            (define res1 #f)
            (define res2 #f)
            (set! res1 (map (lambda (x)
                              (if (= x 0)
                                  (call/cc (lambda (k) (set! cont k) 0))
                                  0))
                            '(1 0 2)))
            (if (not executed-k)
                (begin (set! executed-k #t)
                       (set! res2 res1)
                       (cont 1)))
            res2)))
     (if (equal? result '(0 0 0))
         (display "Map is call/cc safe, but probably not imperative.")
         (display "Map is not call/cc safe, but probably imperative."))
     (newline))

Andre