Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.
share|improve this question
1  
The inductive definition of $T$ has been given to you... it's exactly those 3 rules. –  pelotom 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

1 Answer 1

up vote 2 down vote accepted

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$.

share|improve this answer
1  
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). –  Andres Caicedo Jan 9 '11 at 22:20
    
Yes, I definitely do. Thanks Andres. –  Jason Jan 9 '11 at 22:34

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.