Lean 4 macro paper "binding position"

Stream: lean4

[Chris B]

In the "Beyond Notations" paper about Lean 4's macro system, the terms "binding position" and "binding core form" are used without really being explained. Reading the relevant sections gave me some intuition about it, but can someone with knowledge of the macro system help define those?
Thanks

[Chris B]

My intuition is that it encompasses both "if it's on the left hand side of the macro_rules invocation and can later be referenced in the right hand side", and traditional binders (lambda, let, pi) on either side.

[Justus Springer]

I wouldn't say on either side. For example, in the term λx.x, I'd consider the first occurrence of x to be in binding position, while the second occurrence is "bound".

[Justus Springer]

And similarly, a variable occurring in the binding pattern of a macro rule (so on the left of the "=>") would be in binding position, but not on the right.

[Chris B]

I would agree with that, I may have worded my guess imprecisely; the first x would be "in binding position" and the second x would just be what the paper calls a reference.

[Chris B]

That was another question actually, what's in the space between "binding position" and a reference. A reference is defined as " an identifier not in binding position", with the expansion procedure failing when it comes across a reference that doesn't match a local or top-level item, but in the second example:

macro "m" n:ident : command => `(
  def f := 1
  macro "mm" : command => `(
    def $n := f
    def f := $n))

the first f doesn't seem to be in binding position so should be a reference, but expansion doesn't fail even though it doesn't match a local or top-level item.

[Mario Carneiro]

The first f is in binding position, I think

[Chris B]

I assume you're right since there's no error about it being unbound, but that circles back to the desire for a definition of "binding position".

[Mario Carneiro]

intuitively, I would say that an identifier occurrence is in binding position if it is subject to alpha renaming, where you can change the given occurrence and all later uses of the same identifier without changing the meaning of the code

[Mario Carneiro]

a formal definition would have to enumerate all the syntactic constructs and mark each use of ident as being a binding occurrence or not

[Chris B]

Subject to alpha renaming seems pretty solid, I'll take it.

[Mario Carneiro]

But I don't think macros actually know this information. The only scoping relevant to macros are macro scopes, which are constructed when you have macro-macros like the example

[Mario Carneiro]

The determination of whether an identifier is a binder or not only happens during elab