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

From: AndrevanTonder <andre>
Date: Thu Sep 28 19:29:38 2006

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
Received on Thu Sep 28 2006 - 19:27:02 UTC