Techniques de preuve pour montrer que la vérification du type dépendant est décidable

Je suis dans une situation où je dois montrer que la vérification de typage est décidable pour un calcul typé de manière dépendante sur lequel je travaille. Jusqu'à présent, j'ai pu prouver que le système est en train de normaliser fortement, et donc que l'égalité définitionnelle est décidable.

Dans de nombreuses références que j'ai lues, la décidabilité de la vérification typographique est répertoriée comme un corollaire d'une forte normalisation, et je le crois dans ces cas, mais je me demande comment on peut réellement montrer cela.

En particulier, je suis bloqué sur les points suivants:

• Le fait que des termes bien typés normalisent fortement ne signifie pas que l'algorithme ne bouclera pas indéfiniment sur des entrées mal typées
• Étant donné que les relations logiques sont généralement utilisées pour montrer une forte normalisation, il n'y a pas de métrique décroissante pratique à mesure que nous progressons les termes de vérification de typage. Donc, même si mes règles de type sont dirigées par la syntaxe, il n'y a aucune garantie que l'application des règles finira par se terminer.

Je me demande, est-ce que quelqu'un a une bonne référence à une preuve de décidabilité de la vérification typographique pour une langue typiquement dépendante? Si c'est un petit calcul de base, ça va. Tout ce qui traite des techniques de preuve pour montrer la décidabilité serait formidable.

Il y a en effet une subtilité ici, bien que les choses fonctionnent bien dans le cas de la vérification de type. Je vais écrire le problème ici, car il semble apparaître dans de nombreux sujets connexes, et essayer d'expliquer pourquoi les choses fonctionnent bien lors de la vérification de type dans une théorie de type dépendante "standard" (je serai délibérément vague, car ces problèmes ont tendance à surgir malgré tout):

${\cal D}$$\Gamma\vdash t:A$${\cal D}'$$\Gamma \vdash A:s$$s$$u\leq t$$B$$\Delta$$\cal D''$$\Delta\vdash u:B$

Ce joli fait est quelque peu difficile à prouver, et compensé par un contre-fait assez méchant:

Fait 2: En général, et ne sont pas des sous-dérivations de !$\cal D'$$\cal D''$ $\cal D$

Cela dépend un peu de la formulation précise de votre système de type, mais la plupart des systèmes "opérationnels" mis en œuvre dans la pratique satisfont au fait 2.

Cela signifie que vous ne pouvez pas "passer à des sous-termes" lorsque vous raisonnez par induction sur des dérivations, ou conclure que l'énoncé inductif est vrai sur le type de terme que vous essayez de prouver.

Ce fait vous mord assez durement lorsque vous essayez de prouver des déclarations apparemment innocentes, par exemple que les systèmes avec conversion typée sont équivalents à ceux avec une conversion non typée.

Cependant , dans le cas de l'inférence de type, vous pouvez donner un algorithme d'inférence de type et de tri simultané (le type du type) par induction sur la structure du terme, ce qui peut impliquer un algorithme dirigé par type comme le suggère Andrej. Pour un terme donné (et le contexte , vous échouez ou trouvez tel que et . Vous n'avez pas besoin d'utiliser l'hypothèse inductive pour trouver ce dernier dérivation, et ainsi en particulier vous évitez le problème expliqué ci-dessus.$t$$\Gamma$$A, s$$\Gamma\vdash t:A$$\Gamma\vdash A : s$

Le cas crucial (et le seul cas qui nécessite vraiment une conversion) est l'application:

infer(t u):
   type_t, sort_t <- infer(t)
   type_t' <- normalize(type_t)
   type_u, sort_u <- infer(u)
   type_u' <- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Chaque appel à normaliser a été fait en termes bien typés, car c'est l'invariant du infersuccès de.

Soit dit en passant, lors de sa mise en œuvre, Coq n'a pas de vérification de type décidable, car il normalise le corps des fixinstructions avant de tenter de les vérifier.

En tout cas, les bornes sur les formes normales de termes bien typés sont si astronomiques que le théorème de décidabilité est surtout académique à ce stade de toute façon. Dans la pratique, vous exécutez l'algorithme de vérification de type aussi longtemps que vous en avez la patience et essayez une autre route si elle n'est pas terminée d'ici là.