# Inductively Defined Family of Sets

Suppose I am given the following inductive definition$^1$: Let $T$ be the smallest family of sets $\{T_1,T_2,T_3,\ldots\}$ such that

1. $0 \leq k < n \Rightarrow k \in T_n$
2. $t_1 \in T_n \wedge n > 0 \Rightarrow \lambda.t_1 \in T_{n - 1}$
3. $t_1 \in T_n \wedge t_2 \in T_n \Rightarrow (t_1 ~ t_2) \in T_n$

The elements of $T_n$ are the nameless $\lambda$-terms (with de Bruijn indices) with at most $n$ free variables numbered between 0 and $n - 1$. I want to express $T$ inductively, but am having trouble. In particular, I'm not sure how to express (2) and (3). For instance, suppose I try to define the set $T_{n + 1}$ in terms of $T_n$ for (2): in order to define $T_{n + 1}$, I need to know which elements occur in $T_{n + 2}$. For (3), in order to define $T_{n + 1}$, I need to know which elements occur in $T_{n + 1}$. I am being led in circles!

I don't understand the underlying principle which would permit me to define the family of sets $T$, because it's not a straightforward inductive definition. I assume the answer lies in defining mutually recursive sets, then finding their union. However, I'm stuck. Can anyone enlighten me?

1. Pierce, Types and Programming Languages, 6.1.2.
-
The inductive definition of $T$ has been given to you... it's exactly those 3 rules. – Tom Crockett Jan 8 '11 at 9:05
I understand that $T$ has been defined inductively; what I don't understand how to define $T_{n + 1}$ in terms of $T_n$. I'm probably just missing something fundamental, though. – danportin Jan 8 '11 at 20:11

First note that this problem is given in the context of some larger set $S$ that already satisfies the required properties. In this case, the "smallest" $T$ (should it exist) would mean a subset $T$ of $S$ satisfying these properties $\mathscr{P}$ such that every set $X \subseteq S$ having $\mathcal{P}$ has $T \subseteq S$. But the reason such a $T$ will exist is because we are implicitly given a well-defined procedure without choices of how to build up our $T$. Because of this fact, you can express the properties in a form that's equivalent and adheres to the more formal definition of induction, but this is unnecessary and can inhibit understanding.

To the more practical side of the matter, definitions like these fall into the "closure category" and often involve iterating steps infinitely many times starting with the emptyset and repeating iteratively until you've met all of the conditions (which is usually after an infinite number of steps). The intuition here is that if you've started with the empyset and added elements only as required by the definitions ("closing under the required properties"), then any elements that you added must always be contained in the "smallest" set. Many times, stepping through all of the Natural numbers will be sufficient.

Let's begin the procedure to get an idea. Here, you will be building up each of the $T_n$'s simultaneously as required by the conditions:

Start with $T_n = \emptyset$ for all $n \in \mathbb{N}$.

Step (1): After condition (1), $T_n = \{0, 1, \ldots, n-1\}$ for all $n$.

After condition (2), $T_n = \{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\}$.

After condition (3), $T_n = \{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\} \cup$ $\{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\} \times \{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\}$ (union of result from condition (2) and all possible ordered pairs from condition (2)).

Now start with result from Step (1), condition (3): $T_n = \{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\} \cup$ $\{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\} \times \{0, 1, \ldots, n-1, \lambda.0, \lambda.1, \ldots \lambda.n\}$ and repeat conditions (1) - (3) with this set instead of the emptyset for Step (2). Then plug in the final result from Step (2), and repeat conditions (1) - (3) with this set for Step (3). Keep repeating for each Natural number step. Of course condition (1) doesn't need to be repeated in this process because it won't add anything new.

If you continue this process of what is known as "closing under the operations" ad infinitum (all Natural numbers), you will wind up with the desired set. The reason for this is intuitively simple. Any terms $t_1$ and $t_2$ in the final set were added by some Natural number steps $m$ and $n$, say $n > m$ here. But then in step $n+1$, you make sure you've satisfied conditions (2) and (3) for any elements in the set so far constructed, including the elements $t_1$ and $t_2$.

-
Jason, you may want to replace your $T_n$ after condition (3) with the union of the $T_n$ you currently have, and the $T_n$ from after condition (2). – Andrés Caicedo Jan 9 '11 at 22:20
Yes, I definitely do. Thanks Andres. – Jason Jan 9 '11 at 22:34