Le problème de l'arrêt pourrait-il être «résolu» en s'échappant vers une description de niveau supérieur du calcul?

21

J'ai récemment entendu une analogie intéressante qui déclare que la preuve de Turing de l'indécidabilité du problème d'arrêt est très similaire au paradoxe du barbier de Russell.

Je me suis donc demandé: les mathématiciens ont finalement réussi à rendre la théorie des ensembles cohérente en passant de la formulation naïve du champ de Cantor à un système plus complexe d'axiomes (théorie des ensembles ZFC), faisant d'importantes exclusions (restrictions) et ajouts en cours de route.

Serait-il donc possible d'essayer de trouver une description abstraite du calcul général qui soit plus puissante et plus expressive que les machines de Turing, et avec laquelle on pourrait obtenir soit une preuve existentielle, soit peut-être même un algorithme pour résoudre le problème d'arrêt pour une machine de Turing arbitraire?

H2CO3
la source
1
Bienvenue sur Computer Science Stack Exchange. Veuillez lire cs.stackexchange.com/tour.si vous ne l'avez pas encore fait. --- Qu'avez-vous essayé pour un modèle plus puissant que TM? Qu'est-ce qui vous bloque?
babou
2
@babou Au contraire, vous avez besoin d'un modèle moins puissant.
Yuval Filmus
2
@YuvalFilmus Eh bien, l'OP demande un modèle plus puissant, pas plus faible. --- avec des excuses à H2CO3 ... Ma question était en fait une blague car c'est une question standard lorsque les gens soumettent leurs devoirs comme question. Ce n'était bien sûr pas approprié ici, car personne ne s'attend à ce que vous trouviez un tel modèle. J'espère que vous ne le prendrez pas trop acide.
babou
1
Vous aimerez peut-être en savoir plus sur l'hypercomputation en.wikipedia.org/wiki/Hypercomputation .
Eric Towers

Réponses:

15

Vous ne pouvez pas vraiment comparer. La théorie des ensembles naïfs avait des paradoxes qui ont été éliminés par la théorie des ensembles ZFC. La théorie doit être améliorée pour la cohérence, car une hypothèse de base du travail scientifique est que la cohérence est réalisable (sinon le raisonnement devient une affaire hasardeuse). Je suppose que les mathématiciens s'attendaient à ce que cela soit possible et ils ont travaillé pour résoudre le problème.

Il n'y a pas une telle situation avec la théorie du calcul et le problème d'arrêt. Il n'y a pas de paradoxe, pas d'incohérence. Il se trouve qu'il n'y a pas de machine Turing capable de résoudre le problème d'arrêt de TM. C'est simplement un théorème, pas un paradoxe.

Il se peut donc qu'une percée dans notre compréhension de l'univers conduise à des modèles de calcul au-delà de ce que nous pouvons envisager maintenant. Le seul événement de ce type, sous une forme très faible, qui reste dans le domaine de la MT, était peut-être l'informatique quantique. Outre cet exemple très faible qui touche à la complexité (combien de temps cela prend-il?) Plutôt qu'à la calculabilité (est-ce faisable?), Je doute que quiconque sur cette planète ait une idée que la calculabilité au-delà de la MT est à prévoir.

De plus, le problème de l'arrêt est une conséquence directe du fait que les machines de Turing peuvent être décrites par un morceau de texte fini, une séquence de symboles. C'est en fait vrai de toutes nos connaissances (à notre connaissance), et c'est pourquoi la parole et les livres sont si importants. Cela est vrai de toutes nos techniques pour décrire les preuves et les calculs.

Donc, même si nous devions trouver un moyen d'étendre la façon dont nous calculons, disons avec les machines T +. Soit cela signifierait que nous avons trouvé un moyen d'exprimer des connaissances au-delà de l'écriture de documents finis, auquel cas le tout tombe hors de ma juridiction (je revendique une incompétence absolue) et probablement de n'importe qui d'autre. Ou il serait toujours exprimable dans des documents finis, auquel cas il aurait son propre problème d'arrêt pour les machines T +. Et vous poseriez à nouveau la question.

En fait, cette situation existe en sens inverse. Certains types de machines sont plus faibles que les machines de Turing, comme les automates linéaires délimités (LBA). Ils sont assez puissants cependant, mais il peut être montré exactement comme cela est fait pour TM que LBA ne peut pas résoudre le problème d'arrêt pour LBA. Mais TM peut le résoudre pour LBA.

Enfin, vous pouvez imaginer des modèles de calcul plus puissants en introduisant oracle, qui sont des appareils qui peuvent donner des réponses à des problèmes spécifiques, et peuvent être appelés par une MT pour obtenir des réponses, mais malheureusement, ils n'existent pas physiquement. Une telle extension TM oracle est un exemple de la machine T + que j'ai considérée ci-dessus. Certains d'entre eux peuvent résoudre le problème d'arrêt de la MT (abstraitement, pas pour de vrai), mais ne peuvent pas résoudre leur propre problème d'arrêt, même abstraitement.

