Existe-t-il une bonne notion de non-terminaison et d'arrêt des preuves dans la théorie des types?

La théorie des types constructifs avec son interprétation de base sous la correspondance de curry howard consiste uniquement en fonctions calculables totales. Dans la littérature, certains ont dit que l'utilisation de la "théorie du type informatique" pour représenter la non-terminaison dans les programmes fonctionnels, mais dans les articles que j'ai rencontrés, cela ne semble pas être la principale motivation de la théorie (par exemple Benton mentionne le non-déterminisme, les continuations et les exceptions, sans entrer dans les détails sur la non-terminaison), donc je n'ai pas encore trouvé de document donnant une interprétation robuste de la non-terminaison en utilisant la théorie du type informatique.

Plus précisément, ce que je recherche, c'est un moyen qui, étant donné un type représentant un calcul éventuellement non final de type , T ( A ) , il devrait y avoir une certaine notion de preuves que x : T ( A ) se termine de type H ( x ) , de telle sorte que donnés x : T ( a ) et p : H ( x ) , on peut construire un terme ~ x : a .$A$$T(A)$$x : T(A)$$H(x)$$x:T(A)$$p:H(x)$$\tilde x : A$

Ma motivation pour cela est que j'aimerais éventuellement pouvoir relier plus formellement les notions de théorie de la complexité informatique à la théorie des types constructifs. Plus précisément, je suis intéressé par le pouvoir que les types constructifs d'une théorie formelle acquièrent avec l'accès à un oracle en arrêt, et pour ce faire, j'ai bien sûr besoin d'avoir réellement une notion formelle de non-résiliation possible, et des preuves de l'arrêt de aller de pair avec elle dans un cadre de théorie des types.

Parce que l'une des principales applications de la théorie des types dans les formalisations a été d'étudier les langages de programmation et le calcul en général, de nombreuses réflexions ont été menées sur les moyens de représenter des programmes éventuellement non terminés.

Je ne ferai pas un sondage complet ici, mais je vais essayer de donner des indications sur les principales orientations de différentes directions.

• $F\ x\ y$$f$$x$$f(x)=y$$\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$

  Une méthode plus sophistiquée est la méthode "Bove-Capretta" (voir Modélisation de la récursivité dans la théorie des types , qui définit pour chaque fonction récursive un "prédicat accessible" qui code le fait qu'un calcul donné est fini. La définition de la fonction prend un argument supplémentaire qui est une preuve que les entrées données sont accessibles. Pour définir la fonction sans ce prédicat supplémentaire, vous devez prouver que toutes les combinaisons possibles d'entrées sont accessibles.

• $A$

  codata Delay A =
  | Now : A -> Delay A
  | Later (Delay A)
  

  Cela code un flux éventuellement infini de Laterjetons ("ticks" de calcul) se terminant peut-être par un résultat Now a. La non-résiliation équivaut à être similaire au programme

  loop = Boucle ultérieure et terminaison peuvent être définies par un prédicat inductif sur Delay A:

  data Terminates : Data A -> Prop =
  | Term_now : forall x, Terminates (Now x)
  | Term_later : forall d, Terminates d -> Terminates (Later d)
  

  Je pense que les agda-istas ont beaucoup à dire sur ce qu'ils appellent la monade de la partialité (voir par exemple Danielsson ).

• L'approche de la "théorie des types partiels" : elle est un peu plus expérimentale (la théorie est encore en cours d'élaboration), mais il existe des théories de types qui sont développées pour faire face au fait qu'il existe essentiellement deux types de fonctions que nous voulons écrire en théorie des types: les termes de preuve et les programmes. Il s'avère difficile d'obtenir une théorie raisonnable de ces choses (et de conserver la cohérence de la théorie), mais une tentative sérieuse est faite ici par Casinghino et al , et un effort similaire par Kimmel et al .

Je suis sûr qu'il existe d'autres approches que je ne connais pas, et je serais heureux si quelqu'un veut compléter cette liste.

$\Pi^0_1$

Il existe d'autres interactions assez fructueuses entre la théorie des types et la théorie de la complexité, généralement sous l'égide de la complexité informatique implicite .