[with corrections by Al Petrofsky, 15 June 2002]

Factoid.  According to the denotational semantics of Scheme
as published in the IEEE/ANSI and R3RS/R4RS/R5RS documents,
when augmented with the obvious definitions of K[[0]] and
K[[1]], in any environment r and store s such that

    s (r call-with-current-continuation) [1]
        = (<a_cwcc, cwcc> from F into E)

the expression

  (call-with-current-continuation (lambda (c) (0 (c 1))))

either returns 1 or runs out of memory.

Proof.  We assume that

    K [[ 0 ]] = 0 from R into E
    K [[ 1 ]] = 1 from R into E

    permute <x, y> = <x, y>
    unpermute <x, y> = <x, y>

There is one other possibility for permute and unpermute, but
the calculation for that possibility is essentially the same,
so it is left as an exercise for the reader.

The calculation below also assumes that the expression is
evaluated in an environment and store that map the free
variable call-with-current-continuation to its usual value,
and that the store s has at least 3 free locations.  More
precisely, we assume that

    s (r call-with-current-continuation) [1]
        = (<a_cwcc, cwcc> from F into E)
and
    new s isIn L
and
    new (update (new s | L) unspecified s) isIn L
and
    new (update (new (update (new s | L) unspecified s) | L)
                unspecified
                (update (new s | L) unspecified s)) isIn L

If one of the last three assumptions is not true, then the
calculations below show that evaluation of the expression
will run out of memory and pass control to wrong, which is
an unspecified continuation.

Notational conventions:
 x ? y : z           conditional expression, same as (x -> y, z) in R5RS
 isIn                member of summand, same as set membership epsilon in R5RS
 from F into E       injection into sum, same as "in E" in R5RS
 E                   sometimes means scriptE
 \                   means lambda
 +                   sometimes means concatenation of sequences
 s[i]                means the ith element (1-origin) of the sequence s
 s!i                 means the sequence s without its first i elements

--------

E [[ (call-with-current-continuation (lambda (c) (0 (c 1)))) ]]

= \ r k . E* (permute ( <call-with-current-continuation,
                         (lambda (c) (0 (c 1)))> ))
             r
             (\ e* . (( \ e* . applicate (e*[1]) (e*!1) k)
                      (unpermute e*)))

= \ r k . E* <call-with-current-continuation,
              (lambda (c) (0 (c 1)))>
             r
             (\ e* . applicate (e*[1]) (e*!1) k)

= \ r k . E [[ call-with-current-continuation ]]
            r
            single (\ e0 . E* [[ (lambda (c) (0 (c 1))) ]]
                           r
                           (\ args . (\ e* . applicate (e*[1]) (e*!1) k)
                                     ( <e0> + args )))

= \ r k . E [[ call-with-current-continuation ]]
            r
            single (\ e0 . E [[ (lambda (c) (0 (c 1))) ]]
                             r
                             (single (\ e1 . E* [[ ]]
                                                r
                                                (\ nada . k2 ( e1 + nada )))))

    where k2 = (\ args . (\ e* . applicate (e*[1]) (e*!1) k)
                         ( <e0> + args ))
             = (\ args . applicate e0 args k)

= \ r k . E [[ call-with-current-continuation ]]
            r
            single (\ e0 . E [[ (lambda (c) (0 (c 1))) ]]
                             r
                             (single (\ e1 . (\ nada . k2 ( e1 + nada )) <> )))

= \ r k . E [[ call-with-current-continuation ]]
            r
            single (\ e0 . E [[ (lambda (c) (0 (c 1))) ]]
                             r
                             (single (\ e1 . k2 < e1 >)))

= \ r k . E [[ call-with-current-continuation ]]
            r
            single (\ e0 . (\ s . new s isIn L ?
                                  send (<new s | L, f> from F into E)
                                       (single (\ e1 . k2 < e1 >))
                                       (update (new s | L) unspecified s) :
                                  wrong "out of memory" s))

    where f = \ e* k' . #e* = 1 ?
                        tievals (\ a* . (\ r' . C [[ ]] r'
                                                (E [[ (0 (c 1)) ]] r' k'))
                                        (extends r <c> a*))
                                e* :
                        wrong "wrong number of arguments"

