Ординалы замыкания для индуктивных типов с функциональными пространствами

Функторы, построенные из конечных произведений и сумм, имеют порядковый номер замыкания $\omega$подробно описанный в этой рукописи Франсуа Метайера. т.е. мы можем достичь индуктивного типа$nat := \mu X. 1 + X$ перебирая функтор $1 + X$, которая достигает своей фиксированной точки после $\omega$ итераций.

Но как только мы допускаем постоянное возведение в степень, такое как в $\mu X. 1 + X + (nat \rightarrow X)$, тогда $\omega$ не достаточно

Я ищу результаты, которые включают возведение в степень. Какие порядковые номера достаточно?

Особенно ценится ссылка, которая представляет доказательство того, что такие функторы $\alpha$-прерывно для некоторого порядкового $\alpha$ как в приведенной выше рукописи.

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)$$ Как вы отметили в своем ответе, каждый $O_n$можно считать внутренне быть$n$регулярный кардинал вашей системы. В теории множеств этот тип данных может быть представлен действительным порядковым номером и соответственно огромен.

Однако такие конструкции могут быть добавлены к некоторой версии теории типов, и возникает вопрос: какой порядковый номер необходим для того, чтобы дать теоретико-множественную интерпретацию этой конструкции? Теперь, если мы ограничимся конструктивной семантикой, естественной идеей будет попытка интерпретировать каждый тип с помощью набора «реализаторов» этого типа, который является подмножеством набора$\lambda$-термины или, что эквивалентно, натуральные числа $\mathbb{N}$,

В этом случае легко показать, что порядковый номер исчисляется для любого $O_n$Но этот ординал растет очень быстро. Как быстро? Опять же, это зависит от степени свободы, которую вы имеете при попытке создать функции. Теория построения таких ординалов описана в теории больших счетных ординалов, о которой Википедия , к удивлению, может многое сказать. В общем, легко показать, что рассматриваемые ординалы меньше, чем ординал Черча-Клини , если вы не допускаете неконструктивных средств построения функций (скажем,$Beaver(n)$ который вычисляет число занятых бобров для машин с $n$ состояния).

Хотя это мало что говорит, за исключением того, что в конструктивной теории вам нужны только конструктивные ординалы для построения интерпретаций. Хотя, есть еще что сказать. Во-первых, Тьерри Кокванд предлагает очень хорошую презентацию, в которой подробно говорится , что в отсутствие элиминатора для всех других типов, кроме$nat$Вы можете построить $O_1$ в точности $\epsilon_0$ шаги.

В целом, похоже, существует соответствие между логической силой теории типов и размером наибольшего порядкового числа, которое она может представлять таким образом. Это соответствие является предметом Порядкового Анализа , который подробно изучался с конца 60-х годов и до сих пор изучается (с некоторыми удивительными открытыми вопросами). Предупреждение: предмет настолько же технический, насколько и увлекательный.

Надеюсь это поможет.

Я думаю, что нашел ответ, который работает в категориях, достаточно похожих на Set. Это теорема 3.1.12 в Начальных алгебрах и терминальных коалгебрах: обзор Адамека, Милиуса и Мосса.

Ответ заключается в том, что для всех таких функторов не хватает ни одного порядкового номера. Они становятся сколь угодно большими.

Точнее, для $F(X) = C_0\times(A_0 \rightarrow X) + C_1\times(A_1 \rightarrow X)\;+\;...\;+\; C_n\times(A_n \rightarrow X)$ответ является первым регулярным порядковым номером, большим, чем все$A_i$, Мы говорим$\alpha$ регулярно, если для всех $\beta < \alpha$, все $\beta$-индексированные цепочки ординалов < $\alpha$ иметь превосходство < $\alpha$, Грубо говоря,$\alpha$ не достижимо из меньшей цепочки меньших порядковых чисел.

Ключевым результатом является то, что для $\alpha$ регулярный порядковый, обоснованный $\alpha$ветвящиеся деревья имеют трансфинитную глубину < $\alpha$,

Неформально это я понимаю как любой $f : A_k \rightarrow F^\alpha(0)$ (т.е. $f : A_k \rightarrow \bigcup_{i<\alpha} F^i(0)$) "вписывается в" $A_k \rightarrow F^j(0)$ где $j := \mathrm{sup}_{(a:A_k)} \text{``the i such that }f(a) \text{ fits into } F^i(0)"$, Который$j < \alpha$ держит именно потому, что $\alpha$ регулярно и $|A_k| < \alpha$,

Так $(A_k \rightarrow \bigcup_{i<\alpha}F^i(0)) \subseteq \bigcup_{j<\alpha} (A_k \rightarrow F^j(0))$ для каждого $k$,

Так распространяя это через $+$с и $\times$у нас есть: $F(F^\alpha(0)) \subseteq \bigcup_{j<\alpha}F(F^j(0)) = \bigcup_{j<\alpha}F^j(0) = F^\alpha(0)$и поэтому он достиг фиксированной точки в $\alpha$,

Мне не совсем понятно, как обобщить этот аргумент за пределы Set, хотя. Как мы берем$A_k$индексированные колимиты?