Re: [Scheme-reports] Errors (?) in 7.2, Formal Semantics

Hi Will,

Thank you for the detailed review!

On Thu, Nov 27, 2014 at 8:50 AM, William Cushing <william.cushing@x> wrote:

I'm trying to grok the formal semantics section, 7.2, of r7rs small.

It seems to me there are numerous small errors, but perhaps I'm just confused.

I don't see any errata for the formal section on the web page; and I couldn't find a better place to submit bugs....so, here goes:

;;;;
;; car-internal
;;;;

As written, the declared type of car-internal is "_expression_-value to
_expression_-continuation to command-continuation" (E->K->C).

However, the definition starts with "lambda ewk", and results in calling hold on two
args (and that results in a command-continuation). So the type of the
definition is "_expression_-value to dynamic-point to _expression_-continuation
to command-continuation" (E->P->K->C).

Based on how car-internal is called, the fix appears to be: simply delete
the w in the definition (that is, delete the \omega). In other words, the
type statement is correct, but the definition is not.

The addition of the w (dynamic point) arguments comes from reference 40,

"How to Add Threads to a Sequential Language Without Getting Tangled Up"

by Gasbichler, et al. I think we trusted too much that any errata in that

would have turned up by now and didn't do a thorough enough review on

our end.

For this case I think you are exactly correct, and we should delete the \omega.

;;;;
;; valueslist
;;;;

As-is the definition of valueslist resembles:

;; E->K->C
(define valueslist
(lambda (e k)
(if (pair? e)
(cdr-internal e
(lambda (e*) ; (0)
(valueslist e* ; (1)
(lambda (e**)
(car-internal e
(single (lambda (e+) ; (2)
(k (list* e+ e**)))) ; (3) list*=cons
))
))
)
;; not a pair
(if (null? e) (k (list)) (error "non-list argument to
*values-list*"))
)))

At (1), e* will be a (singleton) sequence of values, but values-list does
not accept a sequence of values as its first argument. Since car-internal
and cdr-internal work by sending a singleton sequence to their
_expression_-continuation, it seems that (1) should be:

(valueslist (first e*) ...) ; (A)

Alternatively, (0) could be:

(single (lambda (e++) (valueslist e++ ...)) ; (B)

That is perhaps more pleasing, since it would be symmetric with how
car-internal is called at (2).

On the other-hand, calling internal functions (bypassing type-checks)
suggests complete confidence, and so perhaps bypassing
argument-count checking (from single) is desirable as well. If so,
then (A) is preferable, and for symmetry, likewise (2) should be:

(lambda (e***) (k (list (first e***) e**) )) ; (A')

Again I think you're analysis is spot-on. I prefer (A').

Incidentally, list->values seems more Scheme-y than valueslist.

The RnRS denotational semantics has always avoided punctuation

in identifiers, probably because it uses infix notation. This rule was

only broken in the new change for c[ad]r-internal (arguably in the

spirit of Dylan).

This is all I have time for now, and I'll be traveling the next week,

but will get back to this afterwards.

Thanks again!

Alex