Re: [Scheme-reports] Technical question

[Jay Reynolds Freeman <jay_reynolds_freeman@x>]

Perhaps the formal semantics have not correctly captured the
language?  The text description, "Except for continuations created
by the call-with-values procedure, all continuations take exactly one
value," does not seem to offer any leeway for the interpretation that
Andre suggests.  (The R7 draft and R5 are identical here.)

Lest I be accused of excessive pedantry, I point out that the description
of what the formal semantics is, in the the introduction to chapter 7
(and again R7 and R5 are identical in  wording) suggests that
the purpose of the formal semantics is to capture the informal
description rather than to serve in its own right as a definition
of Scheme.  If the question of what to do with multiple values has
only just come up, there is no particular reason to think that whoever
wrote the formal semantics got it right.

Jay Reynolds Freeman
-------------------------------
Jay_Reynolds_Freeman@x
http://web.mac.com/Jay_Reynolds_Freeman



On May 26, 2011, at 8:03 PM, Anton van Straaten wrote:

> 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


_______________________________________________
Scheme-reports mailing list
Scheme-reports@x
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports