Reynolds: "the basic laws of variable binding"

Question

I recently came across this passage in an article by John Reynolds (emphasis added):

...from designers innocent of the principles of programming language design, we have been given a nearly endless succession of “input formats” that seem to be designed to encourage error. (Flawed macro facilities that violate the basic laws of variable binding are particularly prominent examples.)

I was happy to come across the phrase in italics because for some time now I've been aware of having precisely this deficiency, but not knowing what to call it, and therefore failing repeatedly at finding a way to remedy it.

Can someone point me to where I can learn about these "basic laws of variable binding"?

Answer 1

See chapter 1 of Robert Harper's book Practical Foundations of Programming Languages. He formalizes syntax with binding operators using the notion of "abstract binding trees", which IIRC were originally introduced in the Nuprl proof assistant. The main keyword you need to find further information is "alpha-equivalence".

Answer 2

Reynolds is referring to so-called unhygenic macros, as found in traditional Lisp implementations, including modern Common Lisp. The basic problem is that a variable referenced in a macro might change behavior when the macro is used, or that a variable seemingly bound around a macro use could be inadvertently captured by the macro.

These issues were first remedied in macro systems for Scheme, in particular Kohlbecker et al's 1986 paper Hygenic Macro Expansion, and improved by Clinger and Rees' 1991 paper Macros that Work.