Self-application as the fixpoint of call/cc
ol...@pobox.com
(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
> 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).