From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED!not-for-mail From: Mark H Weaver Newsgroups: gmane.lisp.guile.devel Subject: Mistakes in the R7RS-small formal denotational semantics Date: Tue, 20 Jun 2017 22:45:22 -0400 Message-ID: <87podykqil.fsf@netris.org> NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: blaine.gmane.org 1498013147 22819 195.159.176.226 (21 Jun 2017 02:45:47 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 21 Jun 2017 02:45:47 +0000 (UTC) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) Cc: guile-devel@gnu.org To: Alex Shinn , cowan Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Wed Jun 21 04:45:40 2017 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dNVeF-0005Zs-Qa for guile-devel@m.gmane.org; Wed, 21 Jun 2017 04:45:39 +0200 Original-Received: from localhost ([::1]:51516 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dNVeK-0005JC-WD for guile-devel@m.gmane.org; Tue, 20 Jun 2017 22:45:45 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33270) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dNVeF-0005Iq-U2 for guile-devel@gnu.org; Tue, 20 Jun 2017 22:45:41 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dNVeC-0001Ec-HW for guile-devel@gnu.org; Tue, 20 Jun 2017 22:45:39 -0400 Original-Received: from world.peace.net ([50.252.239.5]:43637) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dNVeC-0001EB-A7 for guile-devel@gnu.org; Tue, 20 Jun 2017 22:45:36 -0400 Original-Received: from pool-72-93-34-106.bstnma.east.verizon.net ([72.93.34.106] helo=jojen) by world.peace.net with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1dNVUF-0006vQ-6Q; Tue, 20 Jun 2017 22:35:19 -0400 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-Received-From: 50.252.239.5 X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: "guile-devel" Xref: news.gmane.org gmane.lisp.guile.devel:19225 Archived-At: 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: <(=CF=89=E2=82=81,=CF=89=E2=82=81|(F=C3=97F=C3=97P)=E2=86=932)> should be: <(=CF=89=E2=82=81|(F=C3=97F=C3=97P)=E2=86=933,=CF=89=E2=82=81|(F=C3=97F= =C3=97P)=E2=86=932)> and similarly, in 'pathdown', the final element of the result sequence: <(=CF=89=E2=82=82,=CF=89=E2=82=82|(F=C3=97F=C3=97P)=E2=86=931)> should be: <(=CF=89=E2=82=82|(F=C3=97F=C3=97P)=E2=86=933,=CF=89=E2=82=82|(F=C3=97F= =C3=97P)=E2=86=931)> 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. ((=CF=80*=E2=86=931)= =E2=86=932) 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 ((=CF=80*=E2=86=931)=E2=86=932). 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 =CE=BA. Regards, Mark