Le MLTT est-il effectivement pCiC sans Prop?

11

La théorie du type de Martin-Löf est-elle fondamentalement le calcul prédicatif des constructions inductives sans imprédicatif ?Prop

S'ils sont étroitement liés mais avec plus de différences que simplement , quelles sont ces différences?Prop

type-theory calculus-of-constructions utilisateur
la source
Dans mon livre, MLTT est une théorie de type dépendante intuitioniste (ancienne et établie), tandis que j'associe le calcul des constructions à l'assistant de preuve Coq. Mais je peux me tromper.
Thomas Klimpel
1
MLTT utilise des types d'identité pour gérer l'égalité. Quelle serait l'égalité dans le fragment prédicatif du CiC?
Martin Berger
2
@MartinBerger: CiC a aussi des types d'identité!
cody
1
C'est un peu comme demander si le Royaume-Uni est l'UE sans les 27 autres États membres :-)
Andrej Bauer
3
@AndrejBauer Si j'étais assez spirituel, je proposerais une blague brexit, mais malheureusement je ne le suis pas. :-P
utilisateur

Réponses:

17

La réponse courte est oui, MLTT peut raisonnablement être assimilé à CIC sans imprédicatif Prop.

Le principal problème technique est qu'il existe des dizaines de variantes lorsque l'on parle de la théorie des types de Martin-Löf et, peut-être plus surprenant, lorsque l'on parle de CIC. Par exemple, en prenant la version de CIC définie dans la thèse de Benjamin Werner, cela n'a même pas de sens de la supprimer Prop, car on n'a ni l'un ni l'autre des Setunivers Type.

Les principales variations que l'on peut considérer dans l'une ou l'autre de ces théories sont:

  1. Univers : combien et comment sont-ils définis (Palmgren, On Universes in Type Theory , discute de nombreuses variations inégales), et si le polymorphisme de l'univers est admis ou non .

  2. Quels types / familles inductifs: Agda admet les types inductifs-récursifs, mais il existe de nombreuses variantes plus banales en fonction de la taille des types dans les constructeurs et les éliminateurs, en gérant les paramètres par rapport aux indices, etc.

  3. Injectivité des constructeurs de types . Cela conduit à un système incompatible avec EM dans Agda. Bien sûr, Epigram a une "théorie du type observationnelle" plus extrême, mais cela peut être considéré comme quelque chose de complètement différent.

  4. Axiom K : cela vient gratuitement avec certaines versions de correspondance de modèle dépendante.

  5. Γ⊢t:IdType A BΓ⊢A = B

  6. La présence de types coinductifs et des principes d'élimination associés.

Toutes les variations ci-dessus (sauf OTT) ont été prises en compte dans la littérature et associées au nom "Martin-Löf Type Theory" ou "Calculus of Inductive Constructions", principalement en raison de leur association avec les systèmes Agda et Coq, respectivement.

La réponse longue est donc qu'il n'y a pas de consensus sur la définition exacte de l'un ou l'autre de ces systèmes.

cody
la source