Existe-t-il un sous-ensemble de programmes qui évitent le problème d'arrêt

Je lisais juste une autre explication du problème d'arrêt, et cela m'a fait penser que tous les problèmes que j'ai vus qui sont donnés à titre d'exemples impliquent des séquences infinies. Mais je n'utilise jamais de séquences infinies dans mes programmes - elles prennent trop de temps. Toutes les applications du monde réel ont des limites inférieures et supérieures. Même les réels ne sont pas vraiment réels - ce sont des approximations stockées en 32/64 bits, etc.

La question est donc de savoir s'il existe un sous-ensemble de programmes qui peuvent être déterminés s'ils s'arrêtent? Est-ce assez bon pour la plupart des programmes. Puis-je construire un ensemble de constructions de langage que je peux déterminer la «cessabilité» d'un programme. Je suis sûr que cela a été étudié quelque part auparavant, donc tout conseil serait apprécié. Le langage ne serait pas complet, mais existe-t-il quelque chose de presque complet qui soit assez bon?

Naturellement, une telle construction devrait exclure la récursivité et les boucles while non limitées, mais je peux écrire un programme sans celles-ci assez facilement.

La lecture de l'entrée standard comme exemple devrait être limitée, mais c'est assez facile - je limiterai ma saisie à 10 000 000 caractères, etc., en fonction du domaine problématique.

tia

[Mise à jour]

Après avoir lu les commentaires et les réponses, je devrais peut-être reformuler ma question.

Pour un programme donné dans lequel toutes les entrées sont limitées, pouvez-vous déterminer si le programme s'arrête. Si oui, quelles sont les contraintes du langage et quelles sont les limites de l'ensemble d'entrée. L'ensemble maximal de ces constructions déterminerait un langage qui peut être déduit pour s'arrêter ou non. Y a-t-il une étude qui a été réalisée à ce sujet?

[Mise à jour 2]

voici la réponse, c'est oui, en 1967 depuis http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

Le fait que le problème d'arrêt puisse être au moins théoriquement résolu pour les systèmes à états finis a déjà été avancé par Minsky en 1967 [4]: ​​«... toute machine à états finis, si elle est laissée à elle-même, tombera finalement dans une situation parfaitement périodique. motif répétitif. La durée de ce motif répétitif ne peut pas dépasser le nombre d'états internes de la machine ... »

(et donc si vous vous en tenez aux machines à turing finies, vous pouvez construire un oracle)

Le problème n'est pas sur l'entrée (évidemment, avec une entrée illimitée, vous pouvez avoir un temps d'exécution illimité juste pour lire l'entrée), c'est sur le nombre d'états internes.

Lorsque le nombre d'états internes est limité, théoriquement, vous pouvez résoudre le problème d'arrêt dans tous les cas (émulez-le jusqu'à ce que vous arriviez à l'arrêt ou à la répétition d'un état), quand il ne l'est pas, il y a des cas où il n'est pas résoluble . Mais même si le nombre d'états internes est en pratique limité, il est également si énorme que les méthodes reposant sur la limitation du nombre d'états internes sont inutiles pour prouver la fin de tous les programmes sauf les plus triviaux.

Il existe des moyens plus pratiques de vérifier la fin des programmes. Par exemple, exprimez-les dans un langage de programmation qui n'a ni récursivité ni goto et dont les structures en boucle ont toutes une limite sur le nombre d'itérations qui doit être spécifié à l'entrée de la boucle. (Notez que la limite ne doit pas être vraiment liée au nombre effectif d'itérations, une façon standard de prouver la fin d'une boucle est d'avoir une fonction dont vous prouvez qu'elle est strictement décroissante d'une itération à l'autre et votre condition d'entrée assurez-vous qu'il est positif, vous pouvez mettre la première évaluation comme limite).

Tout d'abord, réfléchissez à ce qui se passerait si nous avions un détecteur d'arrêt. Nous savons par l'argument diagonal qu'il existe au moins un programme qui ferait en sorte qu'un détecteur d'arrêt ne s'arrête jamais ou ne donne pas une mauvaise réponse. Mais c'est un programme bizarre et peu probable.

Il existe cependant un autre argument selon lequel un détecteur d'arrêt est impossible, et c'est l'argument le plus intuitif qu'un détecteur d'arrêt serait magique. Supposons que vous vouliez savoir si le dernier théorème de Fermat est vrai ou faux. Vous écrivez simplement un programme qui s'arrête s'il est vrai et qui s'exécute pour toujours s'il est faux, puis exécutez le détecteur d'arrêt sur celui-ci. Vous n'exécutez pas le programme , vous exécutez simplement le détecteur d'arrêt sur le programme . Un détecteur d'arrêt nous permettrait de résoudre immédiatement un grand nombre de problèmes ouverts en théorie des nombres simplement en écrivant des programmes.

Alors, pouvez-vous écrire un langage de programmation qui est garanti pour produire des programmes dont l'arrêt peut toujours être déterminé? Sûr. Il ne peut tout simplement pas avoir de boucles, de conditions et utiliser arbitrairement beaucoup de stockage. Si vous êtes prêt à vivre sans boucles, sans instructions "si" ou avec une quantité de stockage strictement limitée, alors bien sûr, vous pouvez écrire une langue dont l'arrêt est toujours déterminable.

Je vous recommande de lire Gödel, Escher, Bach . C'est un livre très amusant et éclairant qui, entre autres, touche au théorème d'incomplétude de Gödel et au problème de l'arrêt.

Pour répondre à votre question en un mot: le problème d'arrêt est décidable tant que votre programme ne contient pas de whileboucle (ou l'une de ses nombreuses manifestations possibles).

