Si una máquina abstracta puede simularse, ¿eso hace que Turing se complete?

Por ejemplo, en los lenguajes de programación es común escribir un compilador / intérprete X-in-X, pero en un nivel más general, muchos sistemas completos de Turing conocidos pueden simularse de formas impresionantes (por ejemplo, simulando el Juego de la vida de Conway en el Juego de la vida de Conway). )

Entonces, mi pregunta es: ¿es un sistema capaz de simularse lo suficiente como para demostrar que está Turing completo? Ciertamente es una condición necesaria.

No necesariamente. Por ejemplo, el autómata celular de bloque bidimensional con dos estados, en el que una célula se activa solo cuando sus cuatro predecesores tienen exactamente dos células vivas adyacentes, puede simularse con un factor de dos desaceleración y un factor de explosión de dos tamaños, pero No se sabe que Turing esté completo. Para más información sobre este autómata de bloque y sobre la regla B36 / S125 para el vecindario de Moore, que también es capaz de simular este autómata de bloque, consulte el Autómata celular realista similar a B36 / S125 "2x2" de Nathaniel Johnston.

No, no es. Conozco dos clases principales de técnicas para evitar inconsistencias / integridad de Turing.

1. La primera línea de ataque es configurar el sistema para que la sintaxis se pueda aritmetizar, pero el teorema del punto fijo de Godel no se cumple. Dan Willard ha trabajado mucho en esto y ha dado sistemas lógicos de autoverificación consistentes. El truco consiste en eliminar los símbolos de la función de multiplicación y suma, y ​​reemplazarlos con divisibilidad y resta. Esto le da suficiente potencia para representar la sintaxis aritméticamente, pero el teorema del punto fijo no se cumple, ya que la multiplicación no es demostrablemente total.

   Ver Dan Willard. Sistemas de autoverificación de axiomas, el teorema de incompletitud y principios de reflexión relacionados . Journal of Symbolic Logic 66 (2001) págs. 536-596.

2. La segunda línea de ataque permite un mayor uso de puntos fijos, pero para configurar las cosas para que la sintaxis no aritmetice. Los sistemas más bonitos para esto son (IMO) basados ​​en variantes de lógica lineal. Por ejemplo, en la teoría de conjuntos afines a la luz de Kazushige Terui, incluso el principio de comprensión de conjuntos sin restricciones es sólido, pero dado que la lógica ambiental de la teoría de conjuntos es lineal (y, por lo tanto, no se permite la contracción), la paradoja de Russell no es derivable.

   La razón intuitiva por la que falla la aritmetización es que el espacio de función lineal de luz está configurado de modo que todos sus habitantes sean tiempo polinomial. Como resultado, la versión lineal ligera de los axiomas de Peano no puede probar la exponenciación total (ya que la exponenciación de números unarios toma tiempo exponencial), por lo que ya no hay un isomorfismo entre los números naturales y las cadenas de bits.$A \multimap B$

   Kazushige Terui. Teoría de conjuntos afín ligera: una teoría de conjuntos ingenua del tiempo polinomial. Studia Logica, vol. 77, núm. 1, págs. 9-40, 2004.

   Creo que este documento es más accesible después de leer el siguiente documento de Yves Lafont:

   Y. Lafont, Soft Linear Logic and Polynomial Time , Theoretical Computer Science 318 (número especial sobre Complejidad computacional implícita) p. 163-180, Elsevier (2004)

   La teoría de conjuntos de Terui es muy expresiva, pero es difícil de comparar con las teorías de conjuntos tradicionales, ya que los ordinales teóricos de prueba no son una buena herramienta para comparar sistemas muy débiles. Por ejemplo, la teoría de conjuntos de Terui obviamente no puede probar la exponenciación total y, por lo tanto, su fuerza teórica de prueba ni siquiera puede alcanzar hasta . Las clases de complejidad son probablemente mejores: está completa para polytime (puede probar el total de todas las funciones de polytime, pero no más).$\omega$

   Tiendo a pensar en este tipo de sistemas como pruebas de concepto de la idea de que la teoría de la complejidad puede servir como base para ciertos tipos de ultrafinitismo.

Considere el siguiente modelo de máquina. La máquina con el código , en la entrada x , emite 0 siempre$i$$x$$0$

Tenga en cuenta que cualquier máquina en este modelo es universal, como M ( ⟨ ⌜ M ' ⌝ , x ⟩ ) = M ' ( x ) = 0 para todos los M ' , x .$M$$M(\langle \ulcorner M' \urcorner, x \rangle ) = M'(x) = 0$$M', x$

Claramente, esto no es completo para Turing, pero también tiene máquinas universales.