Self-application as the fixpoint of call/cc

-------- Original Message --------
Subject: Self-application as the fixpoint of call/cc
Date: 18 Sep 2003 23:39:00 -0700
From: [email protected] ([email protected])
Organization: http://groups.google.com/
Newsgroups: comp.lang.scheme

We shall show in which way (call/cc call/cc) is equivalent to (lambda
(x) (x x)). We shall show how to express Y via call/cc. The result has
a distinctive feature: Y can be expressed *without* resorting to
a self-application. We shall also illustrate the use of syntax-rules
in proving theorems.

Theorem 1.
Expressions
 - ((call/cc ... (call/cc call/cc)) p)
 - ((call/cc ... (call/cc (call/cc id))) p)
 - ((lambda (x) (x x)) p)

(where p is a procedure) either
   - all yield (in CBV) values that are indistinguishable under
     a CPS transform, or
   - all diverge/stuck.
Here (call/cc ...) signify zero or more applications of call/cc, and
id is the identity function (lambda (x) x). For non-procedural values
(such as numbers, strings, etc.), the equivalence under CPS implies
identity.

Illustration (using the higher-order syntax):

   (define (p x) (if (eq? x p) '(p p) `(p ,x)))

   ((lambda (x) (x x)) p)
evaluates===> (p p)
   ((call/cc call/cc) p)
evaluates===> (p p)
   ((call/cc (call/cc call/cc)) p)
evaluates===> (p p)
   ((call/cc (call/cc (call/cc (call/cc (call/cc (lambda (x) x)))))) p)
evaluates===> (p p)

Catchy phrase 1.
	self-application is the fixpoint of call/cc

Proof. see Appendix.

Corollary 1. Y combinator via call/cc -- Y combinator without a
self-application.

(define (Y f)
  ((lambda (u) (u (lambda (x) (lambda (n) ((f (u x)) n)))))
   (call/cc (call/cc (lambda (x) x)))))

Corollary 2. factorial via call/cc

(define fact
  (lambda (f) (lambda (n)
    (if (<= n 0) 1 (* n (f (- n 1)))))))

then, given the above definition of Y,
        (list ((Y fact) 5) ((Y fact) 6) ((Y fact) 7))
does return
        '(120 720 5040)

Additional reference:
http://google.com/groups?selm=7eb8ac3e.0302131759.4735faf3%40posting.google.com

Proof of Theorem 1.

We will be using the CPS transformation, the equations for which are taken
verbatim from Danvy and Filinski "Abstracting Control" (p. 2). CPS is
a source-to-source translation. Therefore, it behooves us to use
Scheme's syntax-transformers.

(define-syntax CPS
  (syntax-rules (lambda call/cc)
    ((CPS (?e1 ?e2)) 			; application
      (lambda (k) ((CPS ?e1) (lambda (f) ((CPS ?e2) (lambda (a) ((f a) k)))))))
    ((CPS (lambda (x) ?e))		; abstraction
      (lambda (k) (k (lambda (x) (CPS ?e)))))
    ((CPS call/cc)
      (lambda (k0)
	(k0 (lambda (p) (lambda (k)
			  ((p (lambda (a) (lambda (k1) (k a)))) k))))))
    ((CPS ?x)
      (lambda (k) (k ?x)))))

We will be using Petite Chez Scheme, which provides a form (expand e)
to macro-expand an expression e.

For example,

> (expand '(CPS (lambda (x) (x x))))
(lambda (#:k)
  (#:k (lambda (#:x)
         (lambda (#:k)
           ((lambda (#:k) (#:k #:x))
            (lambda (#:f)
              ((lambda (#:k) (#:k #:x))
               (lambda (#:a) ((#:f #:a) #:k)))))))))


We can see the problem -- there are too many lambdas, some of which
could be reduced. They are administrative lambdas. Because all our
expressions here will assuredly terminate, we can use the full
normalization.

(define-syntax NORM
  (syntax-rules (lambda)
    ((NORM (lambda (x) ?e) ())
      (lambda (x) (NORM ?e ())))
    ((NORM (lambda (x) ?b) (?e . stack))
      (let-syntax
	((subst
	   (syntax-rules ()
	     ((subst x) (NORM ?b stack)))))
	(subst ?e)))
    ((NORM (?e1 ?e2) stack)
      (NORM ?e1 (?e2 . stack)))
    ((NORM ?x ()) ?x)
    ((NORM ?x stack) (unwind ?x stack))
))

(define-syntax unwind
  (syntax-rules ()
    ((unwind t (t1 ...))
      (t (NORM t1 ()) ...))))

Given above is indeed the lambda-calculator, the normal-order lambda
calculator. The particular algorithm (normalization as a yacc-style
parsing) is described in great detail in
	http://pobox.com/~oleg/ftp/Haskell/Lambda_calc.lhs

> (expand `(NORM ,(expand '(CPS (lambda (x) (x x)))) ()))
(lambda (#:k)
  (#:k (lambda (#:x) (lambda (#:k) (#:x #:x #:k)))))

which is far smaller a term to look at. It indeed matches the
derivation by hand.

Lemma 1.
CPS transform of ((lambda (x) (x x)) p) is (lambda (k) (p p k))
Proof:
> (expand `(NORM ,(expand '(CPS ((lambda (x) (x x)) p))) ()))
(lambda (#:k) (p p #:k))

Lemma 2.
CPS transform of (call/cc call/cc) is
(lambda (k) (k (lambda (a) (lambda (k1) (k a)))))
Proof:
> (expand `(NORM ,(expand '(CPS (call/cc call/cc))) ()))
(lambda (#:k)
  (#:k (lambda (#:a) (lambda (#:k1) (#:k #:a)))))

It indeed matches the derivation by hand.

Lemma 3.
CPS transform of (call/cc (call/cc call/cc)) is the same as
that of (call/cc call/cc).
Proof:
> (expand `(NORM ,(expand '(CPS (call/cc (call/cc call/cc)))) ()))
(lambda (#:k)
  (#:k (lambda (#:a) (lambda (#:k1) (#:k #:a)))))

Lemma 4.
CPS transform of (call/cc (call/cc id)) is the same as
that of (call/cc call/cc).
Proof:
> (expand `(NORM ,(expand '(CPS (call/cc (call/cc (lambda (u) u))))) ()))
(lambda (#:k)
  (#:k (lambda (#:a) (lambda (#:k1) (#:k #:a)))))

Lemma 5.
CPS transform of ((call/cc call/cc) p) is the same as
that of ((lambda (x) (x x)) p)
Proof:
> (expand `(NORM ,(expand '(CPS ((call/cc call/cc) p))) ()))
(lambda (#:k) (p p #:k))

and see Lemma 1.

Proof of the main theorem.
Let p be a term, M be ((call/cc call/cc) p) and
N be ((lambda (x) (x x)) p).

By Plotkin's simulation theorem,

CPS_transform_v{eval_v{M}} = eval_v{CPS_transform{M} (lambda (x) x)}

where '=' means observational equivalence. By Lemma 5,
CPS_transform{M} is identical to CPS_transform{N}. Therefore,

CPS_transform_v{eval_v{M}}  = CPS_transform_v{eval_v{N}}
QED.

The proof of the fixpoint follows from Lemmas 2-4 under trivial
induction.