Yo! C'est probablement une question stupide, mais je ne l'ai jamais vu écrit explicitement si, par exemple, la décidabilité de la vérification de type est équivalente à la propriété de normalisation forte. Par conséquent, je pose cette question pour clarifier toutes les relations possibles entre la vérification de type, la typabilité et une forte normalisation.
Laissez-moi vous expliquer ma motivation. Pour les théories de type (je suis intentionnellement vague ici, mais je m'intéresse principalement aux théories de type dépendantes), une forte normalisation est utilisée pour prouver la décidabilité de la vérification de type. De l'autre côté, tous les systèmes typés que je connais qui ont l'une de ces propriétés ont également l'autre. Cependant, je n'ai jamais vu explicitement déclaré qu'une forte normalisation est équivalente à la décidabilité de la vérification de type.
De façon analogue, pour prouver la typabilité, une règle habituellement (peut-être toujours), réduit un terme à une forme normale. Cependant, il est connu que la typabilité n'est pas vraie pour les théories de type dépendantes, alors qu'une forte normalisation peut tenir.
Par décidabilité de la vérification de type, je veux dire que pour tout type donné , contexte et terme non typé , il est possible de décider en un nombre fini d'étapes si est vrai ou non.
Par décidabilité de la typabilité, je veux dire que pour tout terme donné non typé , il est possible de décider en un nombre fini d'étapes s'il existe un contexte et un type tels que est vrai.
1) Est-il vrai que la décidabilité de la vérification de type équivaut à ce que chaque terme soit fortement normalisable?
2) Plus généralement, quelle est la relation entre la décidabilité de la vérification de type, la typabilité et une forte normalisation? Lequel implique l'autre?
Merci d'avance.
ÉDITER
Étant donné l'insatisfaction concernant le niveau de généralité de ma question (que je n'étais pas au courant), je voudrais la limiter uniquement à Pure Type Systems. Bien sûr, des commentaires ou contre-exemples supplémentaires concernant d'autres théories de type seront d'une grande utilité.
la source
Réponses:
Je donnerai une réponse plus ciblée et technique à celle de Martin. Si nous nous intéressons aux théories de type dépendantes, aucune des deux directions n'est évidente, mais les deux sont généralement supposées tenir. Cependant la direction Decidable⇒ La normalisation est ouverte, je crois, même pour des systèmes relativement bien compris, bien que nous ayons des résultats partiels. Cette question explore certains des mêmes problèmes.
Plus techniquement: un bon cadre technique pour ces questions est le réglage de Pure Type Systems dans lequel la normalisation n'implique décidabilité la vérification de type. Le résultat est du folklore, mais non trivial, car il faut trouver une stratégie pour savoir quand appliquer la règle de conversion. La stratégie évidente consiste à normaliser les types inférés avant toutes les applications de la règle d'application. Il y a des subtilités même ici, où l'exactitude d'une stratégie naturelle (plus efficace) appelée report de l'expansion était ouverte depuis un certain temps, mais a été réglée depuis.
Il existe des systèmes de types normalisants mais indécidables, notamment le système avec des types d'intersection qui saisit exactement les termes de normalisation, et doit donc être indécidable (car sinon il pourrait être utilisé pour identifier les termes de normalisation). Il serait tentant de dire ici que le système est défectueux dans le sens où il n'est pas dirigé par type , c'est-à-dire que les termes ne contiennent pas suffisamment d'informations pour déterminer le type.
Maintenant l'inverse, qui suggérerait que les systèmes non normalisateurs sont indécidables, est loin d'être évident: il a même été ouvert pendant un certain temps pour le célèbreType:Type système de Martin-Löf! Ce cas a été résolu en donnant un exemple de combinateur de boucle, qui permet d'écrire des calculs arbitraires.
Cependant, le problème général reste ouvert pour les systèmes généraux de type pur, bien qu'il soit largement admis qu'il soit vrai, et certains résultats partiels ont été montrés dans ce sens, par exemple ici .
la source
(1) Faux. Exemple de compteur: Java, Scala, Haskell, ...
(2) Aucune relation générale ne tient, dépend vraiment des détails du système de langue / dactylographie. Il y a une exception: pour les langages sains et les systèmes de dactylographie, j'imagine que la décidabilité de l'inférence de type (que je suppose être ce que vous entendez par "typabilité") implique trivialement la vérification de type. Mais je ne serais pas surpris si l'on pouvait concocter un système fou où même cette implication ne tient pas.
la source