babou
la source
En supposant que ZFC est cohérent, il est toujours incomplet, c'est-à-dire qu'il y a des phrases que nous ne pouvons ni prouver ni réfuter de ZFC, et cela est intimement lié au problème d'arrêt insoluble, si l'arrêt était résoluble, nous pourrions prouver ou infirmer toutes les phrases. Ce sont des mathématiques, et ce n'est pas une incohérence à résoudre mais aussi un théorème (Gödel)
Hernan_eche
@Hernan_eche Eh bien ... oui et ... quoi ...? Si vous pensez que l'incohérence n'est pas pire que l'incomplétude, c'est votre jugement personnel. Je doute que la plupart des mathématiciens soient d'accord. Vous n'aimerez peut-être pas TM qui ne se termine pas. Mais voudriez-vous qu'ils terminent toujours mieux, en disant parfois oui et parfois non, sur la même entrée. Que feriez-vous de la réponse? Et si vous pensez que le non-déterminisme ... réfléchissez-y à deux fois.
babou
J'ai un commentaire juste pour dire clairement que l'informatique et les mathématiques combattent les mêmes problèmes, pour éviter que les lecteurs interprètent mal la réponse comme si les mathématiques étaient résolues, ses problèmes de base avec ZFC et l'arrêt du problème n'étaient qu'un problème informatique, ce n'est pas le cas, il y a une correspondance un à un entre l'incomplétude et l'arrêt du problème, c'est le même problème. Je ne pense pas que l'incomplétude soit pire ou meilleure que l'incohérence, mais je pense que l'incomplétude deviendra une incohérence si vous voulez construire des systèmes d'ordre supérieur.
Hernan_eche
17

Eh bien, vous pouvez toujours envisager une machine Turing équipée d'un oracle pour le problème d'arrêt de la machine Turing ordinaire. Autrement dit, votre nouvelle machine a une bande spéciale, sur laquelle elle peut écrire la description d'une machine Turing ordinaire et son entrée et demander si cette machine s'arrête sur cette entrée. En une seule étape, vous obtenez une réponse et vous pouvez l'utiliser pour effectuer d'autres calculs. (Peu importe que ce soit en une seule étape ou non: ce serait suffisant s'il était garanti de se trouver dans un nombre fini d'étapes.)

Cependant, cette approche présente deux problèmes.

  1. Les machines de Turing équipées d'un tel oracle ne peuvent pas décider de leur propre problème d'arrêt: la preuve de Turing de l'indécidabilité du problème d'arrêt ordinaire peut facilement être modifiée pour ce nouveau paramètre. En fait, il existe une hiérarchie infinie, connue sous le nom de "degrés de Turing", générée en donnant au niveau suivant de la hiérarchie un oracle pour le problème d'arrêt du précédent.

  2. Personne n'a jamais suggéré une quelconque manière de mettre en œuvre physiquement un tel oracle. C'est très bien comme appareil théorique mais personne n'a la moindre idée de comment en construire un.

Notez également que ZFC est, dans un sens, plus faible que la théorie des ensembles naïfs, pas plus fort. ZFC ne peut pas exprimer le paradoxe de Russell, contrairement à la théorie naïve des ensembles. En tant que tel, une meilleure analogie serait de se demander si le problème d'arrêt est décidable pour les modèles de calcul plus faibles que les machines de Turing. Par exemple, le problème d'arrêt pour les automates finis déterministes (DFA) est décidable, car les DFA sont garantis pour s'arrêter pour chaque entrée.

David Richerby
la source
Je pense que son propre problème d'arrêt est résoluble par n'importe quelle famille d'automates s'il est trivial, c'est-à-dire qu'ils s'arrêtent tous ou qu'aucun d'eux ne le fait (ce qui peut être considéré comme étrange dans ce cas).
babou
1
@babou: qu'en est-il des automates où la machine 0 boucle pour toujours, la machine 1 sort FALSE si son entrée est 0 sinon la sortie TRUE puis s'arrête. Toutes les autres machines sortent FALSE puis s'arrêtent. Est-ce une famille d'automates dans laquelle le programme 1 résout le problème d'arrêt non trivial? Ou n'est-ce pas même une famille d'automates, faute de propriété, par exemple de composition quelconque?
Steve Jessop
@SteveJessop Eh bien, vous (et Davis Richerby) avez probablement raison dans un sens. Ce qui me dérange, c'est que c'est un exemple artificiel. Vous construisez une famille très faible, de telle sorte qu'une machine de la famille se révèle être un facteur décisif pour toute la famille. Mais, comme vous vous en doutez (cf. votre remarque sur la composition), il peut y avoir une propriété de fermeture de base qui manque pour que le problème puisse être banalisé. Je n'ai pas de réponse toute prête et je suis d'accord pour dire que ma remarque a besoin de plus de précisions sur ce qui constitue une famille d'automates, mais votre contre-exemple ne me laisse pas convaincu.
babou
3

