# How to understand inductive definitions of recursive data types?

The problem was encountered when learning Computability Notes by Roberto Zunino (link), page 9 and 11. It seems as if it is a well-known issue and I don't need to specify the "canonical" meaning of the symbols used due to the context we are dealing with.

However, to my understanding, $\uplus$ is the disjoint symbol, e.g. $\{a\} \uplus \{b\} = \{\langle 0, a \rangle, \langle 1, b \rangle \}$, where $0$, $1$ are mark signs showing the disjointness. As for $\simeq$, there is no information given in the notes, I believe it would say an isomorphism.

So the question is "How to understand recursive set-theoretic equations?". Any reference books? I don't wish to bother Mr. Zunino if it is a common concept.

And the equations:

• the set of naturals, $\mathbf{1}$ is a singleton set $\{0\}$. $$\mathbb{N} \simeq \mathbf{1} \uplus \mathbb{N}$$
• the set of binary trees of naturals (information stored only at the leaves) represented as $$\mathbb{T} \simeq \mathbb{N} \uplus (\mathbb{T} \times \mathbb{T})$$
-
What does $\uplus$ denote? – Asaf Karagila Aug 13 '12 at 22:52
What does $\simeq$ denote? – William Aug 13 '12 at 22:59
Where did you encounter this, and what precisely are you asking? Some of this notation is used for multiple things, so you should clarify what you mean by it in this context. What is your definition of a (binary) tree? If we're to be able to help you, you should make things clearer for us. – Cameron Buie Aug 13 '12 at 23:16
Also please try to make the question self-contained. The title is a pitcher line, not a part of the actual question. – Asaf Karagila Aug 13 '12 at 23:40
To downvoters: I have tried to make the answer detailed enough to explain what the question is about. – Carl Mummert Aug 14 '12 at 12:10

I am having trouble loading the notes you linked to, but I believe you are seeing an example of an inductive definition. It doesn't really have anything to do with "set theory" and set theorists are unlikely to see it; it's much more common in constructive mathematics, particularly in type theory.

I will explain that by talking about $$\mathbb{N} \simeq \mathbf{1} \uplus \mathbb{N}$$

This makes sense with the definition of $\uplus$ you have given, if we take $\simeq$ just to mean that the the structure on the left is inductively defined with the rule on the right.

Start by thinking about the natural numbers as "the smallest set containing $1$ and closed under the successor operation". Given that, what would it mean for me to tell you a natural number? I could either tell you the number is $1$, or I could tell you it is a successor. If it is a successor, you can ask me "the successor of what?", and then I have to tell you another natural number - which itself could be $1$ or a successor.

To use a variation of formal definition above, when I tell you $1$, I would really tell you $\langle L, \mathbf{1}\rangle$, and if I know that $\tau$ is what I tell you for a natural number $k$, to tell you the successor of $k$ I would say $\langle R, \tau\rangle$. Here I want to use $L$ and $R$ so that the number $1$ doesn't get re-used as much.

Thus $2$ would be $\langle R, \langle L, \mathbf{1}\rangle \rangle$ and $3$ would be $\langle R, \langle R, \langle L, \mathbf{1}\rangle \rangle \rangle$. Thus a natural number is either $1$ or it is of them form $\langle R, \tau\rangle$ where $\tau$ represents a natural number, and this situation can be summarized by $\mathbb{N} \simeq \mathbf{1} \uplus \mathbb{N}$. (There is a slight quibble that $\mathbf{1}$ is a particular type, which can safely be ignored for now; just view $\mathbf{1}$ as some arbitrary starting symbol that is not a pair.)

Now consider $\mathbb{T} \simeq \mathbb{N} \uplus (\mathbb{T}\times\mathbb{T})$ as a code for a binary tree whose leaves are labeled with natural numbers. This says that, to tell you a tree (the thing on the left), I can tell you one of two things. I can tell you a natural number ($\mathbb{N}$) or I can tell you two trees ($\mathbb{T}\times\mathbb{T}$). The point of the $\uplus$ is that you can tell which one I have told; this is theoretically important in some cases. The terminology is that $\uplus$ represents the disjoint union of two types.

What if I wanted to label all the nodes of the tree with natural numbers, not just the leaves? That would be $$\mathbb{T}' \simeq \mathbb{N} \uplus (\mathbb{N}\times (\mathbb{T}'\times \mathbb{T}'))$$

So $\times$ means that I have to tell you both of the two things, while $\uplus$ means I have to tell you exactly one, and you can determine which option I took. (The extra parentheses in $\mathbb{N}\times(\mathbb{T}'\times\mathbb{T}')$ are formally necessary but don't really change anything).

In principle, we can think of a situation where I give you an object but you don't know which type it is. For example, if you say "give me a prime number or an odd number" and I give you $3$, you cannot tell which option I chose. But if $\mathbb{P}$ is the set of primes and $\mathbb{O}$ the set of odds, and I give you an element of $\mathbb{P}\uplus\mathbb{O}$, you can tell which I have given you. For example, $\langle L, 3\rangle$ is not the same as $\langle R, 3\rangle$.

The notation $\simeq$ thus gives a compact way to describe how a type is built up out of other types, and at the same time it gives a recipe for how to parse the new type in a computer program.

-
Hello Mr. Mummert, I am to say a late thank you for the effort and help you've made. God bless you! – MeadowMuffins Oct 4 '13 at 21:33