= \ r k . hold (lookup r call-with-current-continuation)
               (single (\ e . e = undefined ?
                              wrong "undefined variable" : 
                              send e k3))

    where k3 =
            single (\ e0 . (\ s . new s isIn L ?
                                  send (<new s | L, f> from F into E)
                                       (single (\ e1 . k2 < e1 >))
                                       (update (new s | L) unspecified s) :
                                  wrong "out of memory" s))

--------

That is about as far as we can take it without using the
environment and store in which the expression is evaluated.

--------

E [[ (call-with-current-continuation (lambda (c) (0 (c 1)))) ]] r k s

= hold (lookup r call-with-current-continuation)
       (single (\ e . e = undefined ?
                      wrong "undefined variable" : 
                      send e k3))
       s

= send (s (r call-with-current-continuation) [1])
       (single (\ e . e = undefined ?
                      wrong "undefined variable" : 
                      send e k3))
       s

= send (<a_cwcc, cwcc> from F into E)
       (single (\ e . e = undefined ?
                      wrong "undefined variable" : 
                      send e k3))
       s

= (single (\ e . e = undefined ?
                 wrong "undefined variable" : 
                 send e k3))
  < (<a_cwcc, cwcc> from F into E) >
  s

= (\ e* . # (e*) = 1 ?
          (\ e . e = undefined ?
                 wrong "undefined variable" :
                 send e k3) (e*[1]) :
          wrong "wrong number of return values")
  < (<a_cwcc, cwcc> from F into E) >
  s

= send (<a_cwcc, cwcc> from F into E) k3 s

= k3 < (<a_cwcc, cwcc> from F into E) > s

= single (\ e0 . (\ s . new s isIn L ?
                        send (<new s | L, f> from F into E)
                             (single (\ e1 . k2 < e1 >))
                             (update (new s | L) unspecified s) :
                        wrong "out of memory" s))
  < (<a_cwcc, cwcc> from F into E) >
  s

= new s isIn L ?
  send (<new s | L, f> from F into E)
       (single (\ e1 . (\ args . applicate (<a_cwcc, cwcc> from F into E)
                                           args k)
                       < e1 >))
       (update (new s | L) unspecified s) :
  wrong "out of memory" s))

= send (<new s | L, f> from F into E)
       (single (\ e1 . applicate (<a_cwcc, cwcc> from F into E) <e1> k))
       (update (new s | L) unspecified s)

= (single (\ e1 . applicate (<a_cwcc, cwcc> from F into E) <e1> k))
  <(<new s | L, f> from F into E)>
  (update (new s | L) unspecified s)

= applicate (<a_cwcc, cwcc> from F into E) <<new s | L, f> from F into E>
  k
  (update (new s | L) unspecified s)

= cwcc
  <<new s | L, f> from F into E>
  k
  (update (new s | L) unspecified s)

= onearg (\ e k . e isIn F ?
                  (\ s1 . new s1 isIn L ?
                          applicate e
                                    <<new s1 | L, \ e* k' . k e*>
                                     from F into E>
                                    k
                                    (update (new s1 | L) unspecified s1) :
                          wrong "out of memory" s1) :
                  wrong "Bad procedure")
  <<new s | L, f> from F into E>
  k
  (update (new s | L) unspecified s)

= (<<new s | L, f> from F into E> isIn F ?
   (\ s1 . new s1 isIn L ?
           applicate <<new s | L, f> from F into E>
                     <<new s1 | L, \ e* k' . k e*>
                      from F into E>
                     k
                     (update (new s1 | L) unspecified s1) :
           wrong "out of memory" s1) :
   wrong "bad procedure argument")
  (update (new s | L) unspecified s)

= (\ s1 . new s1 isIn L ?
          applicate <<new s | L, f> from F into E>
                    <<new s1 | L, \ e* k' . k e*>
                     from F into E>
                    k
                    (update (new s1 | L) unspecified s1) :
          wrong "out of memory" s1)
  (update (new s | L) unspecified s)

