Algorithme pour résoudre le «problème d'arrêt de Turing»

23

"Alan Turing a prouvé en 1936 qu'un algorithme général pour résoudre le problème d'arrêt pour toutes les paires d'entrée de programme possibles ne pouvait pas exister"

Puis-je trouver un algorithme général pour résoudre le problème d'arrêt pour certaines paires d'entrée de programme possibles?

Puis-je trouver un ou plusieurs langages de programmation, où pour chaque type de programme dans ce langage, il peut décider si le programme se termine ou s’exécute pour toujours?

Kaveh
la source
3
L'ACMC a publié un article très intéressant en mai: Prouver la fin du programme
Christoph Walesch
3
"un algorithme général [...] pour certaines paires d'entrée de programme possibles" - qui est presque contradictoire. Je suppose que vous voulez vous limiter à une sous-classe infinie de tous les programmes?
Raphael

Réponses:

25

Puis-je trouver un algorithme général pour résoudre le problème d'arrêt pour certaines paires d'entrée de programme possibles?

Oui bien sûr. Par exemple, vous pouvez écrire un algorithme qui renvoie "Oui, il se termine" pour tout programme qui ne contient ni boucles ni récursivité et "Non, il ne se termine pas" pour tout programme qui contient une while(true)boucle qui sera certainement atteinte et ne contient pas une déclaration de pause et "Dunno" pour tout le reste.

Puis-je trouver un ou plusieurs langages de programmation, où pour chaque type de programme dans ce langage, il peut décider si le programme se termine ou s’exécute pour toujours?

Pas si cette langue est Turing-complete, non.

Cependant, il existe des langages complets non Turing comme par exemple Coq , Agda ou Microsoft Dafny pour lesquels le problème d'arrêt est décidable (et en fait est décidé par leurs systèmes de types respectifs, ce qui en fait un total de langues (c'est-à-dire qu'un programme qui pourrait ne pas se terminer ne sera pas compiler)).

sepp2k
la source
1
La classe des fonctions primitives-récursives est un "langage de programmation" bien connu pour lequel le problème d'arrêt est trivialement décidable.
Raphael
Il existe plusieurs langages de " programmation fonctionnelle totale " dans lesquels tous les programmes se terminent de manière prouvée.
Anderson Green
3

Je pense que toutes les réponses ici manquent complètement et complètement le point. La réponse à la question est: en supposant que le programme est destiné à s'arrêter, alors oui, vous feriez mieux de pouvoir montrer qu'il s'arrête. Si vous ne pouvez pas montrer qu'il s'arrête facilement, le programme doit être considéré comme très mal écrit et rejeté par le contrôle qualité en tant que tel.

La possibilité d'écrire un algorithme machine approprié dépend du langage de programmation d'entrée et de votre ambition. C'est un objectif de conception raisonnable pour un langage de programmation de permettre facilement de prouver la terminaison.

Si le langage est C ++, vous ne pouvez probablement pas écrire l'outil, en effet, il est peu probable que vous lanciez l'analyseur, et encore moins prouviez la terminaison. Pour un langage mieux structuré, vous devriez au moins pouvoir générer une preuve, ou du moins le faire avec certaines hypothèses: dans ce dernier cas, l'outil devrait sortir ces hypothèses. Une approche similaire consisterait à inclure les assertions de terminaison dans la langue et à les utiliser dans des situations complexes où l'outil ferait confiance aux assertions.

L'essentiel est que personne ne semble comprendre que la preuve qu'un programme s'arrête est en effet possible parce que les (bons) programmeurs ayant l'intention d'écrire de tels programmes d'arrêt le font toujours intentionnellement et avec une image mentale des raisons pour lesquelles ils se terminent et agissent correctement: un tel code est délibérément écrit de sorte qu'il est clair qu'ils s'arrêtent et sont corrects et si un algorithme raisonnable ne peut pas le prouver, éventuellement avec quelques indices, alors le programme doit être rejeté.

Le point: les programmeurs n'écrivent pas de programmes arbitraires, donc la thèse du théorème d'arrêt n'est pas satisfaite et la conclusion ne s'applique pas.

