Théorie de type intuitioniste «minimale»?

Je suis surpris que les gens continuent d'ajouter de nouveaux types dans les théories de types, mais personne ne semble mentionner une théorie minimale (ou je ne la trouve pas). Je pensais que les mathaticiens aiment le minimum, n'est-ce pas?

Si je comprends bien, dans une théorie des types avec un imprédicatif Prop, l'abstraction λ et les types Π suffisent. En disant suffire, je veux dire qu'il pourrait être utilisé comme une logique intuitionniste. D'autres types peuvent être définis comme suit:

⊥ \overset{d e f}{=} Π α : P r o p . α \neg A \overset{d e f}{=} A \to ⊥ A \land B \overset{d e f}{=} Π C : P r o p . (A \to B \to C) \to C A \lor B \overset{d e f}{=} Π C : P r o p . (A \to C) \to (B \to C) \to C \exists_{X : S} (P (X)) \overset{ré e F}{=} Π α : P r o p . (Π X : S . P X \to α) \to α

$\bot \stackrel{def}{=} \Pi \alpha: Prop. \alpha \\ \neg A \stackrel{def}{=} A \to \bot \\ A \land B \stackrel{def}{=} \Pi C: Prop. (A \to B \to C) \to C \\ A \lor B \stackrel{def}{=} \Pi C: Prop. (A \to C) \to (B \to C) \to C \\ \exists_{x: S}(P(x)) \stackrel{def}{=} \Pi \alpha: Prop. (\Pi x: S. P x \to \alpha) \to \alpha \\$

Ma première question est, est-ce qu'ils ( λ, Π) suffisent vraiment? Ma deuxième question est, de quoi avons-nous besoin au minimum si nous n'avons pas d'imprédicatif Prop, comme dans le MLTT? Dans MLTT, Church / Scott / quel que soit l'encodage ne fonctionne pas.

Modifier: lié

type-theory dependent-types 盛安安
la source

Quel serait un type "minimal" resp. quelles propriétés aurait-elle, selon vous?

Raphael

Pouvoir prouver ce que Coq peut prouver? J'avoue ne pas avoir de réponse claire dans ma tête D:

盛安安

Mais j'ai entendu dire que Coq a ajouté le polymorphisme de l'univers, pour lequel le système minimal que j'ai proposé ne fonctionne évidemment pas. Qu'en est-il de «pouvoir prouver ce que le MLTT (au sens normal) peut prouver»? Je pensais que les types W pouvaient être simulés? Bien que je n'ai pas fait le tour de la tête en général.

盛安安

Attendez, il semble qu'avec l'imprédicatif, Propnous n'avons même pas besoin de l'égalité.

盛安安

Réponses:

Pour développer les clarifications de Gallais, une théorie des types avec Prop imprédicatif et des types dépendants peut être considérée comme un sous-système du calcul des constructions, généralement proche de la théorie des types de Church . La relation entre la théorie des types de Church et le CoC n'est pas si simple, mais a été explorée, notamment par l' excellent article de Geuvers .

Dans la plupart des cas, cependant, les systèmes peuvent être considérés comme équivalents. Alors en effet, vous pouvez vous en tirer avec très peu, en particulier si vous n'êtes pas intéressé par la logique classique, alors la seule chose dont vous avez vraiment besoin est un axiome de l'infini : il n'est pas prouvable en CoC que n'importe quel type ait plus d'un élément! Mais avec juste un axiome exprimant qu'un certain type est infini, disons un type de nombres naturels avec le principe d'induction et l'axiome , vous pouvez aller assez loin: la plupart des mathématiques de premier cycle peuvent être formalisées dans ce système (en quelque sorte, c'est difficile de faire certaines choses sans le milieu exclu). $0\neq 1$

Sans accessoire imprédicatif, vous avez besoin d'un peu plus de travail. Comme indiqué dans les commentaires, un système d'extension (un système avec une extensionnalité fonctionnelle dans la relation d'égalité) peut se débrouiller avec seulement et -types, , les types vides et unitaires et , et les types W. Dans le cadre intensionnel, ce n'est pas possible: vous avez besoin de beaucoup plus d'inductifs. Notez que pour construire des types W utiles, vous devez pouvoir créer des types par élimination sur comme ceci: $\Sigma$ $\Pi$ $\mathrm{Bool}$ $\bot$ $\top$ $\mathrm{Bool}$

je F b t h e n ⊤ e l s e ⊥

$\mathrm{if}\ b\ \mathrm{then}\ \top\ \mathrm{else}\ \bot$

Pour faire des méta-mathématiques, vous aurez probablement besoin d'au moins un univers (par exemple, pour construire un modèle de Heyting Arithmetic).

Tout cela semble beaucoup, et il est tentant de chercher un système plus simple qui n'a pas l'imprédicativité folle du CoC, mais qui reste relativement facile à écrire en quelques règles. Une récente tentative de le faire est le système décrit par Altenkirch et al . Ce n'est pas entièrement satisfaisant, car la vérification de la positivité requise pour la cohérence ne fait pas partie du système "en l'état". La méta-théorie doit encore être étoffée également. $\Pi\Sigma$

Un aperçu utile est l'article ZF est-il un hack? par Freek Wiedijk, qui compare en fait les nombres réels de tous ces systèmes (nombre de règles et d'axiomes).

cody
la source

Les types ils définissables dans ETT?

Σ

$\Sigma$

盛安安

En fait non, je pense que vous devez aussi les assumer. Mon erreur.

cody

Le problème avec les encodages de l'Église est que vous ne pouvez pas obtenir des principes d'induction pour vos types, ce qui signifie qu'ils sont à peu près inutiles lorsqu'il s'agit de prouver des déclarations à leur sujet.

En termes de minimalité du système, l'un des chemins mentionnés dans les commentaires consiste à utiliser des conteneurs et des types (W / M), mais ils sont plutôt extensionnels, ce qui n'est pas vraiment pratique à utiliser dans des systèmes comme Coq ou Agda.

$\Pi$ $\Sigma$ $\mu$ $\nu$

$\mu$ $\nu$

gallais
la source