# Self-application as the fixpoint of call/cc

20 views

### ol...@pobox.com

Sep 19, 2003, 2:39:00 AM9/19/03
to
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)

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

> (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.

### Joe Marshall

Sep 19, 2003, 9:49:40 AM9/19/03
to
ol...@pobox.com (ol...@pobox.com) writes:

> 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)))))

(call/cc (lambda (x) x)) *is* self-application (albiet disguised).