|
The article basically shows that call/cc and Y are two sides of the
same coin. The article however makes the claims formal and proves them
as a theorem. The way of proving the theorem is interesting too: we
extensively rely on syntax-rules macros. Indeed, one macro does a
CPS transform, and another simple macro -- which is actually a
lambda-calculator -- normalizes the result of the CPS transform.
The article shows in which way (call/cc call/cc) is equivalent to (lambda (x) (x x)). If you ever felt the (call/cc call/cc) itch, you'll want to check this out.
The article makes clever use of macros. Continuations, fixpoints, CPS, higher-order syntax, syntax-rule macros and lambda-calculators all take part in this Scheme tour de force.
Great fun...
Posted to theory by Ehud Lamm on 10/1/03; 12:50:17 AM
|
|
Self-application as a fixpoint of call/cc
