Ramification d'une théorie de type imprédicative

La plupart des théories de type que je connais sont prédictives par lesquelles je veux dire que

Void : Prop
Void = (x : Prop) -> x

n'est pas bien typé dans la plupart des prouveurs de théorèmes car ce type pi appartient au même univers Propet ce n'est pas le cas Prop : Prop. Cela les rend prédictifs et interdit les définitions imprédicatives comme ci-dessus. Cependant, beaucoup de "langages de tableau noir" tels que le système F ou CoC sont en fait imprédicatifs. En fait, cette imprédicativité est vitale pour définir la plupart des constructions non incluses primitivement dans le langage.

Ma question est pourquoi voudrait-on renoncer à l'imprédicativité étant donné son pouvoir dans la définition de constructions logiques? J'ai entendu quelques personnes remarquer que l'imprédicativité gâche le "calcul" ou l '"induction" mais j'ai du mal à trouver une explication concrète.

lo.logic type-theory Daniel Gratzer
la source

Les théoriciens des types sont-ils prédictifs ou leurs théories?

Andrej Bauer

Je suppose que Coq n'est pas "la plupart des prouveurs de théorèmes" pour vous, car il accepte la définition ci-dessus.

Andrej Bauer

@AndrejBauer Pourquoi pas les deux? :) Je suppose que coq a un univers imprédicatif et prédictif. Je suppose que ma question est. "Pourquoi le jeu n'est-il pas aussi imprédicatif?" dans le cadre du coq

Daniel Gratzer

Pourquoi le type n'est-il pas imprédicatif? > Vérifier le type. Type: Tapez. Eh bien sacrément :)

cody

Pas besoin de déranger les développeurs! L'ensemble imprédicatif est assez méchant, et en particulier, il entre en conflit avec certains principes de choix plutôt naturels et le soi-disant «milieu exclu informatif» forall P : Type, {P} + {~P}, car cet ensemble + imprédicatif implique la pertinence de la preuve (et natn'est pas la preuve non pertinente). Voir par exemple coq.inria.fr/library/Coq.Logic.ClassicalUniqueChoice.html et coq.inria.fr/library/Coq.Logic.Berardi.html

cody

Réponses:

Je vais développer mes commentaires en réponse. Les origines de la théorie des types prédicative sont presque aussi anciennes que la théorie des types elle-même, car l'une des motivations de Russel était d'interdire les définitions "circulaires" qui étaient identifiées comme faisant partie de la source des incohérences et des paradoxes du XIXe siècle. Thierry Coquand donne ici un aperçu éclairé . Dans cette théorie, les prédicats sur un "niveau" ou type appartiennent aux types du niveau "suivant", où il existe un nombre infini (dénombrable) de niveaux.

Alors que la hiérarchie prédicative de Russel était (apparemment) suffisante pour écarter les paradoxes connus, elle s'est avérée très difficile à utiliser comme système fondateur. En particulier, définir quelque chose d'aussi simple que le système de nombres réels était extrêmement difficile, et Russel a donc postulé un axiome, l' Axiom of Reductibility qui a postulé que tous les niveaux étaient "réduits" à un. Il va sans dire que cette évolution n'a pas été satisfaisante.

Cependant, contrairement aux déclarations imprédicatives "nuisibles" (comme la compréhension sans restriction), cet axiome ne semble pas introduire d'incohérences. Les formulations subséquentes de théories fondamentales ( théorie des types simples , théorie des ensembles de Zermelo ) les ont acceptées en gros, faisant des familles de prédicats (quantifiant éventuellement sur tout l'univers des ensembles), des prédicats au même niveau.

Vers 1971, Martin-Löf a introduit la théorie des types dépendants dans laquelle ce principe et l'axiome ultérieur Type : Typetiennent. Ce système s'est révélé incohérent pour des raisons subtiles: le paradoxe naïf de Russel ne peut pas être joué (de manière simple), mais un encodage intelligent permet néanmoins de trouver une contradiction. Cela a provoqué une crise de foi similaire à celle de Russel, résultant en la théorie du type prédicatif avec des univers que nous connaissons et aimons.