Yttrill
la source
4
Je pense que c'est vous qui avez complètement et complètement raté le point. Le premier paragraphe de votre réponse ne s'applique pas à la question, car il concerne les algorithmes - pas ce qu'un humain peut ou ne peut pas prouver. Le reste de la réponse répond au premier paragraphe de la question, à savoir si un algorithme pourrait prouver la terminaison pour certains programmes. Toutes les réponses précédentes ont déjà dit «oui» à celle-là.
sepp2k
3
Votre affirmation selon laquelle il est possible d'écrire un algorithme qui puisse prouver la fin de chaque programme bien écrit dans un langage Turing-complete suffisamment simple est tout simplement fausse. Pour chaque algorithme possible qui essaie de prouver la terminaison, il y a des problèmes où chaque programme qui résout ce problème ne peut pas être arrêté par cet algorithme. Donc, à moins que vous ne disiez que chaque programme résolvant ce problème est mal écrit par définition (ce qui serait ridicule), cela réfute votre argument.
sepp2k
1
@Sam Si quelqu'un me demande si certains codes s'arrêtent, je vais regarder le code et essayer de le comprendre. Mais je ne suis pas un algorithme. Et oui, il est possible d'écrire un algorithme qui peut vérifier si un programme s'arrête pour beaucoup de programmes. Mais ce n'est pas ce que Yttrill a dit. Yttrill a déclaré que c'était possible pour tous les programmes bien écrits. Et comme je l'ai dit dans mon commentaire précédent, c'est tout simplement faux, sauf si vous prétendez que certains problèmes ne peuvent être résolus que par des programmes mal écrits (ce qui serait encore ridicule).
sepp2k
1
@Sam "il me semble évident que les programmes intentionnellement écrits pour stopper peuvent être facilement analysés pour les conditions d'arrêt" - si tel était le cas, pourquoi n'avons-nous pas de tels outils? Ce n'est pas comme si les gens n'essayaient pas. (Un coupable est le dépassement de méthode: au moment de la compilation, vous ne connaissez pas tout le code qui sera exécuté.)
Raphael
1
@Sam "existe-t-il une boucle infinie" est une chose difficile à aborder, même pour une boucle réelle. Bien sûr, on m'a appris à trouver des invariants de boucle, mais cela ne signifie pas que je puisse en trouver un (facilement) dans de nombreux cas. Pour autant que je sache, deviner et prouver est la référence absolue de nos jours. Encore une fois, s'il y avait assez d' algorithmes généraux, je les attends à inclure dans les grandes ou compiles IDEs (qui font effectuer des vérifications triviales, syntaxiques). Pouvez-vous donner une référence à un algorithme raisonnablement solide?
Raphael
3

excellente et (probablement involontairement profonde) question. il existe en effet des programmes de détection d'arrêt qui peuvent réussir sur des ensembles limités d'entrées. c'est un domaine de recherche actif. il a des liens très forts avec les domaines de démonstration de théorèmes (automatisés).

cependant, l'informatique ne semble pas avoir de terme exact pour désigner les «programmes» qui réussissent «parfois». le mot "algorithme" est généralement réservé aux programmes qui s'arrêtent toujours.

le concept semble être nettement différent des algorithmes probabilistes où les théoriciens CS insistent sur le fait qu'il existe une probabilité connue ou calculable de leur réussite.

il existe un terme semi - algorithmes qui est parfois utilisé, mais c'est apparemment un synonyme de récursivement énumérable ou non calculable.

donc à des fins ici, appelez-les algorithmes quasi-aléatoires . le concept est différent de décidable vs indécidable.

AXBYXYXYBA

dans CS, cette "quasi-hiérarchie d'algorithmes" semble être étudiée jusqu'à présent uniquement de manière informelle.

il apparaît dans la recherche sur les castors occupés [1] et le problème PCP [2]. en fait, une attaque informatique basée sur l'ADN sur PCP peut être considérée comme un algorithme quasi-complet [3]. et son vu dans d'autres domaines déjà notés tels que la preuve de théorème [4].

[1] Nouvelle attaque du millénaire contre le problème du castor occupé

[2] Tackling Posts correspondance problem by Zhao (v2?)

[3] Utiliser l'ADN pour résoudre le problème de la correspondance post-bornée par Kari et al

[4] prouver la fin du programme par Cook et al, Comm. de l'ACM

