Closure ordinals for inductive types with function spaces

Question

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by iterating the functor $1 + X$, which reaches its fixed point after $\omega$ iterations.

But once we allow constant exponentiation, such as in $\mu X. 1 + X + (nat \rightarrow X)$, then $\omega$ isn't enough.

I'm looking for results that include exponentiation. What kind of ordinals are sufficient?

Especially appreciated would be a reference that presents a proof that such functors are $\alpha$-continuous for some ordinal $\alpha$ like in the above manuscript.

Answer 1

The answer to your question depends on several things, the most important of which is the size of your function spaces. I'll explain. Define $$O_0 = nat $$ $$O_{n+1} = \mu X.\ 1+X+(O_n\rightarrow X)$$ As you noted in your answer, each $O_n$ can be considered internally to be the $n$-th regular cardinal of your system. In set theory, this datatype can be represented by an actual ordinal and is appropriately huge.

However, such constructions may be added to some version of type theory, and the question becomes: what ordinal is needed to give a set-theoretic interpretation to this construct? Now if we restrict ourselves to constructive semantics, a natural idea is to try to interpret each type by the set of "realizers" of this type, which is a subset of the set of $\lambda$-terms, or equivalently, the natural numbers $\mathbb{N}$.

In this case, it is easy to show that the ordinal is countable for any $O_n$, but that this ordinal grows very quickly. How quickly? Again, this depends on the amount of freedom you have when trying to build functions. The theory to building such ordinals is described in the theory of Large Countable Ordinals, of which Wikipedia has, surprisingly, a lot to say. In general it is easy to show that the ordinals in question are smaller than the Church-Kleene Ordinal, unless you allow non-constructive means of building functions (say $Beaver(n)$ that computes the busy beaver number for machines with $n$ states).

This isn't saying much though, except that in a constructive theory, you only require constructive ordinals to build interpretations. There is a bit more to say though. First, there is a very nice presentation by Thierry Coquand that details that in the absence of an eliminator for all other types but $nat$, you can build $O_1$ in exactly $\epsilon_0$ steps.

In general there seems to be a correspondence between the logical strength of a type theory, and the size of the largest ordinal that it can represent in this manner. This correspondence is the subject matter of Ordinal Analysis, which has been studied at great length since the late sixties, and is still under study today (with some amazing open questions). Warning though: the subject matter is as technical as it is fascinating.

Hope this helps.

Answer 2

I think I've found an answer that works in categories sufficiently like Set. It's theorem 3.1.12 in Initial algebras and terminal coalgebras: a survey by Adamek, Milius, and Moss.

The answer is that no one ordinal is sufficient for all such functors. They get arbitrarily large.

More precisely, for $F(X) = C_0\times(A_0 \rightarrow X) + C_1\times(A_1 \rightarrow X)\;+\;...\;+\; C_n\times(A_n \rightarrow X)$, the answer is the first regular ordinal larger than all the $A_i$. We say $\alpha$ is regular if for all $\beta < \alpha$, all $\beta$-indexed chains of ordinals < $\alpha$ have a supremum < $\alpha$. Roughly, $\alpha$ is not reachable from a smaller chain of smaller ordinals.

The key result is that for $\alpha$ a regular ordinal, the well-founded $\alpha$-branching trees have transfinite depth < $\alpha$.

Informally, I understand it as any $f : A_k \rightarrow F^\alpha(0)$ (i.e. $f : A_k \rightarrow \bigcup_{i<\alpha} F^i(0)$) "fits into" $A_k \rightarrow F^j(0)$ where $j := \mathrm{sup}_{(a:A_k)} \text{``the i such that }f(a) \text{ fits into } F^i(0)"$. That $j < \alpha$ holds is precisely because $\alpha$ is regular and $|A_k| < \alpha$.

So $(A_k \rightarrow \bigcup_{i<\alpha}F^i(0)) \subseteq \bigcup_{j<\alpha} (A_k \rightarrow F^j(0))$ for each $k$.

So extending this across the $+$s and $\times$s, we have: $F(F^\alpha(0)) \subseteq \bigcup_{j<\alpha}F(F^j(0)) = \bigcup_{j<\alpha}F^j(0) = F^\alpha(0)$, and so it's reached the fixed point at $\alpha$.

It's not quite clear to me how to generalize this argument beyond Set though. How do we take $A_k$-indexed colimits?