Confusion about the definition of de Bruijn terms in the TAPL book

Question

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the definition given:

Let $\mathcal{T}$ be the smallest family of sets $\{\mathcal{T}_0, \mathcal{T}_1, \mathcal{T}_2, \ldots \}$ such that

1. $k \in \mathcal{T}_n$ whenever $0 \leq k < n$;

2. if $t_1 \in \mathcal{T}_n$ and $n > 0$, then $\lambda.t_1 \in \mathcal{T}_{n-1}$;

3. if $t_i \in \mathcal{T}_n$ and $t_2 \in \mathcal{T}_n$, then $(t_1 t_2) \in \mathcal{T}_n$.

It further clarifies that the elements of $\mathcal{T}_n$ are terms with at most $n$ free variables, numbered between $0$ and $n-1$.

I think I understand the first two points, but the third is confusing me. Here's my understanding of what the points mean:

1. The numbers $0, 1, \ldots, n-1$ are all terms in $\mathcal{T}_n$ (representing $n$ unbound variables).

2. $t_1$ has at most $n$ free variables, and $\lambda. t_1$ binds a single variable ($0$), so it has at most $n-1$ free variables.

Assuming these are correct, my current feeling about point 3 is that $(t_1 t_2)$ should actually be in $\mathcal{T}_{2n}$, because the resultant term will have up to $2n$ free variables ($n$ each). I don't follow how $(t_1 t_2) \in \mathcal{T}_n$.

Could somebody help correct my understanding?

Answer 1

The $n$ isn't indexing how many references to variables there are, it's indexing how many free variables are able to be referred to.

You can think of $0,1,\dots,n-1$ as being variables $v_0,v_1,\dots,v_{n-1}$. A term in $\mathcal T_n$ is a term that is allowed to refer to variables $v_0$ through $v_{n-1}$. If you have two terms of $\mathcal T_n$, then each is allowed to use variables $v_0$ to $v_{n-1}$. If you combine them into a new compound term, i.e. $(t_1, t_2)$, then that compound term still only refers to/uses the free variables $v_0$ through $v_{n-1}$. A use of a free variable $v_{n+4}$ hasn't suddenly appeared.

In the $\lambda.t_1\in\mathcal T_{n-1}$ case, while $t_1$ can contain an instance of $n-1$, i.e. an occurrence of $v_{n-1}$, such an occurence doesn't refer to a free variable. It refers to the variable bound by the $\lambda$. (Or $v_0$ doesn't depending on the convention: de Bruijn levels vs de Bruijn indices.) You could describe this as $\mathcal T_n$ only allows occurrences of $v_m$ if $v_m$ is under at least $m-n+1$ lambdas. From this perspective, $(t_1,t_2)\in\mathcal T_n$ when $t_1,t_2\in\mathcal T_n$, is just saying that if all occurrences of $v_m$ in $t_1$ and $t_2$ occur under at least $m-n+1$ lambdas, then they still occur under at least $m-n+1$ lambdas in $(t_1,t_2)$ since we haven't added or removed any lambdas.

Answer 2

This is crucial:

It further clarifies that the elements of $\mathcal{T}_n$ are terms with at most $n$ free variables, numbered between $0$ and $n-1$.

Then, in the rest of your argument, you forgot the "numbered between $0$ and $n-1$" part.

Item 3 states that, if $t_1$ has its free variables among $\{0,\ldots,n-1\}$ and $t_2$ also has its free variables among $\{0,\ldots,n-1\}$, then $(t_1 t_2)$ has its free variables among $\{0,\ldots,n-1\}$.

So, your issue was that it is not enough to count the number of free variables in $t_1$ and $t_2$, since knowing only that we can only conclude that $(t_1t_2)$ doubles the number of free variables (at most). We need to remember that the free variables are actually the same.