 proof that (call/cc (lambda (c) (0 (c 1)))) => 1
started 6/14/2002; 8:08:18 AM - last post 6/16/2002; 12:34:59 PM
|
|
Ehud Lamm - proof that (call/cc (lambda (c) (0 (c 1)))) => 1 
6/14/2002; 8:08:18 AM (reads: 1945, responses: 4)
|
|
| proof that (call/cc (lambda (c) (0 (c 1)))) => 1 |
|
(via comp.lang.scheme)
William Clinger: In response to recent interest in the denotational semantics
of Scheme, and as an example of its use, I have calculated
that the expression
(call-with-current-continuation (lambda (c) (0 (c 1))))
either returns 1 to its continuation or runs out of memory.
Posted to theory by Ehud Lamm on 6/14/02; 8:10:28 AM
|
|
|
|
Paul Snively - Re: proof that (call/cc (lambda (c) (0 (c 1)))) => 1
6/15/2002; 12:23:45 PM (reads: 983, responses: 1)
|
|
|
Wow, I must be rusty on my Scheme: (call-with-current-continuation (lambda (c) (0 (c 1)))) doesn't even look valid to me because of the zero in the application position.
SCM 5d6:
ERROR: Wrong type to apply: (0 (c 1))
Scheme48 0.57:
Warning: non-procedure in operator position
(0 (c 1))
(procedure: #{Type :exact-integer #f #f})
1
MzScheme 200alpha19:
1
So here we have the gamut from "that's an error" to "that's weird, but OK" to "no problem." Personally, I'm with SCM on this one: you can't have a non-procedure in the application position.
|
|
Ehud Lamm - Re: proof that (call/cc (lambda (c) (0 (c 1)))) => 1
6/15/2002; 1:17:23 PM (reads: 1034, responses: 0)
|
|
|
According to the r4rs (sec. 4.1.3): The operator and operand expressions are evaluated (in an unspecified order)...
|
|
Darius Bacon - Re: proof that (call/cc (lambda (c) (0 (c 1)))) => 1
6/15/2002; 11:47:51 PM (reads: 958, responses: 0)
|
|
|
Re: The operator and operand expressions are evaluated (in an unspecified order)...
Doesn't matter -- it's when you apply the 0 to an argument that you'd get an error, and the continuation bound to c gets called before that, no matter what evaluation order. SCM is just wrong.
|
|
Paul Snively - Re: proof that (call/cc (lambda (c) (0 (c 1)))) => 1
6/16/2002; 12:34:59 PM (reads: 949, responses: 0)
|
|
|
Ah, I've been bitten by making assumptions about order of evaluation. Bad Paul.
It's not clear to me, though, that SCM is wrong to say "I've evaluated something that I know to be in the application position and it's not a procedure; that's an error." From R5RS:
A procedure call is written by simply enclosing in parentheses expressions for the procedure to be called and the arguments to be passed to it. The operator and operand expressions are evaluated (in an unspecified order) and the resulting procedure is passed the resulting arguments.
Not one word about what happens when "the resulting procedure" isn't one. I maintain that SCM is within its rights to evaluate a procedure application left-to-right, check the type of the evaluation of the procedure expression, and generate an error if the type is not "procedure."
Perhaps most interesting is Scheme48: it recognizes that the evaluation of (c 1) is indeed 1, that applying 0 won't work, but also that control gets passed around the application of the 0, so all is well in the end.
MzScheme, true to form, just quietly does the right thing, if your definition of the right thing includes completing evaluation if it's possible to consistently do so (by contrast with SCM, which complains about the bad type problem apparently without realizing that it doesn't matter in this context).
|
|
|
|