Free variables as defined in TAPL seems wrong

Question

In "Types and Programming Languages" by Benjamin C. Pierce (WorldCat)

5.3.2 Definition: The set of free variables of a term t, written FV(t), is defined as follows:

FV(x) = {x}
FV(λx.t₁) = FV(t₁) \ {x}
FV(t₁ t₂) = FV(t₁) ∪ FV(t₂)

\ is relative complement

---

Based on above definition of free variables my understanding is

For

λx.x x is not free

For

(x y) x is free and y is free

For

(x λx.x) the first x is free and the second x is not free.

So x is both free and not free in (x λx.x).

Since x is both free and not free it seems the definition of free variables is wrong.

How should the definition be interpreted for (x λx.x)?

---

Side notes

These are here in case others are seeking specifics of why I ask this question but I think the question above is self contained.

---

FV(t) is used for substitution in 5.3.5 and so has a more specific context, I.e.

x ↦ s = λy.[x ↦ s]t₁     ​if y ≠ x and y ≠ FV(s)

---

My implementation is in Prolog and the terms are converted to an AST before being passed to fv/2.

AST

app(abs(var(x),var(x)),var(x))

Prolog code

fv(var(V),[V]) :- !.
fv(abs(var(Binder),T),FV) :-
    fv(T,FV0),
    ord_subtract(FV0,[Binder],FV), !.
fv(app(T1,T2),FV) :-
    fv(T1,FV1),
    fv(T2,FV2),
    ord_union(FV1,FV2,FV).

Example run

?- fv(app(abs(var(x),var(x)),var(x)),Vs).
Vs = [x].

The result of the code is that x is a free variable because app is done last and the second x is free.

---

In TAPL chapter 6 the book switches to De Bruijn index and so the question becomes pointless for the remainder of the book.

---

AFAIK there is no official implementation of FV(t) provided for the book. The code for Lambda Calculus from Pierce is here but uses De Bruijn index so no need for FV(t)

---

Nothing in the errata for the definition.

---

EDIT (01/30/2022)

"The Calculi of Lambda-Conversion" by Alonzo Church (pdf)

pp. 8-9

A formula is any finite sequence of primitive symbols. Certain formulas are distinguished as well-formed formulas, and each occurrence of a variable in a well-formed formula is distinguished as free or bound, in accordance with the following rules (1-4), which constitute a definition of these terms by recursion:

1. A variable x is a well-formed formula, and the occurrence of the variable x in this formula is free.
2. If F and A are well-formed, (FA) is well-formed, and an occurrence of a variable y in F is free or bound in (FA) according as it is free or bound in F, and an occurrence of a variable y in A is free or bound in (FA) according as it is free or bound in A.
3. If M is well-formed and contains at least one free occurrence of x, then (λxM) is well-formed, and an occurrence of a variable y, other than x, in (λxM) is free or bound in (λxM) according as it is free or bound in M. All occurrences of x in (λxM) are bound.
4. A formula is well-formed, and an occurrence of a variable in it is free, or is bound, only when this follows from 1-3.

The free variables of a formula are the variables which have at least one free occurrence in the formula. The bound variables of a formula are the variables which have at least one bound occurrence in the formula.

p. 14

A well-formed formula will be said to be in principal normal form if it is in normal form, and no variable is both a bound variable and free variable of it, and the first bound variable occurring in it (in the left-to-right order of the symbols which compose the formula) is the same as the first variable in alphabetical order which is not a free variable of it, and the variables which occur in it immediately following the symbol λ are, when taken in the order in which they occur in the formula, in alphabetical order, without repetitions, and without omissions except of variables which are free variables of the formula.

p. 15

7 III. Every well-formed formula has one of the three forms, x where x is a variable, or (FA), where F and A are well-formed, or (λxM), where M is well-formed and x is a free variable of M.

p. 58

17. THE CALCULUS OF λ-K-CONVERSION. The calculus of λ-K-conversion is obtained if a single change is made in the construction of the calculus of λ-conversion which appears in §§ 5,6: namely, in the definition of well-formed formula (§5) deleting the words "and contains at least one free occurrence of x" from the rule 3.

Answer 1

Since x is both free and not free it seems the definition of free variables is wrong.

Why? There is no rule that says that the sets of free and bound variables have to be disjoint. Nothing breaks if they share elements. It is perfectly legitimate for a variable to occur both free and bound as in your example, so naturally it will be part of both sets. The definition is correct, and the only one that makes sense if you don't want to restrict variables to never occur both free and bound.

Answer 2

Although you don't actually need to do this to define free variables, it helps to think about bound and free occurrences of a variable in a term. An occurrence of a variable $x$ is bound in a term $t$ if it's under a syntax node that binds $x$, and it's free otherwise. The free variables of a term are the ones that have a free occurrence. It doesn't matter whether they have bound occurrences as well.

For example, in the term $T_1 = (\lambda \color{blue}{x}. \color{blue}{x})$, both occurrences of $x$ are bound¹. This term has no free occurrences of any variables, so $\mathsf{FV}(T_1) = \varnothing$.
In $T_2 = \color{red}{x} (\lambda \color{blue}{x}. \color{blue}{x})$, the first (red) occurrence of $x$ is free and the other two (blue) are bound. Since $x$ has a free occurrence, $\mathsf{FV}(T_2) = \{\color{red}{x}\}$.
In $T_3 = \color{red}{x} \color{orange}{y} (\lambda \color{blue}{x}. (\lambda \color{magenta}{z}. \color{magenta}{z} \color{blue}{x}) (\lambda \color{cyan}{x}. \color{cyan}{x} \color{cyan}{x} \color{orange}{y}) \color{blue}{x})$, the first (red) occurrence of $x$ is free and both (orange) occurrences of $y$ are free, whereas the other occurrences (blue, cyan) of $x$ are bound (in two different scopes), and all the occurrences (magenta) of $z$ are bound. Since both $x$ and $y$ have free occurrences but $z$ doesn't, $\mathsf{FV}(T_3) = \{\color{red}{x}, \color{orange}{y}\}$.

It is common when discussing languages with variable binding to use the Barendregt convention. This convention states that in a given term, you never use the name of a free variable as the name of a bound variable. If you need to build a term from multiple parts that have bound variables, you alpha-convert them to rename those variables to be unique. When you obey this convention, in a given term, a variable never has both bound occurrences and free occurrences. If you take the examples above, they don't obey the Barendregt convention if you consider the letters ($x$, $y$, $z$) to be the variable names. But if you consider the letters and their colors to constitute the variable names, they do obey the Barendregt convention: I assigned each distinct variable a different color (“distinct” meaning that alpha-conversion can map them to different names).

¹ _{Depending on how you define “bound”, the occurrence just after the $\lambda$ might be defined as bound, or as binding but not bound. It's more common to consider it not bound when discussing languages where variable binding is simple, such as the lambda calculus, but defining binding occurrences to be bound makes it easier to analyze languages with more complex binding constructions such as pattern matching.}