Ordinaires de fermeture pour les types inductifs avec des espaces fonctionnels

Les foncteurs construits à partir de produits finis et de sommes ont l'ordinal de fermeture $\omega$ , bien détaillé dans ce manuscrit de François Metayer. dire que nous pouvons atteindre le type inductif $nat := \mu X. 1 + X$ en itérant le foncteur $1 + X$ , qui atteint son point fixe après $\omega$ itérations.

Mais une fois que nous permettons à exponentiation constante, comme dans $\mu X. 1 + X + (nat \rightarrow X)$ , alors $\omega$ ne suffit pas.

Je recherche des résultats qui incluent l'exponentiation. Quels types d'ordinaires suffisent?

Une référence particulièrement appréciée serait une référence qui prouve que de tels foncteurs sont $\alpha$ continus pour certains ordinaux $\alpha$comme dans le manuscrit ci-dessus.

La réponse à votre question dépend de plusieurs éléments, dont le plus important est la taille de vos espaces fonctionnels . Je vais t'expliquer. Définir O n + 1 = μ X . 1 + X + ( O n → X ) Comme vous l'avez noté dans votre réponse, chaque O n peut être considéré en interne comme le n- ème cardinal régulier de votre système. Dans la théorie des ensembles, ce type de données peut être représenté par un ordinal réel et est suffisamment grand.

$$O_0 = nat$$ $$O_{n+1} = \mu X.\ 1+X+(O_n\rightarrow X)$$ $O_n$$n$

Cependant, de telles constructions peuvent être ajoutées à une certaine version de la théorie des types, et la question devient: quel ordinal est nécessaire pour donner une interprétation théorique d'ensemble à cette construction? Maintenant , si nous nous limitons à constructive sémantique, une idée naturelle est d'essayer d'interpréter chaque type par l'ensemble des « » de ce réaliseurs type, qui est un sous - ensemble de l'ensemble de -termes, ou, les chiffres de manière équivalente naturels N .$\lambda$$\mathbb{N}$

Dans ce cas, il est facile de montrer que l'ordinal est dénombrable pour tout , mais que cet ordinal croît très rapidement. À quelle vitesse? Encore une fois, cela dépend de la liberté dont vous disposez lorsque vous essayez de créer des fonctions. La théorie de la construction de tels ordinaux est décrite dans la théorie des grands ordinaux dénombrables, dont Wikipedia a, étonnamment, beaucoup à dire. En général, il est facile de montrer que les ordinaux en question sont plus petits que l' ordinal de Church-Kleene , sauf si vous autorisez des moyens non constructifs de construire des fonctions (disons B e a v e r ( n ) qui calcule le nombre de castors occupés pour les machines avec $O_n$$Beaver(n)$$n$ États).

Cela ne veut pas dire grand-chose cependant, sauf que dans une théorie constructive, vous n'avez besoin que d'ordinaux constructifs pour construire des interprétations. Il y a cependant un peu plus à dire. Tout d'abord, il y a une très belle présentation de Thierry Coquand qui détaille qu'en l'absence d'un éliminateur pour tous les autres types mais $nat$ , vous pouvez construire en exactement ϵ 0 étapes.$O_1$$\epsilon_0$

En général, il semble y avoir une correspondance entre la force logique d'une théorie des types et la taille du plus grand ordinal qu'elle peut représenter de cette manière. Cette correspondance est le sujet de l' analyse ordinale , qui a été étudiée en détail depuis la fin des années 60, et qui est toujours à l'étude aujourd'hui (avec quelques questions ouvertes étonnantes). Attention cependant: le sujet est aussi technique que fascinant.

J'espère que cela t'aides.

Je pense que j'ai trouvé une réponse qui fonctionne dans des catégories suffisamment comme Set. C'est le théorème 3.1.12 des algèbres initiales et des houillères terminales: une étude d'Adamek, Milius et Moss.

La réponse est qu'aucun ordinal n'est suffisant pour tous ces foncteurs. Ils deviennent arbitrairement grands.

$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 < α α | A k | < $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$

Donc pour chaque .$(A_k \rightarrow \bigcup_{i<\alpha}F^i(0)) \subseteq \bigcup_{j<\alpha} (A_k \rightarrow F^j(0))$$k$

Donc, en étendant cela sur les s et s, nous avons: , et donc il a atteint le point fixe à .× F ( F α ( 0 ) ) ⊆ ⋃ j < α F ( F j ( 0 ) ) = ⋃ j < α F j ( 0 ) = F α ( 0 ) $+$$\times$$F(F^\alpha(0)) \subseteq \bigcup_{j<\alpha}F(F^j(0)) = \bigcup_{j<\alpha}F^j(0) = F^\alpha(0)$$\alpha$

Cependant, je ne sais pas très bien comment généraliser cet argument au-delà de Set. Comment prenons-nous les indexés par A_k?$A_k$