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

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

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!


Scheme-reports mailing list