Il existe un moyen de réparer la théorie pour permettre l'imprédicativité "innocente" à la théorie des ensembles de Zermelo, ce qui a donné lieu à des théories de type comme le calcul des constructions, mais le mal a été fait, et l '"école suédoise" de la théorie des types a tendance à rejeter l'imprédicativité.

Plusieurs points:

Qu'est-ce que cela a à voir avec les mathématiques intuitionnistes? La réponse n'est pas beaucoup. Au tournant du XXe siècle, les mathématiciens avaient tendance à confondre l'utilisation de principes circulaires / imprédicatifs avec un raisonnement non constructif (l'intuition étant que le raisonnement imprédicatif semble supposer un univers mathématique préexistant , tout comme les utilisations du milieu exclu). Cependant, il existe des théories imprédicatives parfaitement intuitionnistes (comme IZF ). Les personnes intéressées par l'intuitionnisme ont toujours tendance à s'intéresser au prédicativisme pour une raison quelconque (j'en suis bien sûr coupable).
Que pouvez- vous faire en mathématiques prédicatives? Comme Martin le souligne dans sa réponse, Hermann Weyl (à ne pas confondre avec Andre Weil) a lancé un programme qui tentait d'explorer le pouvoir expressif des systèmes prédicatifs, en prenant comme point de départ que les systèmes prédicatifs étaient d'une force expressive entre Peano Arithmetic et Second Order Arithmétique , qui est à peu près reconnue comme imprédicative par la plupart des normes (et est comparable au système F du côté de la théorie des types). Le programme a ensuite été surnommé «mathématiques inversées», car il tentait de classer la force des théorèmes mathématiques connus en termes d'axiomes nécessaires pour les prouver (l'inverse de l'approche habituelle). lela page wikipedia donne un bon aperçu; le programme a connu un certain succès, dans la mesure où la plupart des mathématiques du XIXe siècle peuvent facilement être hébergées dans des systèmes très faibles. Il reste à savoir si ce programme peut évoluer vers des résultats plus récents, disons, dans une théorie de catégorie supérieure (le soupçon est que la réponse est "oui, avec beaucoup d'efforts").

cody
la source

Votre bel article contient une remarque secondaire très intéressante: "est à peu près accepté comme imprédicatif par la plupart des normes ". Cela indique quelque chose de subtil, à savoir qu'il n'est pas clair où exactement la frontière entre prédicatif et imprédicatif doit être tracée.

Martin Berger

{P A}_{2}

$\mathrm{PA}_2$

Une dimension est l'inférence de type. L'inférence de type du système F par exemple n'est pas décidable, mais certains de ses fragments prédicatifs ont une inférence de type décidable (partielle).

Une autre dimension est la cohérence en tant que logique. Des penseurs éminents se sont toujours sentis un peu inquiets d'avoir des fondements imprédicatifs des mathématiques. Après tout, c'est une forme de raisonnement circulaire. Je pense que H. Weyl aurait pu être le premier ou l'un des premiers à avoir essayé de reconstruire autant de mathématiques que possible de manière prédicative ... juste pour être du bon côté. Nous avons appris que les circularités de l'imprédicativité ne sont pas problématiques en mathématiques classiques, en ce sens qu'aucune contradiction n'a jamais été dérivée des définitions imprédicatives «apprivoisées». Au fil du temps, nous avons appris à leur faire confiance. Notez que cette (absence de paradoxa) est un empiriqueobservation! Cependant, une grande partie du développement de la théorie de la preuve, avec ses constructions ordinales étranges, a pour objectif ultime le souhait de construire toutes les mathématiques «par le bas», c'est-à-dire sans définitions imprédicatives. Ce programme n'est pas terminé. Ces dernières années, l'intérêt pour les fondements prédictifs des mathématiques est passé des inquiétudes concernant le paradoxe au contenu informatique des preuves, ce qui est intéressant pour diverses raisons. Il s'avère que les définitions imprédicatives rendent difficile l'extraction du contenu informatique. Un autre angle dans le souci de cohérence vient de la tradition de Curry-Howard. La théorie de type originale de Martin-Löf était imprédicative ... et peu solide. À la suite de ce choc, il a proposé uniquement des systèmes prédictifs, mais combinés à des types de données inductifs pour regagner une grande partie du pouvoir de l'imprédicativité.

Martin Berger
la source

Pour être juste, Russel a été l'un des premiers à essayer . Il a en quelque sorte admis sa défaite (avec l'axiome de la réductibilité).