(donc c'est en fait une question très profonde qui mérite d'être sur TCS.SE à mon humble avis ... peut-être que quelqu'un peut la poser à nouveau de manière à ce qu'elle s'adapte et reste)

vzn
la source
ps comme un exemple impressionnant de la puissance des algorithmes quasial, la référence ACM indique que la fonction ackermanns peut être prouvée comme arrêtée par un algorithme quasial, mais elle est plus grande que (non calculable par) toutes les fonctions récursives primitives.
vzn
1
"le mot" algorithme "est généralement réservé aux programmes qui s'arrêtent toujours." - Je ne suis pas sûr que ce soit vrai. Il y a beaucoup d'algorithmes se terminant partiellement (en particulier dans la vérification) et je n'ai jamais entendu personne dire "algorithme".
Raphael
il existe des utilisations informelles de "l'algorithme". "se terminant partiellement" est correct mais probablement non fixe. comme indiqué, il ne semble pas encore y avoir de terme standardisé. wikipedia définit un algorithme comme une méthode efficace, c'est-à-dire décidable avec les caractéristiques suivantes (1) donne toujours une réponse plutôt que de ne jamais donner de réponse; (2) toujours donner la bonne réponse et ne jamais donner une mauvaise réponse; (3) toujours être complété en un nombre fini d'étapes, plutôt qu'en un nombre infini; (4) travailler pour tous les cas de problèmes de la classe.
vzn
puis plus loin dans le même article, il est dit "Une autre explication du terme" méthode efficace "peut inclure l'exigence selon laquelle, en cas de problème extérieur à la classe pour laquelle la méthode est efficace, la méthode peut s'arrêter ou boucler pour toujours sans s'arrêter , mais ne doit pas renvoyer un résultat comme s'il s'agissait de la réponse au problème. " c'est à dire qu'il se contredit presque!?! il est donc clair, remarquable, qu'il existe une réelle confusion sur la question clé et la terminologie existante n'est pas stricte. notez que le mot "algorithme" est proche de plus d'un millénaire ou plus et a considérablement changé ....
vzn
C'est vrai: le sens traditionnel est probablement «méthode efficace» dans la façon dont Wikipedia dit (il n'y a pas de contradiction dans la phrase que vous citez; c'est un peu flou, cependant) - les gens n'ont pas conçu de fonctions / algorithmes qui ne se sont pas terminés (pour certaines entrées). Je pense que cela a changé depuis les années 50; comme je l'ai dit, aujourd'hui, les gens appellent clairement une méthode à «terminaison partielle» «algorithme».
Raphael
2

Tant que le langage de programmation en question est suffisamment complexe (c'est-à-dire s'il est Turing complet), alors il y a toujours des programmes dans le langage qu'aucun programme ne peut prouver pour terminer.

Étant donné que tous les langages, sauf les plus primitifs, sont Turing complet (cela ne prend que des variables et des conditions), vous ne pouvez vraiment créer que de très petits langages jouets pour lesquels vous pouvez résoudre le problème d'arrêt.

Edit: À la lumière des commentaires, permettez-moi d'être plus explicite: Toute langue que vous pourriez concevoir pour laquelle vous pourriez résoudre le problème d'arrêt devrait nécessairement être Turing-incomplète. Cela exclut tout langage contenant un ensemble approprié d'ingrédients de base (par exemple, "variables, conditions et sauts", ou, comme le dit @ sepp2k, une boucle "while" générique).

Apparemment, il existe plusieurs langages pratiques "simples" comme celui-ci (par exemple les solveurs de théorèmes tels que Coq et Agda). Si ceux-ci satisfont à votre notion de "langage de programmation", vous pouvez rechercher s'ils satisfont à une sorte d'exhaustivité, ou si le problème d'arrêt est résoluble pour eux.


la source
3
"Puisque tous les langages, à l'exception des plus primitifs, sont Turing complets (cela ne prend que des variables et des conditions)" Ce n'est pas vrai. Tout d'abord, vous auriez au moins besoin d'une récursivité ou d'une forme de construction en boucle (qui devrait être aussi puissante qu'une boucle while - une simple boucle de comptage ne suffit pas). Deuxièmement, je ne pense pas qu'il y ait beaucoup de gens qui appellent des langues comme Coq ou Agda (qui sont totales et donc pas complètes) des langues primitives ou jouets.
sepp2k
@ sepp2k: Eh bien, oui. L'arithmétique Peano est également très utile et n'est pas complète. Une déclaration simplifiée, je suppose. Si l'OP est suffisamment familier avec le problème, elle pourra, espérons-le, remplir les détails techniques.
3
Il y a un énorme fossé entre être «suffisamment complexe» et être Turing-complet. Coq est en effet complexe, et il convient à un très large éventail de tâches pratiques.
1
@Kerrek SB Eh bien, il est possible que le langage Turing-complet soit utilisé d'une manière qui reste prouvable jusqu'à la résiliation. Si vous pouvez prouver qu'une formule récursive se rapproche toujours de sa condition de terminaison (comme la fonction factorielle), vous pouvez prouver qu'elle se termine même si vous ne pourriez pas gérer tous les types de récursivité.
@ArtB: Bien sûr, il y a toujours des programmes dont on peut prouver qu'ils se terminent. La première question du PO pourrait faire allusion à cela, mais je ne suis pas sûr de la suivre pleinement. Par exemple, vous ne pourriez pas avoir un "algorithme générique" qui détermine si une famille donnée de programmes se termine, tandis que, inversement, vous pourriez probablement construire une famille restreinte de fonctions de telle sorte qu'en supposant qu'une fonction appartient à cette famille, vous pourriez dire algorithmiquement si elle se termine. (Je ne sais pas si cette famille peut être non triviale, cependant. Je suppose que oui, mais je ne peux pas en faire un exemple.)
2

TT

C'est assez banal. Si nous prenons l'union de n'importe quel sous-ensemble ce de TM en arrêt et tout sous-ensemble ce de TM sans arrêt, le résultat sera un ensemble de MT pour lesquelles le problème d'arrêt est décidable (exécutez les deux machines en parallèle, si le premier accepte le TM s'arrête, si le second accepte alors la machine ne s'arrête pas). Cependant, cela ne conduira pas à des langues très intéressantes.

ALogTimecM

Kaveh
la source
1

Oui, vous pouvez, mais je doute que ce sera utile. Vous devrez probablement le faire par analyse de cas et vous ne pourrez alors rechercher que les cas les plus évidents. Par exemple, vous pouvez grep un fichier pour le code while(true){}. Si le fichier contient ce code, il ne se terminera jamais ^. Plus généralement, vous pourriez dire qu'un programme sans boucle ni récursivité se terminera toujours et il y a plusieurs cas que vous pourriez faire qui pourraient garantir qu'un programme se terminera ou ne se terminera pas, mais même pour un programme de taille moyenne, ce serait très difficile et dans de nombreux cas, ne serait pas en mesure de vous donner une réponse.

tl; dr: Oui, mais vous ne pourrez pas l'utiliser pour la plupart des programmes utiles.


^ Oui, techniquement, si ce code n'est pas sur le chemin de code ou s'il y a d'autres threads, il pourrait toujours se terminer, mais je fais une remarque générale ici.


la source
4
Pourquoi pensez-vous que Coq et Agda ne sont pas utiles? Vous surestimez la valeur d'exhaustivité de Turing.
J'ai utilisé Coq, mais ma réclamation demeure car la plupart des logiciels commerciaux sont écrits en Java / C ++ / Ruby / C # pour lesquels mes réclamations sont vraies. Le genre de programmes que 90% des gens sont intéressés à écrire ne bénéficierait pas. Fondamentalement, si vous ne connaissez pas Coq / Agda, etc., vous n'êtes pas le marché cible pour cela.
5
Je dirais que 99% des programmes du monde réel gagneraient à être implémentés dans un sous-ensemble non complet de Turing d'une langue. Vous n'implémenterez pas, disons, la fonction Ackermann tous les jours. 100% de CRUD n'a pas besoin d'une "vraie" langue. Le traitement des données est presque toujours trivial. Voir le projet Terminator - ils servent même un sous-ensemble décent de programmes C ++ possibles, ce qui est plus que suffisant pour le monde réel (y compris les pilotes et autres codes de bas niveau).
La plupart des projets du monde réel souhaitent réutiliser des bibliothèques écrites dans des langages complets de Turing et utiliser leurs IDE, débogueurs et didacticiels. Oui, vous pourriez accomplir des choses dans des langages non-Turing, mais je ne peux pas imaginer que certains disent réellement "Je veux faire X" et ma réponse est "Use Coq". ps- merci de m'avoir présenté le projet Terminator .
4
une part inimaginable de la logique métier est déjà implémentée dans un SQL non complet de Turing. Et les DSL et eDSL sont en hausse maintenant. Ainsi, bientôt la plupart des programmeurs d'applications professionnelles oublieront tous les langages "à usage général".