Exemple de cas où la violation d'une condition de positivité stricte dans les types inductifs entraîne une incohérence

La plupart des systèmes typés dépendants ont des conditions de positivité strictes pour les types inductifs. Quelqu'un connaît-il un exemple où la violation de la condition entraîne une incohérence dans le système?

Il est en fait possible de relâcher une positivité stricte et de rester cohérent. Par exemple, il suffit d'avoir seulement une condition de positivité. Autrement dit, nous pouvons accepter des définitions de type comme

$$T \triangleq \mu\alpha. (\alpha \to 2) \to 2$$

où les variables de type récursif apparaissent à gauche d'un nombre pair de flèches et conservent leur cohérence.

Cependant, les théories autorisant ce type de type inductif n'ont pas de modèles de théorie des ensembles - vous ne pouvez pas interpréter les types comme des ensembles et des termes comme des éléments d'ensembles. Dans ce cas, nous disons que est isomorphe à son double ensemble de pouvoirs (c'est-à-dire ), et cela viole le théorème de Cantor .$T$$T \simeq \mathcal{P}(\mathcal{P}(T))$

Étant donné que les théories de type dépendant sont souvent utilisées pour formaliser les mathématiques, leurs concepteurs hésitent généralement à ajouter des principes qui ne sont pas compatibles avec une sémantique à ensemble théorique, même s'ils sont cohérents.

EDIT: J'ajoute cette édition en réponse à la question d'Andrej. Le type est cohérent si vous l'ajoutez (disons) à Agda; il n'y a aucun problème avec cela. Nous n'avons un problème que si nous combinons une positivité non stricte avec un milieu exclu.$T$

L'intuition pour savoir pourquoi est sûr est (OMI) mieux vue à travers la lentille de la paramétrie. Dans le système F, nous pouvons montrer en utilisant la paramétrie que pour tout foncteur définissable , le type est en effet un type inductif.$F$$\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$

Rappelons maintenant qu'un foncteur définissable est un opérateur de type , avec un opérateur satisfaisant aux conditions de fonctionnalité (c'est-à-dire et ).$F$$F : \ast \to \ast$

$$\mathrm{map} : \forall \alpha,\beta.\;(\alpha \to \beta) \to F\;\alpha \to F\;\beta$$ $\mathrm{map}\;id = id$$\mathrm{map}\;f\;\circ \mathrm{map}\;g = \mathrm{map}\;(f \circ g$

Maintenant, nous pouvons définir un opérateur de type pour le double ensemble de puissance

$$C = \lambda \alpha.\; (\alpha \to 2) \to 2$$

et parce que ne se produit que positivement, nous pouvons également définir un opérateur de carte pour cela:$\alpha$

$$map_C = \lambda f : \alpha \to \beta, a' : (\alpha \to 2) \to 2, k : \beta \to 2.\; a' \;(\lambda a:\alpha.\; k\;(f\;a))$$

Nous savons donc que est un type inductif légitime.$T = \mu C$