= new (update (new s | L) unspecified s) isIn L ?
  applicate <<new s | L, f> from F into E>
            <<new (update (new s | L) unspecified s) | L, \ e* k' . k e*>
             from F into E>
            k
            (update (new (update (new s | L) unspecified s) | L)
                    unspecified
                    (update (new s | L) unspecified s)) :
  wrong "out of memory" (update (new s | L) unspecified s))
  
= applicate <<a1, f> from F into E>
            <<a2, \ e* k' . k e*> from F into E>
            k
            s2
  
    where a1 = (new s | L)
          s1 = (update a1 unspecified s)
          a2 = (new s1 | L)
          s2 = (update a2 unspecified s1)

= applicate <<a1, f> from F into E>
            <<a2, \ e* k' . k e*> from F into E>
            k
            s2
  
= f <<a2, \ e* k' . k e*> from F into E>
    k
    s2

= (\ e* k' . #e* = 1 ?
             tievals (\ a* . (\ r' . C [[ ]] r'
                                     (E [[ (0 (c 1)) ]] r' k'))
                             (extends r <c> a*))
                     e* :
             wrong "wrong number of arguments")
  <<a2, \ e* k' . k e*> from F into E>
  k
  s2

= (#<<a2, \ e* k' . k e*> from F into E> = 1 ?
   tievals (\ a* . (\ r' . C [[ ]] r'
                           (E [[ (0 (c 1)) ]] r' k))
                   (extends r <c> a*))
           <<a2, \ e* k' . k e*> from F into E> :
   wrong "wrong number of arguments")
  s2

= tievals (\ a* . (\ r' . C [[ ]] r'
                          (E [[ (0 (c 1)) ]] r' k))
                  (extends r <c> a*))
          <<a2, \ e* k' . k e*> from F into E>
          s2

= (\ phi e* s . #e* = 0 ?
                phi <> s :
                (new s isIn L ?
                 tievals (\ a* . phi (< new s | L > + a*))
                         (e* ! 1)
                         (update (new s | L) (e*[1]) s) :
                 wrong "out of memory" s))
  (\ a* . (\ r' . C [[ ]] r'
                  (E [[ (0 (c 1)) ]] r' k))
          (extends r <c> a*))
  <<a2, \ e* k' . k e*> from F into E>
  s2

= #<<a2, \ e* k' . k e*> from F into E> = 0 ?
  phi <> s :
  (new s2 isIn L ?
   tievals (\ a* . phi (< a3 > + a*))
           (<<a2, \ e* k' . k e*> from F into E> ! 1)
           s3 :
   wrong "out of memory" s2)

    where a3 = new s2 | L
          s3 = update a3 (<a2, \ e* k' . k e*> from F into E) s2
          phi = (\ a* . (\ r' . C [[ ]] r'
                                (E [[ (0 (c 1)) ]] r' k))
                        (extends r <c> a*))

= new s2 isIn L ?
  tievals (\ a* . phi (< a3 > + a*))
          (<<a2, \ e* k' . k e*> from F into E> ! 1)
          s3 :
  wrong "out of memory" s2

= tievals (\ a* . phi (< a3 > + a*))
          <>
          s3

= (\ a* . phi (< a3 > + a*))
  <>
  s3

= phi <a3> s3

= (\ r' . C [[ ]] r'
          (E [[ (0 (c 1)) ]] r' k))
  (extends r <c> <a3>)
  s3

= E [[ (0 (c 1)) ]] r2 k s3

    where r2 = (extends r <c> <a3>)

= E* (permute <0, (c 1)>)
     r2
     (\ e* . ((\ e* . applicate (e*[1]) (e*!1) k)
              (unpermute e*)))
     s3

= E* [[ 0 (c 1) ]]
     r2
     (\ e* . applicate (e*[1]) (e*!1) k)
     s3

= E [[ 0 ]]
    r2
    (single (\ z . E* [[ (c 1) ]] r2 (\ e* . k (<z> + e*))))
    s3

= send K [[ 0 ]]
    (single (\ z . E* [[ (c 1) ]] r2 (\ e* . k (<z> + e*))))
    s3

= E* [[ (c 1) ]] r2 (\ e* . k (<0 from R into E> + e*)))) s3

= E [[ (c 1) ]]
  r2
  (single (\ e . E* [[ ]]
                    r2
                    (\ nada . (\ e* . k (<0 from R into E> + e*))
                              (<e> + nada))))
  s3

= E [[ (c 1) ]]
  r2
  (single (\ e . k (<0 from R into E> + <e>)))
  s3

= E* (permute <c, 1>)
     r2
     (\ e* . ((\ e* . applicate (e*[1]) (e*!1) k4)
              (unpermute e*)))
     s3

    where k4 = (single (\ e . k (<0 from R into E> + <e>)))

= E* [[ c, 1 ]]
     r2
     (\ e* . applicate (e*[1]) (e*!1) k4)
     s3

= E [[ c ]]
    r2
    (single (\ e0 . E* [[ 1 ]] r2 (\ e* . k5 (<e0> + e*))))
    s3

    where k5 = (\ e* . applicate (e*[1]) (e*!1) k4)

= hold (lookup r2 c)
       (single (\ e . e = undefined ?
                      wrong "undefined variable" :
                      send e (single (\ e0 . E* [[ 1 ]]
                                             r2 (\ e* . k5 (<e0> + e*))))))
       s3

= hold (lookup (extends r <c> <a3>) c)
       (single (\ e . e = undefined ?
                      wrong "undefined variable" :
                      send e (single (\ e0 . E* [[ 1 ]]
                                             r2 (\ e* . k5 (<e0> + e*))))))
       s3

= hold a3
       (single (\ e . e = undefined ?
                      wrong "undefined variable" :
                      send e (single (\ e0 . E* [[ 1 ]]
                                             r2 (\ e* . k5 (<e0> + e*))))))
       (update a3 (<a2, \ e* k' . k e*> from F into E) s2)

= send (<a2, \ e* k' . k e*> from F into E)
       (single (\ e . e = undefined ?
                      wrong "undefined variable" :
                      send e (single (\ e0 . E* [[ 1 ]]
                                             r2 (\ e* . k5 (<e0> + e*))))))
       s3

= send (<a2, \ e* k' . k e*> from F into E)
       (single (\ e0 . E* [[ 1 ]]
                          r2 (\ e* . k5 (<e0> + e*))))
       s3

= E* [[ 1 ]]
     r2
     (\ e* . k5 (<(<a2, \ e* k' . k e*> from F into E)> + e*))))
     s3

= E [[ 1 ]]
    r2
    (single (\ e1 . E* [[ ]]
                       r2
                       (\ nada . (\ e* . k5 (<(<a2, \ e* k' . k e*>
                                             from F into E)> + e*))
                                 (<e1> + nada))))
    s3

= E [[ 1 ]]
    r2
    (single (\ e1 . (\ e* . k5 (<(<a2, \ e* k' . k e*>
                                             from F into E)> + e*))
                    <e1>))
    s3

= E [[ 1 ]]
    r2
    (single (\ e1 . k5 (<(<a2, \ e* k' . k e*> from F into E)> + <e1>)))
    s3

= send (K [[ 1 ]])
       (single (\ e1 . k5 (<(<a2, \ e* k' . k e*> from F into E)> + <e1>)))
       s3

= k5 (<(<a2, \ e* k' . k e*> from F into E)> + <1 from R into E>)))
     s3

= (\ e* . applicate (e*[1]) (e*!1) k4)
  <(<a2, \ e* k' . k e*> from F into E), (1 from R into E)>
  s3

= applicate (<a2, \ e* k' . k e*> from F into E)
            <1 from R into E>
            k4
            s3

= (\ e* k' . k e*)
  <1 from R into E>
  k4
  s3

= k <1 from R into E> s3

This says that the value 1 is passed to the expression's
continuation, which is to say that the expression returns 1.

QED.