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

9

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?

Konstantin Solomatov
la source

Réponses:

10

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μα.(α2)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 .TTP(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μFα.(Fαα)α

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 ).FF:

map:α,β.(αβ)FαFβ
mapid=idmapfmapg=map(fg

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

C=λα.(α2)2

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

mapC=λf:αβ,a:(α2)2,k:β2.a(λa:α.k(fa))

Nous savons donc que est un type inductif légitime.T=μC

Neel Krishnaswami
la source
Pouvons-nous trouver un exemple qui crée une incohérence à lui tout seul? Votre exemple est incohérent si nous supposons également (assez) le milieu exclu.
Andrej Bauer
Une autre raison est que nous pouvons ajouter le théorème FAN à Agda, après quoi nous pouvons prouver que le type en question est (isomorphe) aux nombres naturels.
Andrej Bauer
Je pense devrait être assez mauvais. μα.(α2)α
Andrej Bauer
1
Ah, j'ai mal compris la question - le fait est que la positivité stricte est une condition suffisante mais pas nécessaire. Votre exemple (avec une occurrence négative réelle) est incohérent.
Neel Krishnaswami
Ouais, je viens de réaliser ça. Mon exemple ne tient pas la route.
Andrej Bauer