Existe-t-il un modèle de calcul non complet de Turing dont le problème d'arrêt est indécidable?

26

Je ne peux pas penser à un tel modèle, peut-être une forme de calcul lambda typé? un automate cellulaire élémentaire?

Cela réfuterait presque le «principe d'équivalence informatique» de Wolfram:

Presque tous les processus qui ne sont évidemment pas simples peuvent être considérés comme des calculs de sophistication équivalente

automata-theory computability turing-machines lambda-calculus universal-computation Diego de Estrada
la source

Réponses:

18

Vous pouvez facilement construire des modèles artificiels qui ne sont pas complets, mais le problème d'arrêt pour eux est indécidable. Par exemple, prenez toutes les MT qui ne s'arrêtent sur rien d'autre que .0

Concernant la déclaration:

Vous ne pouvez pas réfuter une déclaration qui n'est pas suffisamment précise. Presque aucun des mots de l'énoncé n'est bien défini (veuillez en fournir la définition si ce n'est pas le cas).

Kaveh
la source
mmm, disons qu'un modèle est Turing-complet s'il peut simuler un UTM.
Diego de Estrada
1
Je pense que le principe d'équivalence de Wolfram est plus proche de la physique que de la logique. Les logiciens semblent vouloir l'attaquer pour diverses raisons: ce n'est pas précis, ce n'est pas prouvé, on peut arranger les choses donc c'est faux, etc. Mais en fait Wolfram pointe, à sa manière, un fait très intéressant sur le calcul , car il se pose "dans la nature".
Andrej Bauer
1
Je ne connais pas la cueillette des cerises, le livre me semble assez complet, surtout toutes ces notes. Y a-t-il une raison a priori de ne pas autoriser les modifications des définitions standard? Vous mesurez avec le mauvais critère ici. Wolfram ne fait pas de mathématiques, du moins pas dans le sens traditionnel du terme.
Andrej Bauer
4
@Andrej, mon principal problème est que la déclaration est si vague que je ne vois pas comment elle peut faire des prédictions vérifiables / réfutables. Et oui, si quelqu'un modifie les définitions standard juste pour pouvoir interpréter ce qui ne serait pas un support pour une revendication comme un support pour la revendication, alors je pense que c'est problématique.
Kaveh
4
La déclaration est vague, mais alors quoi? Ce n'est pas de la logique ou des mathématiques. C'est une observation, étayée par un livre épais rempli d'exemples, que, dans la nature, les «systèmes de calcul» ont tendance à être trivialement simples ou extrêmement sophistiqués et «équivalents» les uns aux autres. Plutôt que de critiquer Wolfram pour ne pas parler du jargon de la logique et des mathématiques, il serait plus productif de voir qu'il a un point, puis de formuler ce point dans le formalisme que votre cœur désire. Mais bien sûr, si votre cœur ne désire rien de tel, alors vous ne le ferez pas.
Andrej Bauer
4

Je suis sûr que l'argument de la diagonalisation s'applique à tout modèle de calcul qui:

  • peut se représenter comme une chaîne, et
  • peut simuler une autre machine, étant donné la représentation ci-dessus

Si nous avions un modèle qui violait l'une des conditions ci-dessus, sa puissance de calcul serait extrêmement limitée.

gabgoh
la source
10
∀x.f(x)≠x
2

Je ne suis pas sûr de la connexion exacte, mais cela semble lié au théorème de Friedberg-Muchnik (voir ici ): il y a un re set dont le degré de Turing est inférieur au problème d'arrêt. Ce résultat a répondu à une question influente de la poste et a conduit à l'introduction de la "méthode prioritaire" dans la calculabilité.

Super0
la source
-2

Probablement. Il existe de nombreux problèmes mathématiques qui en incluent probablement certains, qui sont indécidables, c'est-à-dire que la réponse est "oui" mais aucune preuve de cela n'existe. Par exemple, le problème Collatz 3x + 1 vient à l'esprit en tant que candidat. Ou la question de savoir si pi contient des chaînes arbitrairement longues de 9 consécutifs. Un tel problème pourrait être considéré comme un "modèle de calcul" vraisemblablement beaucoup moins puissant qu'un UTM, mais il serait toujours indécidable s'il "s'arrête" ou s'il "s'arrête toujours".

Warren D. Smith
la source
Je ne pense pas que cette approche puisse fonctionner. Voir: pour une telle instruction fixe, il existe un algorithme qui décide s'il est "vrai" ou "faux" dans un laps de temps fini, même lorsqu'il est indécidable dans ZFC (ref: en.wikipedia.org/wiki/Busy_beaver #Applications ). En revanche, si vous considérez comme un modèle de calcul le problème "étant donné un énoncé, décidez s'il a une preuve en ZFC", je pense que ce modèle est Turing-complet.
Diego de Estrada