Consider the following free type definition:
$\text{Tree} := \text{leaf}\langle\!\langle\mathbb{N}\rangle\!\rangle\ |\ \text{branch}\langle\!\langle\text{Tree}\times\text{Tree}\rangle\!\rangle$
How can I tell, by looking at this definition, that there exists a set, $T$, and two injective functions, $l:\mathbb{N}\rightarrow T$, and $b:(T\times T)\rightarrow T$, such that
- $\text{Rng}(l)\cap\text{Rng}(b) = \emptyset$.
- Every $S \subseteq T$, such that $\text{Rng}(l) \subseteq S$, and such that $b[S\times S] \subseteq S$, coincides with $T$.
More generally, given a free type definition, how can I tell that there is a set and functions that are consistent with the definition?
Where can I read more about this topic?
Best Answer
Working in set theory, we can start by defining some concrete implementations of $l$ and $b$: $$ l(n) = \langle 0,n\rangle \qquad\qquad b(x,y) = \langle 1,\langle x,y\rangle\rangle $$ So far these are class functions -- we have not defined the domain of $b$ yet, but it is clear that a priori these expressions make sense for any domains whatsoever, and that their ranges will always be disjoint.
Now recursively define a sequence of sets $T_n$ by $$ \begin{align} T_0 ={}& \varnothing \\ T_{n+1} ={}& (\text{range of $l$ on $\mathbb N$}) \cup (\text{range of $r$ on $T_n\times T_n$}) \end{align} $$ and finally, using the axioms of replacement and union, set $$ T = \bigcup_{n\in\mathbb N} T_n $$
Now you can define $l$ and $r$ to have domains $\mathbb N$ and $T\times T$, and it is then straightforward to prove that $T$ has the properties you've listed.
Note that how this construction is derived completely mechanically from the original definition and can be easily generalized to other similar definitions. So you don't need to "look at the definition" particularly close to tell that there's a set that satisfies it, because every such definition can be run through the above procedure.
What makes this work is that all the set operations are increasing, such that if you apply them to a superset of what you had before, the result will be a superset of the result before. This holds for power sets, cartesian products, sequences, etc. -- but not for function spaces, because $X^{\{1,2,3\}}$ is not a superset of $X^{\{1,2\}}$.