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

10

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.

jmite
la source
7
Les algorithmes de vérification de type bidirectionnels habituels ne tentent jamais de normaliser un terme (ou un type) sans d'abord vérifier qu'il est bien typé (ou bien formé). Vous n'avez pas à vous soucier de normaliser les termes non typés.
Andrej Bauer
7
Concernant l'application des règles: toutes les règles de terme et de type diminuent l'objectif, à l'exception de la conversion de type. Nous devons donc contrôler la conversion de type, ce que nous faisons en utilisant une approche bidirectionnelle.
Andrej Bauer

Réponses:

9

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):

DΓt:ADΓA:ssutBΔDΔ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 !DD 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ΓA,sΓt:AΓ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à.

cody
la source
J'ai trouvé votre réponse très utile, merci. J'ai deux questions: 1. Que signifie «systèmes opérationnels»? Quelle est l'alternative? 2. Pouvez-vous être plus explicite sur l'exemple: ce que cela signifie (quel fait essayons-nous de prouver?) "Les systèmes avec conversion typée sont équivalents à ceux avec conversion non typée."? Merci!
Łukasz Lew
1
@ ŁukaszLew L'alternative à un système opérationnel (implémenté dans la pratique par exemple dans le logiciel Coq ou Agda) serait un système théorique, qui est utile pour prouver les propriétés méta-théoriques, mais est inefficace ou peu pratique à utiliser dans la pratique. Prouver l'équivalence d'un système opérationnel et d'un système théorique est souvent un élément important de la conception d'un système. J'en parle plus ici: cstheory.stackexchange.com/a/41457/3984
cody
Je pense qu'il vaut la peine de mentionner Plus simple, plus facile de Lennart Augustsson ! . Il s'agit d'une implémentation Haskell minimale de la vérification de type et d'une certaine inférence pour le calcul lambda typé de manière dépendante. Il y a un code qui correspond étroitement à celui de Cody infer(t u):; pour le trouver, recherchez " tCheck r (App f a) =". Pour une implémentation plus complète mais toujours simple, vous pouvez vérifier celle de MortetypeWith .
Łukasz Lew
1
@ ŁukaszLew Le problème de conversion typé vs non typé est une question ouverte bien connue qui concerne 2 formulations de théories de types, et a été résolue assez récemment: pauillac.inria.fr/~herbelin/articles/…
cody
Que signifie ? ut
jonaprieto