2
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Are you sure about $n-1$ being bound by the $\lambda$ in your example? I think the $\lambda$ actually binds the $0$ variable. That is $\lambda 0 1$ stands for $\lambda x.xy$, not $\lambda x.yx$. (+1 anyway) $\endgroup$ – chi Jun 26 '18 at 9:02
  • $\begingroup$ @chi It depends on whether you're using de Bruijn levels or de Bruijn indices as I mentioned. I agree that de Bruijn indices where the index counts from inside out is the more usual presentation. It just didn't seem to fit quite as nicely as de Bruijn levels for the flow of what I was saying, and it doesn't otherwise make much of a difference for what I was saying. $\endgroup$ – Derek Elkins Jun 26 '18 at 9:23
  • $\begingroup$ I see. I think TAPL, which is mentioned by the OP, uses the other convention. Hopefully the OP is not misled by this. $\endgroup$ – chi Jun 26 '18 at 9:33
  • $\begingroup$ Whether de Bruijn indices or levels are used cannot be discerned from the grammar itself, one has to look at how substitution is defined. $\endgroup$ – Andrej Bauer Jun 26 '18 at 14:33
  • $\begingroup$ I think I follow. So if we have terms $t_1 = \lambda . 1 0$ and $t_2 = 0 1$, then $t_1, t_2 \in \mathcal{T}_2$, and $t_1 t_2 = 1 0 1$? I'm inclined to say that the variable capture of $t_2$ is incorrect, but I'm having trouble putting my reasoning into words. Or is this definition only concerned about the syntax of the language? $\endgroup$ – MattDs17 Jun 26 '18 at 15:04
4
$\begingroup$

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.

$\endgroup$

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.