Existe-t-il une notion judicieuse d'un algorithme d'approximation pour un problème indécidable?

On sait que certains problèmes sont indécidables, mais il est néanmoins possible de progresser dans leur résolution. Par exemple, le problème d'arrêt est indécidable, mais des progrès pratiques peuvent être réalisés dans la création d'outils permettant de détecter les boucles infinies potentielles dans votre code. Les problèmes de carrelage sont souvent indécidables (par exemple, ce polyomino est-il un rectangle?), Mais encore une fois, il est possible d'améliorer l'état de la technique dans ce domaine.

Ce que je me demande, c'est s'il existe une méthode théorique décente pour mesurer les progrès accomplis dans la résolution de problèmes indécidables, qui ressemble à l'appareil théorique mis au point pour mesurer les progrès réalisés dans les problèmes difficiles à résoudre. Ou semble-t-il que nous sommes coincés avec des évaluations ad hoc, je-sais-progresser-quand-je-vois-rien-à-dire, de combien d'avancées particulières font progresser notre compréhension des problèmes indécidables?

Edit : En réfléchissant à cette question, je me rends compte que la complexité paramétrée est peut-être pertinente ici. Un problème indécidable peut devenir décidable si nous introduisons un paramètre et en fixons la valeur. Je ne suis cependant pas sûr que cette observation soit utile.

Dans le cas du problème d’arrêt, la réponse est "pas encore". La raison en est que la méthode logique standard pour caractériser la force de la preuve de terminaison d'un programme (par exemple, l'analyse ordinale) a tendance à perdre trop de structure combinatoire et / ou théorique.

$\omega$

Cela signifie qu’il n’ya pas de relation nette entre la force de preuve de la métalogique dans laquelle vous montrez une terminaison (c’est très important dans la théorie de la réécriture, par exemple) et les fonctions que des techniques comme la synthèse par fonction de rang peuvent indiquer une terminaison. .

Pour le lambda calcul, nous avons une caractérisation précise de la terminaison en termes de typabilité: un terme lambda est fortement normalisant si et seulement s’il est typable sous la discipline du type intersection. Bien entendu, cela signifie qu'une inférence de type complète pour les types d'intersection est impossible, mais cela peut également permettre de comparer des algorithmes d'inférence partielle.

D'après une conversation mémorable sur une personne qui a implémenté un algorithme qui résout un problème indécidable: "Cela prend 2-3 secondes pour toutes les entrées que j'ai essayées".

Cela répond plus au titre de la question qu'à son contenu, mais vous pouvez également considérer les "approximations" du problème bloquant comme des algorithmes qui vous donneront une réponse correcte sur "presque tous" les programmes.

La notion de "presque tous" les programmes n'a de sens que si votre modèle de calcul est optimal (au même sens que pour la complexité de Kolmogorov ), afin d'éviter les situations où la majorité de vos programmes sont triviaux.

$M$$n$$\lt n$$\epsilon$$\epsilon$$p\gt 0$

$\rho_n$$\rho_n$$<n$