Si une machine abstraite peut se simuler, cela rend-il Turing complet?

Par exemple, dans les langages de programmation, il est courant d'écrire un compilateur / interprète X-in-X, mais à un niveau plus général, de nombreux systèmes Turing-complets connus peuvent se simuler de manière impressionnante (par exemple, simuler le jeu de la vie de Conway dans le jeu de la vie de Conway ).

Ma question est donc la suivante: un système capable de se simuler est-il suffisant pour prouver que Turing est complet? C'est certainement une condition nécessaire.

Pas nécessairement. Par exemple, l' automate cellulaire à bloc bidimensionnel à deux états, dans lequel une cellule ne devient vivante que lorsque ses quatre prédécesseurs ont exactement deux cellules vivantes adjacentes, peut se simuler avec un facteur de ralentissement de deux et un facteur de gonflement de deux tailles, mais n'est pas connu pour être Turing complet. Voir Le B36 / S125 "2x2" Life-Like Cellular Automaton par Nathaniel Johnston pour plus d'informations sur cet automate bloc et sur la règle B36 / S125 pour le quartier Moore qui est également capable de simuler cet automate bloc.

Non ce n'est pas. Je connais deux grandes classes de techniques pour éviter l'incohérence / l'exhaustivité de Turing.

1. La première ligne d'attaque consiste à configurer le système de sorte que la syntaxe puisse être arithmétique, mais le théorème du point fixe de Godel ne passe pas. Dan Willard a beaucoup travaillé sur ce sujet et a fourni des systèmes logiques d'auto-vérification cohérents. L'astuce consiste à éliminer les symboles de fonction de multiplication et d'addition et de les remplacer par la divisibilité et la soustraction. Cela vous donne suffisamment de puissance pour représenter la syntaxe arithmétiquement, mais le théorème du point fixe ne passe pas car la multiplication n'est pas prouvée totale.

   Voir Dan Willard. Systèmes Axiom à vérification automatique, théorème d'incomplétude et principes de réflexion associés . Journal of Symbolic Logic 66 (2001) p. 536-596.

2. La deuxième ligne d'attaque permet une plus grande utilisation des points fixes, mais pour configurer les choses afin que la syntaxe ne soit pas arithmétique. Les plus beaux systèmes pour cela sont (IMO) basés sur des variantes de logique linéaire. Par exemple, dans la théorie des ensembles d'affines légères de Kazushige Terui, même le principe de compréhension d'ensemble sans restriction est sain, mais comme la logique ambiante de la théorie des ensembles est linéaire (et donc la contraction n'est pas autorisée), le paradoxe de Russell n'est pas dérivable.

   $A \multimap B$

   Kazushige Terui. Théorie des ensembles affinés légers: théorie des ensembles naïfs du temps polynomial. Studia Logica, vol. 77, n ° 1, pp. 9-40, 2004.

   Je pense que cet article est plus accessible après avoir lu l'article suivant d'Yves Lafont:

   Y. Lafont, Logique linéaire douce et temps polynomial , Informatique théorique 318 (numéro spécial sur la complexité computationnelle implicite) p. 163-180, Elsevier (2004)

   La théorie des ensembles de Terui est très expressive, mais elle est difficile à comparer avec les théories des ensembles traditionnelles, car les ordinaux théoriques de preuve ne sont pas un bon outil pour comparer des systèmes très faibles. Par exemple, la théorie des ensembles de Terui ne peut évidemment pas prouver l'exponentiation totale, et donc sa force de preuve théorique ne peut même pas atteindre . Les classes de complexité sont probablement meilleures - elles sont complètes pour le polytemps (elles peuvent prouver le total de chaque fonction de polytemps, mais pas plus).$\omega$

   J'ai tendance à considérer ces types de systèmes comme des preuves de concept pour l'idée que la théorie de la complexité peut servir de base à certains types d'ultrafinitisme.

Considérez le modèle de machine suivant. La machine avec le code , à l'entrée , sort toujours .x $i$$x$$0$

Notez que toute machine dans ce modèle est universelle, comme pour tous les .$M$M ' , $M(\langle \ulcorner M' \urcorner, x \rangle ) = M'(x) = 0$$M', x$

Ce n'est clairement pas Turing complet, mais il a aussi clairement des machines universelles.