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}$.

  • $\begingroup$ The incorrect definition incurs capture, whereas capture-avoiding substitution is generally regarded as a pillar of proper language design. $\endgroup$
    – gardenhead
    Nov 24 '16 at 17:48
  • $\begingroup$ @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. $\endgroup$
    – afsmi
    Nov 25 '16 at 2:27
  • $\begingroup$ 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]. $\endgroup$ 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$).

  • $\begingroup$ 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. $\endgroup$
    – afsmi
    Nov 24 '16 at 3:03
  • 1
    $\begingroup$ I can't say I'm certain, but the naming issue is the whole reason why your weakening rule doesn't exist. You can't say let(y, x.x) has a free variable x because it uses x and does not have a renaming rule. Your weakening rule would work for stipulations that there are no re-used variable names. Anyways I would need to re look through PFPL to be totally sure $\endgroup$ Nov 24 '16 at 3:24
  • $\begingroup$ Weakening is valid: if a is an abt in B[X], the free variables of a are a subset of X, but not necessarily all of X (see my comment cs.stackexchange.com/questions/66350/…). Tho this answer seems to suggest that weakening only fails for the “wrong” definition? $\endgroup$ Sep 11 '18 at 5:59

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.