13
$\begingroup$

Here is the context (Structure and Interpretation of Computer Programs, section 1.1.8, under heading "Local names"):

A formal parameter of a procedure has a very special role in the procedure definition, in that it doesn't matter what name the formal parameter has. Such a name is called a bound variable, and we say that the procedure definition binds its formal parameters. The meaning of a procedure definition is unchanged if a bound variable is consistently renamed throughout the definition.

At the end of that last line, there is a footnote (26), which says:

The concept of consistent renaming is actually subtle and difficult to define formally. Famous logicians have made embarrassing errors here.

What or who is the text referring to? Why would defining "consistent renaming" be hard, which logicians have made errors trying to define this, and what were those errors?

$\endgroup$
  • 3
    $\begingroup$ I tell my students that the only way to understand "consistently rename bound variables" is to implement the damn thing correctly. Many logic books avoid the issue, give incomplete renaming procedures, or at the very least omit proofs that the given renaming procedures are correct. But I do not know which particular gossip the book refers to. $\endgroup$ – Andrej Bauer Sep 22 '18 at 9:25
  • 5
    $\begingroup$ Precisely dealing with variable renaming, fresh names, capture-avoiding substitution, and the like, is one of the most trivial things that quickly becomes really cumbersome in definitions and proofs. For such a trivial issue, one does not want to spend more than a trivial amount of mental cycles, yet much more than that would be needed to avoid a lot of tricky captures / collisions / etc. Often, PL people take some care in their definitions, but then invoke the "Barendregt convention" and ignore the issue, somewhat abusing "fresh" here and there, when needed. $\endgroup$ – chi Sep 22 '18 at 9:26
  • 1
    $\begingroup$ I'd appreciate more concrete answers, below in the answer box, if at all possible. These comments still make the issue sound mysterious as you have written them to be read by someone who is already acquainted with the issue at hand, whereas I am not $\endgroup$ – ubadub Sep 22 '18 at 17:45
  • $\begingroup$ @chi in particular I'd appreciate reading recommendations that deal with this topic, if you have any. Thanks in advance $\endgroup$ – ubadub Sep 23 '18 at 16:27
11
+50
$\begingroup$

This is a partial answer: I have no idea about which errors or people SICP is referring to. I can only provide some hints about "why" variable renaming can be painful to handle precisely.

First of all, it does seem trivial to define. For instance, we can rename bound variables in indexed sums

$$ \sum_x e = \sum_y (e\{y/x\}) $$

where $e$ is any expression, and $e\{y/x\}$ denotes the syntactic replacement of each $x$ with $y$. Trivial, right?

Well, if we blindly apply the rule above, we get

$$ \sum_x (x+y) = \sum_y (y+y) $$

That's not good. We need to add the requirement "$y$ does not occur in $e$", or we get a name clash.

Now, consider this correct renaming

$$ \sum_x \sum_y (x+y) = \sum_x \sum_z (x+z) $$

if we want to rename $x$ into $y$, by the rule above we can do it on the right hand side, but not on the left hand side. That's inconvenient, since the two differ only by a renaming, so they should be handled in the same way.

A typical approach here is to resort to redefining $e\{y/x\}$ as "capture-avoiding substitution", and relax the requirement "$y$ does not occur in $e$" and use instead "$y$ does not occur free in $e$".

We then define free occurrences:

$$ free(x)=\{x\} \qquad free(e+t) = free(e)\cup free(t) \qquad free(\sum_x e) = free(e)\setminus\{x\} $$

Finally, capture avoiding substitution:

  • $x\{t/y\}$ is $t$ if $x=y$, and $x$ otherwise.
  • $(e+e')\{t/y\} = e\{t/y\} + e'\{t/y\}$ (easy case)
  • $(\sum_x e)\{t/y\} = ??$

The last case is painful. If $x=y$, the substitution is no-op, since we want it to affect free variables only, and $x$ is bound. So the result is just $\sum_x e$.

If $y\neq x$, we would like to say that $(\sum_x e)\{t/y\} = \sum_x (e\{t/y\})$. This however is wrong, in general, since if $x$ occurs free in $t$ we get a capture.

Sigh. So, we let $z$ to be the "first" variable which is 1) not $y$, 2) not free in $t$, and 3) not free in $\sum_x e$. Here, "first" means that we need to well-order the set of variable names (e.g. by picking a bijection between names and naturals). Then, we finally let $(\sum_x e)\{t/y\} = \sum_z (e\{z/x\}\{t/y\})$.

I hope I got it right. (My first attempt was wrong, by the way)

Some authors consider more cases, but the result is the same "up to renaming". The choice of the "first" $z$ does not really matter above: any such $z$ would work fine, and lead to the same result (again, up to renaming).

Now, finally, we have a sound definition of renaming ($\alpha$-conversion) and capture-avoiding substitution of a free variable. Above, I considered sums, but they apply to all binders (e.g. $\lambda x$ in the lambda calculus, function definitions in many PLs, etc.).

Now, imagine having to deal with this intricate definition every time we want to prove something in PL theory. We could, but we do not want to. It's boring, tedious, error-prone, clutters the proof and provides no insight to the reader. For this reason, many PL authors simply skip the details by saying (or even taking as granted!) that terms are to be taken "up to variable renaming", that all bound variables are assumed distinct from whatever they need to be distinct from, that we assume the "Barendregt convention", or something to the same effect.

To be brutally honest, this is cheating in proofs. We could also add "wink wink, nudge nudge, say no more!" in the same spirit. We essentially ask for mercy and tell the reader: "look, this is boring, I do not want to do it, you do not want to read it -- we both know that, with a huge effort, we could rewrite this proof to include all the details".

Technically, it is possible to exploit this shortcut to prove a false statement. The experienced proof reviewer, however, knows what is "morally fine" and could made perfect (with great effort), and what is suspicious. The latter could include something which depends on the actual choice of bound names (so we are not really working "up to" as promised!). In those cases, the review will ask for more details, so that (s)he can be convinced.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.