Toward (call/cc (lambda (c) (0 (c 1)))) => "bad procedure"
Bill Richter
(call/cc (lambda (c) (0 (c 1)))) => 1
and I'm glad I did, as it uncovered a bug in my DS code. Thanks, Al &
Thomas and Will! Wasn't too hard DS once I found my bug. I'll post a
full solution tomorrow.
In hindsight, it seems pretty obvious. c is bound to the "escape
continuation", and when we evaluate
(0 (c 1))
first 0 & (c 1) are evaluated, before the DS checks that 0 isn't a
function, and then c applies the "escape continuation" to 1. Cool.
I'd like to change the DS to where instead we get "bad procedure", and
this can be done by using my bug :) I suppose what I've really
figured out is why the DS isn't suitable for hand calculations.
OK, I want the DS to get rid of the permute/unpermute stuff, which
David Rush said long ago didn't really express the Scheme compiler's
freedom of arbitrary evaluation order anyway.
Then, we can make a small change. Right now (assuming left-to-right
evaluation order), the DS does
(curly-E[[ (E_0 E*) ]] rho kappa) = (curly-E[[ E_0 ]] rho kappa_1)
where
kappa_1 = single(lambda (l) (curly-E*[[ E* ]] rho kappa_2))
kappa_2 = (lambda (l) (if (f in F)
(f l kappa)
(wrong "bad procedure")))
Note `single' produces an error message as well, it's:
single(psi) = (lambda (l) (if (= (length l) 1))
(psi (car l))
(wrong "wrong number")))
My bug (which I now recommend!) was to put the two error messages
together, and define a new function `single-F' by
single-F(psi) = (lambda (l) (if (and
(= (length l) 1)
((car l) in F))
(psi (car l))
(wrong "wrong #/bad proc")))
and then define again
(curly-E[[ (E_0 E*) ]] rho kappa) = (curly-E[[ E_0 ]] rho kappa_1)
and now we make a change:
kappa_1 = single-F(lambda (l) (curly-E*[[ E* ]] rho kappa_2))
kappa_2 = (lambda (l) (f l kappa))
The upshot is that now the DS detects that 0 is a bad procedure before
evaluating (c 1), so we don't escape.
My guess is that folks won't like this change. I can still do hand
calculations with single and not single-F, but I contend it's
impossible to do hand calculations with permute/unpermute.
Finally doing Al's calculation exposed a weakness in by SICP-ish DS as
well. I was only talking about the simple non-call/cc version. With
the full R5RS K-ification, we have a real need for
F = E* x K -> C
because our captured continuations live there. I'm not sure how to
handle this problem. Somebody posted a while back a paper of Filinsky
I think (I have the paper at home) about an LC_v approach to
continuations. That sounds like a good thing for me to read now!
But I think the only way to K-ify my SICP-ish non-call/cc DS is to
define a more syntactic version of continuations, and I'm at a loss.
Heck, the main reason I've been reading the R5RS DS at all is to
_learn_ about continuations!
--
Bill
<http://www.math.nwu.edu/~richter>
Bill Richter
First, some formulas:
applicate: E x E* x K x S ---> A
(applicate f l kappa sigma) = (if (in-F? f)
(f l kappa sigma)
(wrong "bad procedure" sigma))
where wrong: X x S ---> A sends error message (AFAIK not using sigma).
For simplicity I'm getting rid of permute/unpermute. I'll simplify S
to (L -> E), getting rid of the boolean flag, and drop the
L-coordinate for procedure values (only used by eqv?), so that's
F = E* x K x S -> A
I'm consistently "un-currying" the R5RS DS definitions to what I think
is a more sensible Scheme convention, as in these 3 examples and also
curly-E: Expressions ---> (U x K x S -> A)
Simplest formulas we need are are
(curly-E[[ nu ]] rho kappa sigma) = (kappa <nu> sigma)
(curly-E[[ (I nu) ]] rho kappa sigma) = (phi <nu> kappa sigma)
if (sigma (rho I)) = phi in F.
for a number nu and a variable I. We have a general formula for a
1-arg combination:
(curly-E[[ (A B) ]] rho kappa sigma)
= (curly-E[[ A ]] rho single(lambda (f s)
(curly-E[[ B ]] rho single(lambda (e s)
(applicate f <e> kappa s)) s)) sigma)
Restricting to a non-procedure 1st arg, say Al's 0, we have
(curly-E[[ (0 B) ]] rho kappa sigma)
= (curly-E[[ B ]] rho kappa_1 sigma)
kappa_1 = single(lambda (e s) (wrong "bad procedure" s))
That's basically Al's formula in a nutshell: instead of returning the
error message "bad procedure", we stick it in the continuation, which
we never reach, since call/cc replaces it with the original cont.
Now we'll do call/cc for a 1-arg 1-body-form lambda expression:
(curly-E[[ (cwcc (lambda (x) B)) ]] rho kappa sigma)
= (curly-E[[ B ]] rho_1 kappa sigma_1)
where rho_1 & sigma_1 are extensions of rho & sigma with
x -rho_1--> (new sigma) -sigma_1--> phi_kappa
where phi_kappa is the procedure value (lambda (l k s) kappa l s).
Now we're ready for Al's formula. For kappa the initial continuation,
which prints out values, we have:
(curly-E[[ (cwcc (lambda (c) (0 (c 1)))) ]] rho kappa sigma)
= (curly-E[[ (0 (c 1)) ]] rho_1 kappa sigma_1)
c -rho_1--> (new sigma) -sigma_1--> phi_kappa
phi_kappa = (lambda (l k s) kappa l s) in F
= (curly-E[[ (c 1) ]] rho_1 kappa_1 sigma_1)
kappa_1 = single(lambda (e s) (wrong "bad procedure" s))
= (phi_kappa <1> kappa_1 sigma_1)
= (kappa <1> sigma_1) = 1
Great work, Al! "For 59 years I've put up with it now!
I must stop Xmas from coming, but how?" --Ted G
I'm sure Will is doing the same thing, but I couldn't follow his
proof. I've forgotten what hold, lookup, tievals etc even mean.
But now instead let's use my single-F, for which I'll give a better
definition today:
single-F: (F x S -> A) ---> (E* x S -> A)
single-F(psi) = (lambda (l s) (if (= (length l) 1)
(if (in-F? (car l))
(psi (car l) s)
(wrong "bad procedure" s))
(wrong "wrong number args" s)))
Then we have a new formula for a 1-arg combination:
(curly-E[[ (A B) ]] rho kappa sigma)
= (curly-E[[ A ]] rho single-F(lambda (f s)
(curly-E[[ B ]] rho single(lambda (e s)
(f <e> kappa s)) s)) sigma)
And then if we have 0 in the 1st position, we get
(curly-E[[ (0 B) ]] rho kappa sigma)
= (wrong "bad procedure" sigma)
and so we'd get instead
(curly-E[[ (cwcc (lambda (c) (0 (c 1)))) ]] rho kappa sigma)
= (curly-E[[ (0 (c 1)) ]] rho_1 kappa sigma_1)
c -rho_1--> (new sigma) -sigma_1--> phi_kappa
phi_kappa = (lambda (l k s) kappa l s) in F
= (wrong "bad procedure" sigma_1)
= "bad procedure"
But I suspect no one will want to adopt this new definition of
curly-E[[ (A B) ]] because it rejects the arbitrary order of
evaluation.
Final notes: to extend my compositional SICP-ish DS to the full
K-ified R5RS DS, I need a more syntactic definition of continuations.
the procedure value (lambda (l k s) kappa l s) in F = E* x K x S -> A
is certainly not in my U x text-of-lambda. I can't think of a slick
way to do this, so I'll book up on the LC_v control literature, but
it's obvious that it can be done. See, we're not getting arbitrary
continuations! If we had to deal with an arbitrary
kappa in K = (E* x S -> A)
then we've got serious Scott-model-requiring
E = X + (E -> E)
problems. But of course, we don't. We have the initial continuation,
which is quite complicated, but then all our other continuations are
just lambda expressions involving the original kappa. At least, in my
hand calculations, that's all I've seen. And that yields an ad-hoc
syntactic definition of the cwcc procedure values which takes us
comfortably away from the full Scott-ish F = E* x K x S -> A.
I suspect nobody is willing to give up permute/unpermute either. So
what's needed is to prove theorems that for "good" combinations (no
mutation ops causing trouble, just as they teach is a 1st yr Scheme
course), we can choose any order we like. My CPS isn't good enough
yet to see how to prove this, but I'll work on. I'm sure such
theorems are known.
But the CPS is too time-consuming to wade through anyway. As a CPS
exercise, I've enjoyed my R5RS DS hand calculations, but what's needed
is a theorem that says that under some conditions we can retreat to
the simpler non-K DS
curly-simple-E: Exp ---> (U x S -> E x S).
I'm not even sure how to state such a result, but something like
that's needed. Something to the effect that
(curly-E[[ X ]] rho kappa sigma)
= (kappa <(curly-simple-E[[ X ]] rho sigma)_1>
(curly-simple-E[[ X ]] rho sigma)_2 )
And maybe that's it for me. If so, happy scheming, hope to be back in
a few years, I'm off to the Lambda algebra, which is in fact the very
simply defined Z/2-algebra generated by symbols lambda_i, i = 0,1,2...
with relations, for p, n \ge 0:
sum_{k=0}^n (n choose k) lambda_{p+k} lambda_{2p+1+n-k} = 0.
--
Bill
<http://www.math.nwu.edu/~richter>
David Rush
> OK, I want the DS to get rid of the permute/unpermute stuff, which
> David Rush said long ago didn't really express the Scheme compiler's
> freedom of arbitrary evaluation order anyway.
I wish I really could take credsit for this, but I'm pretty sure that
was Al* or Matthias. I'm basically just one of those users who treats
the DS as a compiler to a pure-functional-language. I burn my brain
cells for other stuff (like figuring out how to automatically derive
morphology from a dictionary).
david rush
--
To have no errors
Would be life without meaning
No struggle, no joy
-- Joe McCabe (Techy Fella at Netscape)