Can the function argument to `call/cc` equivalently either invoke the continuation or return without invoking the continuation?

Question

The Scheme Programming Language says

Scheme allows the continuation of any expression to be captured with the procedure call/cc. call/cc must be passed a procedure p of one argument. call/cc constructs a concrete representation of the current continuation and passes it to p. The continuation itself is represented by a procedure k. Each time k is applied to a value, it returns the value to the continuation of the call/cc application. This value becomes, in essence, the value of the application of call/cc. If p returns without invoking k, the value returned by the procedure becomes the value of the application of call/cc.

Are the two following ways of defining p equivalent, as far as being called by call/cc is concerned:

• p returns without invoking k,
• p calls k with its otherwise return value?

I am not sure how call/cc is defined. Does call/cc ever directly call the continuation k, besides indirectly via p calling k?

Is it perfectly fine that both call/cc and p don't invoke continuation k?

Answer 1

Yes, (call/cc (lambda (k) 1)) <=> (call/cc (lambda (k) (k 1))). You can prove this by using the continuation passing style transform.

The key part is the CPS form of call/cc is (lambda (k) (lambda (f) ((f k) k))). And the CPS forms of the two functions are (lambda (c) (lambda (k) (c 1))) and (lambda (c) (lambda (k) (k 1))). Substitute and simplify and both result in (lambda (k) (k 1)).

I greatly prefer delimited continuations as they have:

(reset (1 + (shift (lambda (f) f)))) <=> (lambda (v) (+ 1 v))

This can also be proved algebraically.

Answer 2

To work out the details of the follow up question we can use the code scheme-cps-convert.rkt from http://matt.might.net/articles/cps-conversion/

> (T-c '(call/cc (λ (k) 1)) 'halt)
'((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2873) ($k2873 1)) halt)
> (T-c '(call/cc (λ (k) (k 1))) 'halt)
'((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2940) (k 1 $k2940)) halt)

reducing the first expression:

  ((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2873) ($k2873 1)) halt)
= ((λ (k $k2873) ($k2873 1)) (λ (x _) (halt x)) halt)
= (halt 1)

and the second

  ((λ (f cc) (f (λ (x _) (cc x)) cc)) (λ (k $k2940) (k 1 $k2940)) halt)
= ((λ (k $k2940) (k 1 $k2940)) (λ (x _) (halt x)) halt)
= ((λ (x _) (halt x)) 1 halt)
= (halt 1)

proves they are equal, so using k or not using k in that position makes no difference.