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

48

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.

Timothy Chow
la source
3
..reminds moi de la théorie de l'interprétation abstraite.
Jagadish
1
[Avec le commentaire de Jagadish]: Vous pouvez jeter un coup d'œil au cours 16.399 du MIT : Interprétation abstraite . Spécialement, la conférence 3 pourrait être utile pour votre cas.
MS Dousti
6
La mesure évidente que vous n'apprécierez probablement pas est de simplement commander diverses solutions partielles en fonction de leurs domaines (c'est-à-dire l'ensemble des entrées sur lesquelles elles fonctionnent). Pour quoi voudriez-vous utiliser la mesure?
Andrej Bauer
3
@Andrej: laissez-moi répondre à votre question indirectement. Dans le domaine des problèmes NP-difficiles, nous obtenons parfois de très beaux résultats: "Un tel ratio d'approximation est réalisable, et toute amélioration supplémentaire est impossible sans P = NP". Pouvoir prouver des résultats analogues pour des problèmes indécidables intéressants serait bien. Cela nous permettrait de savoir s’il existe un obstacle intrinsèque à de nouveaux progrès.
Timothy Chow
proposer un concept de "quasialgorithmes" avec quelques recherches dans le domaine
vzn

Réponses:

30

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.

ω

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.

Neel Krishnaswami
la source
6

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".

Sariel Har-Peled
la source
2

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.

Mn<nϵϵp>0

ρnρn<n

Ted
la source