Complexité de l'inférence de type dans le calcul lambda simplement typé

Question

Une question similaire a été répondue ici: Le calcul lambda typé est-il simplement équivalent aux fonctions récursives primitives

Ce que je conclus des réponses, c'est que la complexité est celle des polynômes étendus, mais cela fait référence à ce qui peut être calculé dans le STLC, et non aux expressions de vérification de type dans le STLC.

Ce lien fournit un algorithme de vérification de type. On prétend que la vérification de type est un temps linéaire dans une réponse à cette question: Complexité de la vérification de type par rapport à la complexité de la normalisation

En outre, une enquête sur les algorithmes qui font l'inférence de type pour STLC, utilisant l'unification se produit ici, mais aucun résultat de complexité n'est donné.

Answer 1

L'inférence de type pour le calcul lambda simplement typé est complète pour le temps polynomial, comme expliqué avec élégance dans la section 1 du calcul lambda linéaire de Harry Mairson et de l'exhaustivité PTIME .

Pour être un peu plus précis, on entend ici par "inférence de type" le problème du calcul du type simple principal d'un terme lambda non typé. Il s'agit à proprement parler d'un problème fonctionnel ("Étant donné un terme$t$, calculer son type principal "), mais Mairson montre que le problème de décision correspondant (" Étant donné un terme $t$ et tapez $A$, est $A$ le principal type de $t$? ") est PTIME-difficile, par réduction du problème de valeur de circuit. Cela implique l'exhaustivité PTIME, car une inférence de type simple peut être effectuée efficacement en utilisant l'unification du premier ordre. De plus, le codage par Mairson du problème de valeur de circuit a la propriété que le les termes représentant des circuits booléens sont affines (variables utilisées au plus une fois), et dans la section 2 de l'article, il donne un autre codage qui produit des termes linéaires (variables utilisées exactement une fois). Ainsi, sa preuve implique l'exhaustivité PTIME de l'inférence de type simple même lorsqu'elle est restreinte aux termes lambda affines / linéaires.