John, thank you very much for your comments.

Am Fr., 14. Aug. 2020 um 04:41 Uhr schrieb John Cowan <xxxxxx@ccil.org>:

> Suddenly you are talking about *equal* bindings, but until now (and in R[67]RS) it's about the bindings being the *same binding*.  That is, bound in one library (foo) and imported directly or indirectly from (foo) in all other libraries that use it.  Importing two libraries with *distinct* bindings is an error and is usually reported either by signaling an error or by reporting a warning.  It is not enough that the bindings are verbally identifiable: if (foo) defines `plus` with (define plus +) and (bar) does the same, then it is impossible to import both (foo) and (bar), because `plus` does not have the same binding in the two libraries.

Technically, we are talking about equivalence in the sense of
"free-identifier=?" of the appendix to R4RS and the R6RS standard
libraries. I wanted to avoid this term, so I wrote just "equal
binding" (in the sense of "same binding") but I will amend this as it
obviously led to confusion.

So, we are not inventing a third identifier equivalence (besides
"free-identifier=?" and "bound-identifier=?") here, but we are just
talking about the former. As you write, identifiers whose bindings
refer to different locations, where just the stored values are
equivalent (in the sense of "eq?", "eqv?" or "equal?") are not
interesting.

> This is why the (auto) library is good whereas the define-auxiliary-syntax macro is bad.  The library provides a single binding that all other libraries can import, and exactly how it is bound isn't important.  We have shown that it can be done with a simple syntax-rules definition, and anything fancier is just gravy.  Define-aux-syntax, though, attempts to introduce a novel (and unnecessary) notion of *equal* bindings, and should be left out altogether.

This point does not apply as no novel equality is introduced here. I
am sorry for the confusion and will amend the document accordingly.

Actually, introducing the same binding (in the sense of
"free-identifier=?") is nothing novel. Chez, for example, has the
"alias" form, which exactly does this, namely giving an identifier the
same binding as an existing identifier in scope. (It's a nice feature,
which I have already used.)

Operationally, in the expander model of Dybvig, two bound identifiers
are "free-identifier=?" if and only if they have the same label.

I hope this explanation helps to see that the local binding form
"define-auxiliary-syntax" does no more magic than a local import of
the magic "auto" library would do.