Fwd: Mistakes in the R7RS-small formal denotational semantics

[John Cowan]

Formal semantics folks should look at this.

---------- Forwarded message ----------
From: Mark H Weaver <m...@netris.org>
Date: Tue, Jun 20, 2017 at 10:45 PM
Subject: Mistakes in the R7RS-small formal denotational semantics
To: Alex Shinn <alex...@gmail.com>, cowan <co...@ccil.org>
Cc: guile...@gnu.org


Hi Alex and John,

I believe I've found a few mistakes in the formal denotational semantics
for R7RS-small.  The scheme-reports mailing list seems to be gone, so
I'm not sure where to send this.

First, if I understand correctly, the 'pathup' and 'pathdown' auxiliary
functions associate the wrong dynamic point with each before/after
thunk.  In 'pathup', the first element of the result sequence:

  <(ω₁,ω₁|(F×F×P)↓2)>

should be:

  <(ω₁|(F×F×P)↓3,ω₁|(F×F×P)↓2)>

and similarly, in 'pathdown', the final element of the result sequence:

  <(ω₂,ω₂|(F×F×P)↓1)>

should be:

  <(ω₂|(F×F×P)↓3,ω₂|(F×F×P)↓1)>

These changes are needed to match the english description of
'dynamic-wind' in R7RS, which says "The before and after thunks are
called in the same dynamic environment as the call to 'dynamic-wind'".

They are also needed for consistency with the 'dynamicwind' auxiliary
function, which calls the before and after thunks in accordance with the
english specification during the normal code path through 'dynamic-wind'
(e.g. when call/cc is not used).

Because of the mistakes above, the current R7RS formal semantics specify
that the before and after thunks, when called implicitly by invoking a
first-class continuation, are called in the same dynamic environment as
the call to the inner thunk of 'dynamic-wind'.

Another problem: 'travelpath' contains a type error.  ((π*↓1)↓2) has
type F (a procedure value), but what's needed in that context is the
second member of F, which has type E* -> P -> K -> C.  The easiest fix
would be to insert 'applicate' before ((π*↓1)↓2).

These mistakes were inherited from the paper "How to Add Threads to a
Sequential Language Without Getting Tangled Up" by Gasbichler, Knauel,
Sperber and Kelsey.

I also found a mistake that was apparently inherited from R5RS: in
'cwv', the final call to 'applicate' is missing its continuation
argument κ.

     Regards,
       Mark