Re: [Scheme-reports] Technical question

[Anton van Straaten <anton@x>]

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