# How do I interpret the wording of this passage about abstract binding trees from the book Practical Foundations of Programming Languages

On page 7/8, section 1.2, of Practical Foundations of Programming Languages, 2nd edition, Robert Harper gives this initial definition of abstract binding trees:

The smallest family of sets closed under the conditions

1. If $x \in \mathcal{X}_s$, then $x \in \mathcal{B}[\mathcal{X}]_s$
2. For each operator $o$ of arity $(\vec{s_1}.s_1,\ldots,\vec{s_n}.s_n)s$, if $a_1 \in \mathcal{B}[\mathcal{X},\vec{x_1}]_{s_1},\,\ldots,\, a_n \in \mathcal{B}[\mathcal{X},\vec{x_n}]_{s_n}$, then $o(\vec{x_1}.a_1;\ldots;\vec{x_n}.a_n) \in \mathcal{B}[\mathcal{X}]$

(Here $\mathcal{X}$ denotes a set of variables, $\mathcal{X},x$ the union of $\mathcal{X}$ with $\{x\}$ where $x$ is fresh for $\mathcal{X}$, $\vec{x}$ a sequence of variables,$\mathcal{X}_s$ a set of variables of sort $s$, $\mathcal{B}[X]_s$ the set of abstract binding trees of sort $s$ over the variables in $\mathcal{X}$

This definition is almost correct, but fails to properly account for renaming of bound variables. An abt of the form $\text{let}(a_1;x.\text{let}(a_2;x.a_3))$ is ill-formed according to this defnition, because the first binding adds $x$ to $\mathcal{X}$, which implies that the second cannot also add $x$ to $\mathcal{X},x$, because it is not fresh for $\mathcal{X},x$.

I am confused about his meaning here.

How does this definition result in an ill-formed abt?

By first/second binding does he mean A) outer/inner (read from left to right) or B) inner/outer (read from the inside out)?

What I think he is saying:
Because of the outer("first") binding of $x$, assume that $x$ occurs free in $a_2$. For example $a_2=x,\, a_3=x$. Then because $x$ occurs free in $a_2$, it must be that $a_2 \in \mathcal{B}[\mathcal{X}]$ where $\mathcal{X} = \{x\}$. Since $a_3$ occurs inside an abstractor that binds $x$, $a_3 \in \mathcal{B}[\mathcal{X,x}]$, but then $a_3 \in \mathcal{B}[\{x\},x]$ which is ill-formed since $x$ is not fresh for $\{x\}$

But then I think of the concrete example $\text{let}(y,x.\text{let}(z,x.x))$ in which $a_2 \in \mathcal{B}[\{z\}]$ and $a_3 \in \mathcal{B}[\{z\},x]$, which poses no problems in this interpretation.

### Edit to elaborate on the accepted answer...

What I now believe Harper meant is that the outer binding of $x$ indicates that $x$ is considered to be among the free, or "already used" variables in the inner let. This may or may not mean that $x$ must actually appear free in the inner let.

In either case, it means that validation of abts for well-formedness must proceed from the outside-in. In the specific examples Harper gives, the outer binding of $x$ means $x \in X$ in the validation of the inner let:
if $a_2 \in \mathcal{B}[\mathcal{X}]$ and $a_3 \in \mathcal{B}[\mathcal{X},x] \ldots$ (<-- ill formed; $x$ is not fresh for $\mathcal{X}$)

If in particular the wording means that $x$ must specifically appear free in the inner let, then in the given example, it would have to be in $a_2$ as suggested in my question and in the answer below. This amounts to saying that a particular instance of an abt in $\mathcal{X}$ is not automatically an abt in $\mathcal{X}\cup\mathcal{Y}$ for any set of variables $\mathcal{Y}$.

• The incorrect definition incurs capture, whereas capture-avoiding substitution is generally regarded as a pillar of proper language design. – gardenhead Nov 24 '16 at 17:48
• @gardenhead I think you are incorrect in that this definition does not incur variable capture, which is an orthogonal issue. That is dealt with in the definition of substitution. Here he is speaking of the definition of a valid abstract binding tree. In fact, in the book his later (deemed correct) definition of abstract binding trees accepts $\text{let}(a_1,x.\text{let}(a_2,x.a_3))$ as a valid abt. – afsmi Nov 25 '16 at 2:27
• Validation proceeds outside-in, and in B[X] the set X is the set of variables that can occur, not actually the set of free variables. Both things are completely fixed by the definition of abts, because a variable x is for instance in B[x, y]. – Blaisorblade Sep 11 '18 at 5:58

Just to clear something up that may not have been obvious, $\chi$ is a set and the notation $B[\chi, x]$ is meant to be ABTs under free variables that are either $x$ or are in $\chi$. In this notation I believe it is implied that $x \notin \chi$ when you write $B[\chi, x]$, which is important.
Using the definition of ABT above, you cannot prove for any $\chi$ that let(z, x.x) is in $B[\chi,x]$, but i claim that this is necessary to prove if you want to use it as the inner formula $a_1$ in let(y, x.$a_1$).
The reason you cannot prove let(z, x.x) is in $B[\chi,x]$ is because using the rule#1 stated above, the free variable $x$ is only an ABT in $B[\chi]$ when $x \in \chi$ (or alternatively: $x$ is only an ABT in $B[\chi',x]$ for some $\chi'$), but then using rule#2, we deduce $z \in B[\chi] \wedge x \in B[\chi, x] \rightarrow let[z,x.x] \in B[\chi]$. As I had mentioned in the first paragraph, this implies $x \notin \chi$, which means that the formula let(z, x.x) is ONLY in ABTs where $x$ is not a free variable.
The reason why $x$ needs to be free in this inner formula is because otherwise we cant apply rule#2 again on the outer formula let(y, x.$a_1$).
• Are you sure this is what is meant? You are saying that a binding tree over variables $\mathcal{X}$ is not also a binding tree over variables $\mathcal{X} \cup \mathcal{Y}\$ for any set of variables $\mathcal{Y}$. To me this 'weakening' rule seems quite natural. The lambda term $\lambda y.\lambda x.x$ springs to mind. The book seems to neither support or refute that this holds of abt's though. If you're certain, I am willing to accept your answer. – afsmi Nov 24 '16 at 3:03