Report of bug in R7RS-small formal semantics

[John Cowan]

Can someone who feels competent with the R7RS-small formal semantics take a look at <https://github.com/johnwcowan/r7rs-work/issues/39> and see if it makes sense?  Formal semantics is not my thing.

Thanks.

[Steven Ganz]

I just took a look at it.

This indeed appears to be a valid but minor bug.

car-internal takes an unused ω∈P argument, unnecessarily, I think, because it doesn't need to access arbitrary library functions, so that argument doesn't have to be passed in.

car-internal = λεωκ . hold(ε | E_p ↓ 1)κ

would be replaced with:

car-internal = λεκ . hold(ε | E_p ↓ 1)κ

Otherwise, the handling of car looks OK to me.  We could have dealt with errors differently in the formal semantics, pushing them into the answer type A, but that isn't anything to address now.

Going through that, I noticed something even more minor.  It appears that the definition of send uses a round paren "(" in place of a left angle bracket "<".

send = λεκ . κ(ε>

would be replaced with:

send = λεκ . κ<ε>

Steve

---

From: "John Cowan" <co...@ccil.org>
To: "scheme-reports-wg1" <scheme-re...@googlegroups.com>
Sent: Sunday, February 5, 2023 11:45:38 AM
Subject: [scheme-reports-wg1] Report of bug in R7RS-small formal semantics

Can someone who feels competent with the R7RS-small formal semantics take a look at <https://github.com/johnwcowan/r7rs-work/issues/39> and see if it makes sense?  Formal semantics is not my thing.

Thanks.

--
You received this message because you are subscribed to the Google Groups "scheme-reports-wg1" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scheme-reports-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/scheme-reports-wg1/CAD2gp_RRk29ymcjkw9H7rVbmaO34VGw4bTx0f-76ofUqOxKCAA%40mail.gmail.com.

[Steven Ganz]

I'm also noticing an error in cons, with two arguments being swapped.

twoarg( λε₁ε₂κωσ . new σ ∈ L →

would be replaced with:

twoarg( λε₁ε₂ωκσ . new σ ∈ L →

---

From: "Steven Ganz" <steve...@genetius.com>
To: "scheme-reports-wg1" <scheme-re...@googlegroups.com>
Sent: Sunday, February 5, 2023 4:40:21 PM
Subject: Re: [scheme-reports-wg1] Report of bug in R7RS-small formal semantics

[John Cowan]

If  you could prepare a patch for these issues, that would be great.  Also, please check out any other issues related to formal semantics at johnwcowan/r7rs-work.

To view this discussion on the web visit https://groups.google.com/d/msgid/scheme-reports-wg1/1132123391.24283848.1675635276111.JavaMail.zimbra%40genetius.com.

[Steven Ganz]

I just put a pull request through, covering #39 & #40.  The latter was the only other semantics-related issue?

Steve

---

From: "John Cowan" <co...@ccil.org>
To: "scheme-reports-wg1" <scheme-re...@googlegroups.com>

Sent: Friday, February 10, 2023 3:55:30 PM

To view this discussion on the web visit https://groups.google.com/d/msgid/scheme-reports-wg1/CAD2gp_TYyNT0vZWDz-fmigiY2He_ufTPmfQjHi50Ttux0SofEA%40mail.gmail.com.