cody

@cody Je ne connais pas trop l'histoire de ces tentatives. Dans quelle mesure Weyl (et S. Feferman) ont-ils réussi dans leurs tentatives? MLTT / HOTT fonctionne certainement, je dirais.

Martin Berger

Fondamentalement, Weyl a connu un succès retentissant, c'est-à-dire que la plupart du corpus d'analyse peut être formalisé sans recours aux mathématiques du deuxième ordre (imprédicatives). Le corpus d'œuvres fait désormais partie des mathématiques inverses, qui quantifient précisément la quantité d '"imprédicativité" dont vous avez besoin.

cody

Ce n'est pas vrai que la théorie de la preuve peut "avec ses constructions ordinales étranges" construire toutes les mathématiques sans définitions imprédicatives. Le problème est que la théorie de la preuve ne se fait pas dans un vide, mais dans un système formel, qui aurait lui-même un ordinal de preuve-théorie qu'il est incapable de prouver bien fondé. Donc, cette poursuite ne peut certainement pas atteindre le «bas». Certains logiciens pensent que Γ [0] est le premier ordinal imprédicatif, et si c'est le cas, vous êtes coincé et ne pouvez pas justifier de façon prédictive ATR0. Sinon, vous devez justifier que Γ [0] est prédictif. Comment le feriez-vous?

user21820

@ user21820 Je n'ai pas dit que toutes les mathématiques peuvent être construites sans définitions imprédicatives, c'est une question ouverte.

Martin Berger

Les théories de type tendent vers la prédicativité principalement pour des raisons socio-techniques.

Premièrement, le concept informel d'imprédicativité peut être formalisé de (au moins) deux manières différentes. Premièrement, nous disons qu'une théorie de type comme le système F est imprédicative car la quantification de type peut s'étendre sur tous les types (y compris le type auquel le quantificateur appartient). Nous pouvons donc définir des opérateurs génériques d'identité et de composition:

\begin{array}{lclll} je ré & : & \forall une . une \to une & = & Λ une . λ X . X \\ c o m p o s e & : & \forall une, b, c . (une \to b) \to (b \to c) \to (une \to c) & = & Λ une, b, c . λ F, g . λ X . g (F X) \end{array}

$\begin{array}{lclll} \mathit{id} & : & \forall a.\; a \to a & = & \Lambda a.\;\lambda x.\;x\\ \mathit{compose} & : & \forall a, b, c.\; (a \to b) \to (b \to c) \to (a \to c) & = & \Lambda a,b,c.\lambda f, g. \lambda x. g(f\;x) \end{array}$

Cependant, notez que dans la théorie des ensembles standard (par exemple, ZFC), ces opérations ne peuvent pas être définies en tant qu'objets . Il n'existe pas de "fonction d'identité" dans la théorie des ensembles, car une fonction est une relation entre un ensemble de domaines et un ensemble de domaines de codage, et si une seule fonction peut être la fonction d'identité, vous pouvez l'utiliser pour construire un ensemble de tous les ensembles. (C'est essentiellement ainsi que John Reynolds a montré que le polymorphisme de style System-F n'avait pas de modèles de théorie des ensembles.)

$X$ $S$ $P$ $X$ $P$ $X$

L'imprédicativité de style F est donc incompatible avec une vision naïve des types en tant qu'ensembles. Si vous utilisez la théorie des types comme assistant de preuve, il est agréable de pouvoir facilement transférer des mathématiques standard vers votre outil, et donc la plupart des personnes implémentant de tels systèmes suppriment simplement l'imprédicativité. De cette façon, tout a à la fois une lecture théorique et une théorie des types, et vous pouvez interpréter les types de la manière qui vous convient le mieux.

Neel Krishnaswami
la source

N

$\mathbb{N}$

N

$\mathbb{N}$