Avertissement: une réponse philosophique / non rigoureuse

Cela peut devenir un peu «philosophique», mais je pense que cela correspond à l'esprit de votre question.

Une machine non répétable

Une pierre angulaire de la preuve du problème d'arrêt est qu'une machine de Turing se comporte comme une fonction: pour la même entrée, elle donne toujours la même sortie. Si vous supprimez cette propriété, vous n'avez pas à gérer le problème d'arrêt "général", dans le sens où la machine peut découvrir ses propres propriétés. Mais vous perdez également beaucoup des propriétés théoriques souhaitables d'une telle machine.

Suppression de propriétés

C'est un peu comme passer de la théorie des ensembles à la théorie des catégories: vous perdez certains des «paradoxes» en perdant les limites. Mais le résultat est beaucoup plus difficile à gérer.

Dans ce cas, cela signifie: Vous n'auriez aucune idée si la machine vous présente le résultat "correct". Dès que vous pouvez toujours décider quel résultat est correct, vous devez faire face à une sorte de "problème d'arrêt" en appliquant la machine à elle-même et en construisant une contradiction. Une telle machine ne serait donc probablement pas très utile.

stefan.schwetschke
la source
1
Merci, cette chose "machine non répétable" semble assez intéressante, en fait. Je ne me sens pas assez compétent pour dire confortablement un peu de sagesse sur les programmes d'auto-inspection intelligents (parce que mon instinct est qu'ils sont toujours exprimables en tant que machines de Turing), mais je pense qu'ils peuvent très bien être utiles pour certains problèmes.
H2CO3
1
Comment donnerait un exemple de non répétabilité? Comment définiriez-vous l'arrêt dans ce cas? Une difficulté majeure est que, lorsque vous essayez de définir un modèle de calcul étrange, généralement gedanken, vous devez définir la signification de l'arrêt, et quel type d'entrée la machine de décision est censée analyser, et éventuellement quelques autres choses non triviales. Voir par exemple le cas du non-déterminisme . Sans parler de la question de ce qui peut être considéré comme un modèle de calcul (probablement pas une collection ad hoc de machines).
babou
1
@ H2CO3 Une machine non répétable n'est qu'une sorte d '"expérience Gedanken" sur quelle propriété vous devez sacrifier pour sortir du "problème d'arrêt général" (construire une contradiction en laissant la machine s'auto-inspecter). Vous obtiendrez une machine qui a parfois raison, mais vous ne savez pas quand. C'est comme le programme qui calcule les numéros de loterie pour la semaine prochaine. Je peux facilement vous fournir un tel programme. La partie difficile est pour vous de décider quel programme parmi les nombreux que je vais vous donner est le bon ...
stefan.schwetschke
2

Le problème de l'arrêt n'a pas été formulé pour exprimer les limites des machines de Turing, mais plutôt pour exprimer une limitation de tous les systèmes logiques qui peut être exprimée en utilisant un nombre fini de symboles. Une fois qu'un système logique a la capacité d'exprimer les solutions à des problèmes d'une certaine complexité, il aura également la capacité d'exprimer des problèmes qu'il ne peut pas résoudre. Toute extension d'un système logique suffisante pour exprimer des solutions à tous les problèmes qu'il n'a pas pu résoudre auparavant inclura également la possibilité d'exprimer de nouveaux problèmes qu'il ne peut pas résoudre.

Compte tenu de toute spécification particulière de "machine de Turing améliorée", il serait possible de spécifier une "machine de Turing super améliorée" qui pourrait examiner un programme pour l'ETM et signaler s'il s'arrêterait, mais le SETM ne pourrait analyser que des programmes pour l'ETM - il ne serait pas en mesure d'analyser les programmes SETM. Il n'y a aucun moyen de définir une machine qui peut analyser les programmes pour elle-même et déterminer s'ils s'arrêtent parce que l'ajout de nouvelles fonctionnalités créerait de nouvelles exigences pour un auto-analyseur, et il n'y a aucun moyen de faire en sorte que les fonctionnalités «rattrapent» les exigences .

supercat
la source
1

De telles machines ont été envisagées et sont appelées machines super-Turing . Plusieurs grandes classes de machines de super-turing sont

  • Machines à nombre réel (c.-à-d. Ordinateurs analogiques)
  • Machines de Turing à temps infini
  • Machine de turing non déterministe

Toutes les machines de super-turing ne peuvent pas résoudre le problème d'arrêt (les machines de turing non déterministes, en particulier, ne le peuvent pas). Cependant, les machines conceptuelles ont été créées, au moins dans les expériences de pensée.

Cort Ammon - Rétablir Monica
la source