Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc
The presentation at the Workshop ``Daniel P. Friedman: A Celebration.'' December 4, 2004. Bloomington, IN
Normal-order direct-style beta-evaluator with syntax-rules,
and the repeated applications of call/cc Repeated applications of call/cc , formally
, formally Normal-order direct-style beta-normalizer as syntax-rules
Use (2) to prove (1)
A few less common examples
The title of the talk, in the expanded form, is _this_. We will talk about less frequently mentioned applications of call/cc and hygienic Scheme macros. For example, we will use macros as a sort of a proof assistant, to help in tedious lambda-calculations. As you will see, we will be talking about undelimited and delimited continuations, continuation-passing style transforms -- with a detour on hygienic macros and beta-normalization. It should come as no surprise that all these topics are directly influenced by Dan Friedman -- and, in fact, developed straight in response to his challenges. Perhaps he didn't know about that though.
The call/cc challenge ((call/cc call/cc) (call/cc call/cc)) (call/cc call/cc) ==> ?? (call/cc (call/cc call/cc)) ==> ?? (call/cc ... (call/cc call/cc)) ==> ?? (call/cc ... (call/cc id)) ==> ?? (define (p x) (if (eq? x p) '(p p) `(p ,x))) ((call/cc (call/cc call/cc)) p) ===> (p p)
It all started about two years ago, upon the meditation on this famous incantation. It was disclosed by Shriram on USENET. What is the application of call/cc to itself? And one more time? And a few more times? What if we have the identity function? To be sure, on one hand, these questions seem trivial. We can easily find the answer if we just apply these things to a suitable function, like that. It'll tell us what is being applied to what. This is an instance of a type-directed partial evaluation, btw. So we easily find out that all these expressions are just self-applications. A more interesting question is this: are there any side-conditions on p? Can we prove it? As we know, the field of first-class continuations is sufficiently interesting to reasonably doubt one's intuition and rely on a formal proof instead. BTW, there was one surprise, to be mentioned later.
... continue reading