Self-application as the fixpoint of call/cc

20 views
Skip to first unread message

ol...@pobox.com

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

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.

Joe Marshall

unread,
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).

Reply all
Reply to author
Forward
0 new messages