Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

Dismiss

32 views

Skip to first unread message

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.

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

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

0 new messages

Search

Clear search

Close search

Google apps

Main menu