Path: utzoo!mnetor!tmsoft!torsqnt!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!elroy.jpl.nasa.gov!usc!wuarchive!mit-eddie!uw-beaver!rice!news
From: matthias@leto.rice.edu (Matthias Felleisen)
Newsgroups: comp.lang.lisp
Subject: Re: In defense of call/cc (and a plug for T)
Summary: call/cc vs coroutines: a semi-formal treatment of equivalence
Keywords: coroutines, continuations, expressiveness
Message-ID: <1991Feb16.215055.6177@rice.edu>
Date: 16 Feb 91 21:50:55 GMT
References: <1991Feb12.233157.20820@elroy.jpl.nasa.gov> <1350035@otter.hpl.hp.com>
Sender: news@rice.edu (News)
Organization: Rice University, Houston
Lines: 166

Here is a semi-formal treatment of the puzzle that was posed to
comp.lang.lisp by Steve Knight.

GIVEN: An Indiana-style definition of coroutines in Scheme, using
call/cc.

  (extend-syntax (COROUTINE RESUME)
    [(COROUTINE x body)
     (letrec ([lcs (lambda (x) body)]
	      [RESUME (lambda (dest val)
			(call/cc (sigma (lcs) (dest val))))])
       (lambda (x) (lcs x)))])

LOOKING FOR: A definition of call/cc in terms of the COROUTINE syntax.

SOLUTION: 

  (define callcc
    (lambda (f)
      (letrec ([c (COROUTINE x (RESUME f c))]) (c13))))

If you are not interested in a semi-formal proof that callcc is really
related to call/cc, skip the rest. The proof informally uses the
extended lambda calculus for Scheme that several co-workers and myself
have developed over the last few years. -- Matthias Felleisen

P.S. A more readable version is contained in public/puzzle.dvi @
titan.rice.edu, which you may obtain via anonymous ftp. 





-------------------------- cut here -----------------------------------

PROOF: The following is a proof in (a variant of) the
Felleisen-Hieb(*) calculus of Scheme.

[1] Replace the use of the extended syntax by its definition. 

(define callcc
  (lambda (f)
    (letrec ([c (letrec ([lcs (lambda (x) (RESUME f c))]
			 [RESUME (lambda (dest val)
					 (call/cc (sigma (lcs)
					    (dest val))))])
			(lambda (x) (lcs x)))])
      (c 13))))

[2] Flatten the letrec definitions.

(define callcc
  (lambda (f)
    (letrec ([c (lambda (x) (lcs x))]
	     [lcs (lambda (x) (RESUME f c))]
	     [RESUME (lambda (dest val)
		       (call/cc (sigma (lcs) (dest val))))])
      (c 13))))
   ; Expand the non-rho use of letrec to see that this is correct.

[3] Dereference c and use a beta-value step to discharge the
resulting beta-value redex.

(define callcc
  (lambda (f)
    (letrec ([c (lambda (x) (lcs x))]
	     [lcs (lambda (x) (RESUME f c))]
	     [RESUME (lambda (dest val)
		       (call/cc (sigma (lcs) (dest val))))])
      (lcs 13))))

[4] Dereference lcs and use a beta-value step to discharge the
resulting beta-value redex. 13 disappears: lucky us :-). 

(define callcc
  (lambda (f)
    (letrec ([c (lambda (x) (lcs x))]
	     [lcs (lambda (x) (RESUME f c))]
	     [RESUME (lambda (dest val)
		       (call/cc (sigma (lcs) (dest val))))])
       (RESUME f c))))

[5] Dereference RESUME and use multi-beta-value redex to discharge
the resulting beta-value redex.

(define callcc
  (lambda (f)
    (letrec ([c (lambda (x) (lcs x))]
	     [lcs (lambda (x) (RESUME f c))]
	     [RESUME (lambda (dest val)
		       (call/cc (sigma (lcs) (dest val))))])
      (call/cc (sigma (lcs) (f c))))))

[6] Expand call/cc such that it takes a lambda-argument: this is one
form of continuation-eta rule.

(define callcc
  (lambda (f)
    (letrec ([c (lambda (x) (lcs x))]
	     [lcs (lambda (x) (RESUME f c))]
	     [RESUME (lambda (dest val)
		       (call/cc (sigma (lcs) (dest val))))])
      (call/cc (lambda (k)
	 ((sigma (lcs) (f c)) k))))))

[7] Swap letrec and (call/cc (lambda k. ***)).

(define callcc
  (lambda (f)
    (call/cc (lambda (k)
	       (letrec ([c (lambda (x) (lcs x))]
			[lcs (lambda (x) (RESUME f c))]
			[RESUME (lambda (dest val)
				  (call/cc (sigma (lcs) (dest val))))])
		 ((sigma (lcs) (f c)) k))))))

[8] Perform the sigma-assignment.

(define callcc
  (lambda (f)
    (call/cc (lambda (k)
	       (letrec ([c (lambda (x) (lcs x))]
			[lcs k]
			[RESUME (lambda (dest val)
				  (call/cc (sigma (lcs) (dest val))))])
		 (f c))))))

[9] Garbage collect RESUME.

(define callcc
  (lambda (f)
    (call/cc (lambda (k)
	       (letrec ([c (lambda (x) (lcs x))] [lcs k])
		 (f c))))))

[10] Dereference c and garbage collect. (Since f is non-assignable it
is in an evaluation context.)

(define callcc
  (lambda (f)
    (call/cc (lambda (k)
	(letrec ([lcs k])
	  (f (lambda (x) (lcs x))))))))

[11] Dereference lcs via "fancy garbage collection". (It is no longer
assignable so we can substitute its uses via (potentially recursive)
values).

(define callcc
  (lambda (f)
    (call/cc (lambda (k) (f (lambda (x) (k x)))))))

[12] "Expand" call/cc lift in empty context.

(define callcc (lambda (f) (call/cc f)))

And this is as close as we can get since call/cc is an assignable
identifier in the global environment, i.e., Replacing the right hand
side with call/cc would not be correct.

In summary this derivation shows that callcc will always have the
same value as call/cc in the global environment.

(*) {Felleisen, M. and R. Hieb}.  The revised report on the syntactic
theories of sequential control and state.  Technical Report 100, Rice
University, June 1989.