Confusion about the definition of de Bruijn terms in the TAPL book 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
  
  
  $k \in \mathcal{T}_n$ whenever $0 \leq k &lt; n$;
  if $t_1 \in \mathcal{T}_n$ and $n &gt; 0$, then $\lambda.t_1 \in \mathcal{T}_{n-1}$;
  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:


The numbers $0, 1, \ldots, n-1$ are all terms in $\mathcal{T}_n$ (representing $n$ unbound variables).
$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?
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.