[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: scheme-reports@x*Subject*: Re: [Scheme-reports] Technical question*From*: Anton van Straaten <anton@x>*Date*: Thu, 26 May 2011 23:03:59 -0400*In-reply-to*: <1A55FD53-518B-4615-A5F9-447C133F6557@mac.com>*References*: <19934.29464.488954.667781@winooski.ccs.neu.edu> <op.vv3zcuap0p3ku8@localhost> <1A55FD53-518B-4615-A5F9-447C133F6557@mac.com>

On 05/26/2011 07:06 PM, Jay Reynolds Freeman wrote: > I am *not* in WG1, but Aaron has asked for comments that contrast > with his opinion, so I shall risk speaking up ... > > One could argue that the continuation k which is to receive the > three values 1, 2, and 3, is within the body of the unnamed lambda > expression > > (lambda () > (call-with-current-continuation (lambda (k) (k 1 2 3))) > ;; > ;;<-- continuation k is right here, so to speak > ;; > ) > > That is, the task of continuation k is to wrap up whatever the > unnamed lambda expression is going to return, and return it. > Continuation k is not explicitly created by "call-with-values" > -- that procedure is not used in the unnamed lambda expression; > rather, continuation k is created by the unnamed lambda expression. > Thus continuation k must take exactly one value, so it is an error > for k to be called with the three values 1, 2, and 3, and an > implementation might well choose to report that error. As Andre van Tonder mentioned (or implied) in an earlier email, the formal semantics in R5RS doesn't support such an interpretation. According to the formal semantics, the result of the following expression must be 'ok: (call-with-values (lambda () (call-with-current-continuation (lambda (k) (k 1 2 3)))) (lambda (x y z) 'ok)) If anyone is interested in concrete evidence of this, you can evaluate the expression using an executable implementation of the semantics (like mine at http://www.appsolutions.com/SchemeDS/ ) Of course, without a bit of manual verification this doesn't prove anything - any executable implementation of those semantics has to make some assumptions, just as any other implementation does. However, in this case the manual verification is easy enough, because the key features in the expression map directly to features of the semantics, so there's really no room for interpretation. In particular, a semantics for call/cc and call-with-values is given in the form of the auxiliary functions cwcc and cwv, and of course the semantics of lambda terms are similarly provided. The reason the semantics lead to a single interpretation here is simple: continuations in the semantics involve multiple values by default. This is represented by all the e* terms scattered throughout the definitions. Even when a single value is passed to a function, as in the expression (f x), at the semantic level this corresponds to (applicate f <x>), where <x> is a "sequence". Sequences have zero or more values. It is then up to a called procedure to test that it receives the number of arguments it is expecting. This test can be found in the semantics for lambda terms, as e.g. #e* = #I*. So, assuming one accepts that adding restrictions to the behavior described by the semantics is invalid, and accepts that the auxiliary functions cwcc and cwv are supposed to denote the semantics of their Scheme counterparts (I'm not sure this is stated explicitly anywhere!), then thanks to the heroic efforts of our wise and now-grizzled predecessors, this is one of those cases that Leibniz dreamed about in "The Method of Mathematics"[*]: "For all inquiries which depend on reasoning would be performed by the transposition of characters and by a kind of calculus, which would immediately facilitate the discovery of beautiful results. For we should not have to break our heads as much as is necessary today, and yet we should be sure of accomplishing everything the given facts allow. "Moreover, we should be able to convince the world what we should have found or concluded, since it would be easy to verify the calculation either by doing it over or by trying tests similar to that of casting out nines in arithmetic. And if someone would doubt my results, I should say to him: 'Let us calculate, Sir,' and thus by taking to pen and ink, we should soon settle the question." Anton [*] http://www.rbjones.com/rbjpub/philos/classics/leibniz/meth_math.htm _______________________________________________ Scheme-reports mailing list Scheme-reports@x http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports

**Follow-Ups**:**Re: [Scheme-reports] Technical question***From:*Jay Reynolds Freeman <jay_reynolds_freeman@x>

**Re: [Scheme-reports] Technical question***From:*Ray Dillinger <bear@x>

**References**:**[Scheme-reports] Technical question***From:*Eli Barzilay <eli@x>

**Re: [Scheme-reports] Technical question***From:*"Aaron W. Hsu" <arcfide@x>

**Re: [Scheme-reports] Technical question***From:*Jay Reynolds Freeman <jay_reynolds_freeman@x>

- Prev by Date:
**[Scheme-reports] General comments on the draft WG1 R7 report.** - Next by Date:
**Re: [Scheme-reports] Technical question** - Previous by thread:
**Re: [Scheme-reports] Technical question** - Next by thread:
**Re: [Scheme-reports] Technical question** - Index(es):