Décidabilité de l'inférence de type et de la vérification de type dans MLTT

Dans Une théorie intuitioniste des types de Martin-Löf : partie prédicative, il est prouvé que la vérification de type est décidable sous réserve d' être typable en premier lieu, en prouvant un théorème de normalisation pour les termes typables fermés. D'un autre côté, je l'ai vu écrit à plusieurs endroits (Wikipedia, Nördstrom, etc.) que la vérification de type (intensionnelle) MLTT est décidable; restreignent-ils implicitement les termes typables? $a \colon A$ $a$
Sait-on quelque chose sur la décidabilité de l'inférence de type ou de la vérification de type dans le MLTT intensionnel si nous ne nous limitons pas aux termes typables? Par exemple, il existe peut-être un processus de décision qui reconnaît les termes non typables, par exemple en se normalisant à une forme qui ne correspond à aucun des constructeurs, ou en montrant qu'il n'y a pas de séquence non périodique de réductions pour un terme non typable.

Je n'ai pas pu trouver grand chose dans la littérature.

reference-request type-theory type-inference Josh Chen
la source

Réponses:

Certes, le problème de décision

$a$ $A$ $\vdash a :A$

$\vdash a\ :\ ?$ $a$

$\Gamma\vdash a\ :\ ?$

$a$

Par conséquent, la normalisation de termes bien typés est une condition nécessaire pour que le problème d'inférence de type soit décidable.

Vous voudrez peut-être vérifier Nordström, Petersson et Smith pour une introduction.

Je ne connais aucune description générique d'un algorithme d'inférence de type pour normaliser les théories de type, bien que Pollack donne une assez bonne vue d'ensemble (bien que l'état de l'art se soit amélioré) dans Typechecking in Pure Type Systems .

cody
la source

Qu'en est-il des prétypes (termes désignant prétendument un type)? Il pourrait également être utile de clarifier leur statut.

Andrej Bauer

Merci cody, faites-vous référence aux algorithmes de vérification de type mis en œuvre par les assistants de preuve comme ALF et Coq? À ma connaissance, ce sont des algorithmes pour les variantes spécifiques de MLTT sur lesquelles ils sont basés (CIC pour Coq, autre chose pour ALF), mais je ne sais pas comment ils peuvent être utilisés pour taper le type spécifique de MLTT de '73. En particulier, si la hiérarchie de l'univers ou d'autres différences de détail peuvent changer quoi que ce soit ...

Josh Chen

... Ou les algorithmes sont-ils suffisamment généraux pour couvrir ces différences? J'ai du mal à trouver des résultats dans une telle généralité; tout ce que je semble trouver dans ma recherche documentaire, ce sont des résultats très spécifiques, souvent particulièrement adaptés à la théorie sous-jacente d'un assistant de preuve.

Josh Chen

@JoshChen les algorithmes sont à leur base très généraux, car ils impliquent une recherche par type, alternant avec des étapes de normalisation sur des termes bien typés, comme l'a expliqué Andrej. Je ne connais pas de description générique de l'algorithme, malheureusement, bien que j'ajouterai une référence partielle à ma réponse.

cody

@JoshChen Ils ne clarifient pas, mais ils peuvent faire référence à des types d'inférence pour des termes de "style curry", pour lesquels l'inférence est indécidable. J'entre

cody

Je voudrais compléter la réponse par cody par une observation générale transmettant ma compréhension des raisons pour lesquelles les algorithmes de vérification de type fonctionnent.

Pour une large classe de théories de types, la vérification ou l'inférence de type est effectuée de telle manière que nous n'essayons jamais de normaliser un terme, à moins d'avoir établi au préalable qu'il est bien typé. De même, nous n'essayons jamais de normaliser un type, sauf si nous avons déjà établi qu'il s'agit d'un type. Pour cette raison, nous pouvons être sûrs que la normalisation prendra fin (ce qui nécessite une preuve distincte).

Il faut regarder des algorithmes spécifiques et voir qu'ils fonctionnent vraiment de cette façon, mais ils le font. Je voulais juste dire ce qui les fait vibrer. Ou mieux, c'est la raison pour laquelle ils arrêtent de cocher.

Andrej Bauer
la source