Pour chaque programme qui fonctionne sur une quantité limitée de mémoire (y compris le stockage de toutes sortes), le problème d'arrêt peut être résolu; c'est-à-dire qu'un programme indécidable est appelé à prendre de plus en plus de mémoire lors de l'exécution.

Mais même ainsi, cette perspicacité ne signifie pas qu'elle peut être utilisée pour des problèmes du monde réel, car un programme d'arrêt, travaillant sur seulement quelques kilo-octets de mémoire, peut facilement prendre plus de temps que la durée de vie restante de l'univers pour s'arrêter.

Pour répondre (partiellement) à votre question "Existe-t-il un sous-ensemble de programmes qui évitent le problème d'arrêt": oui, en fait il y en a. Cependant, ce sous-ensemble est incroyablement inutile (notez que le sous-ensemble dont je parle est un sous-ensemble strict des programmes qui s'arrêtent).

L'étude de la complexité des problèmes pour «la plupart des entrées» est appelée complexité du cas générique . Vous définissez un sous-ensemble des entrées possibles, prouvez que ce sous-ensemble couvre «la plupart des entrées» et donnez un algorithme qui résout le problème pour ce sous-ensemble.

Par exemple, le problème d'arrêt est résoluble en temps polynomial pour la plupart des entrées (en fait, en temps linéaire, si je comprends bien le papier ).

Cependant, ce résultat est plutôt inutile en raison de trois notes annexes: tout d'abord, nous parlons de machines Turing avec une seule bande, plutôt que de programmes informatiques réels sur des ordinateurs réels. Pour autant que je sache, personne ne sait si c'est la même chose pour les ordinateurs du monde réel (même si les ordinateurs du monde réel peuvent être en mesure de calculer les mêmes fonctions que les machines Turing, le nombre de programmes autorisés, leur durée et s'ils s'arrêtent peuvent être complètement différent).

Deuxièmement, vous devez faire attention à ce que signifie «la plupart des entrées». Cela signifie que la probabilité qu'un programme aléatoire de «longueur» n puisse être vérifié par cet algorithme tend vers 1 car n tend vers l'infini. En d'autres termes, si n est assez grand, alors un programme aléatoire de longueur n peut presque sûrement être vérifié par cet algorithme.

Quels programmes peuvent être vérifiés par l'approche décrite dans l'article? Essentiellement, tous les programmes qui s'arrêtent avant de répéter un état (où «état» correspond à peu près à une ligne de code dans un programme).

Même si presque tous les programmes peuvent être vérifiés de cette manière, aucun des programmes qui peuvent être vérifiés de cette manière n'est très intéressant et ils ne sont généralement pas conçus par des humains, donc cela n'a aucune valeur pratique.

Cela indique également que la complexité des cas génériques ne sera probablement pas en mesure de nous aider avec le problème d'arrêt, car presque tous les programmes intéressants sont (apparemment) difficiles à vérifier. Ou, autrement dit: presque tous les programmes sont inintéressants, mais faciles à vérifier.

Il existe, et en fait, des programmes dans la vie réelle qui résolvent tout le temps le problème de l’arrêt d’autres problèmes. Ils font partie du système d'exploitation sur lequel vous exécutez votre ordinateur. L'indécidabilité est une affirmation étrange qui dit seulement qu'il n'y a pas un tel programme qui fonctionne pour TOUS les autres programmes.

Une personne a déclaré à juste titre que la preuve d'arrêt semble être le seul programme pour lequel elle ne peut pas être résolue, car elle se trace infiniment comme un miroir. Cette même personne a également déclaré que s'il y avait une machine d'arrêt, ce serait magique car cela nous indiquerait des problèmes mathématiques difficiles en nous disant à l'avance si son algorithme de solveur s'arrêterait.

L'hypothèse dans ces deux cas est que la machine d'arrêt ne trace pas car il n'y a aucune preuve qu'elle trace. Cependant, en réalité, il trace / exécute le programme sur lequel il est exécuté avec l'entrée donnée.

La preuve logique au moins est simple. S'il n'avait pas besoin de tracer au moins la première étape, il n'aurait pas besoin de l'entrée avec le programme sur lequel il est exécuté. Pour pouvoir utiliser les informations, il doit au moins tracer la première étape avant d'essayer d'analyser où va ce chemin.

Les problèmes mathématiques difficiles mentionnés dans la première réponse sont ceux où vous ne pouvez pas avancer rapidement pour trouver la réponse, ce qui signifie que le problème d'arrêt devrait continuer à suivre jusqu'à ce qu'un motif soit reconnaissable.

Ainsi, le seul argument pratique à tirer du problème d'arrêt est qu'une machine d'arrêt ne peut pas déterminer le résultat d'un résolveur de problème optimisé plus rapidement que le résolveur de problème ne peut terminer.

Donner une preuve formelle de ce raisonnement est plus difficile, et bien que je pense que je pourrais, tenter de l'expliquer à quiconque dans un milieu universitaire les amènera à jeter un singe comme une colère et à se balancer du lustre. Il vaut mieux ne pas discuter avec ces gens.

voici la réponse, c'est oui, en 1967 depuis http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

Le fait que le problème d'arrêt puisse être au moins théoriquement résolu pour les systèmes à états finis a déjà été avancé par Minsky en 1967 [4]: ​​«... toute machine à états finis, si elle est laissée à elle-même, tombera finalement dans une situation parfaitement périodique. motif répétitif. La durée de ce motif répétitif ne peut pas dépasser le nombre d'états internes de la machine ... »

(et donc si vous vous en tenez aux machines à turing finies, vous pouvez construire un oracle)

Bien sûr, combien de temps cela prend est une autre question

existe-t-il un sous-ensemble de programmes qui peuvent être déterminés s'ils s'arrêtent?

Oui.

Est-ce assez bon pour la plupart des programmes?

Définissez "la plupart".

Puis-je construire un ensemble de constructions de langage que je peux déterminer la «cessabilité» d'un programme?

Oui.

existe-t-il une chose qui soit presque complète, ce qui est assez bon?

Définissez "presque".

Beaucoup de gens écrivent Python sans utiliser d' whileinstructions ou de récursivité.

Beaucoup de gens écrivent Java en utilisant uniquement l' forinstruction avec des itérateurs ou des compteurs simples dont la terminaison peut être triviale; et ils écrivent sans récursivité.

C'est assez facile à éviter whileet à récursivité.

Pour un programme donné dans lequel toutes les entrées sont bornées, pouvez-vous déterminer si le programme s'arrête?

Non.

Si oui, quelles sont les contraintes du langage et quelles sont les limites de l'ensemble d'entrée.

Hum. Le problème Halting signifie que le programme ne peut jamais déterminer des choses sur des programmes aussi complexes que lui-même. Vous pouvez ajouter n'importe laquelle d'un grand nombre de contraintes pour surmonter le problème d'arrêt.

L'approche standard du problème d'arrêt est de permettre des preuves en utilisant un ensemble de formalismes mathématiques légèrement plus «riches» que ceux disponibles dans le langage de programmation.

Il est plus facile d'étendre le système de preuve que de restreindre la langue. Toute restriction conduit à des arguments pour le seul algorithme qui sont difficiles à exprimer en raison de la restriction.

L'ensemble maximal de ces constructions déterminerait un langage qui peut être déduit pour s'arrêter ou non. Y a-t-il une étude qui a été faite à ce sujet?

Oui. Cela s'appelle la "théorie des groupes". Un ensemble de valeurs fermé sous un ensemble d'opérations. Des trucs assez bien compris.