Une simple preuve que la décidabilité de la typabilité dans le système F (

9

Supposons que nous ne connaissions pas le résultat de Joe B. Wells de 1994 selon lequel la typabilité et la vérification de type sont indécidables dans le système F (AKA ). Dans les calculs Lambda avec types de Barendregt (1992), j'ai trouvé une preuve due à Malecki 1989 que la vérification de type implique la typabilité. Ceci est dû au faitλ2

existe tel que M : σσM:σ

est équivalent à

(λxy.y)M:(αα)

(En effet, si un terme est typable dans le système F, tous ses sous-termes le sont.)

Y a-t-il une preuve simple dans l'autre sens? Autrement dit, une preuve que la typabilité implique une vérification de type dans le système F?

Petr Pudlák
la source

Réponses:

5

Pour autant que je sache, montrer que cette direction est la partie difficile de la preuve Wells! C'est du moins ce que Pawel (Urzyczyn) m'a expliqué il y a quelques années.

Apparemment, il n'est pas trop difficile de montrer que la vérification de type est indécidable; la partie difficile montre que cela implique une indécidabilité de la reconstruction de type! En effet, il y a des cas où le premier est indécidable et le second décidable: voir par exemple Dowek 1993.

cody
la source