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@scheme-reports.org
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports