¿Existe un modelo de cómputo no completo de Turing cuyo problema de detención sea indecidible?

26

No puedo pensar en ningún modelo de este tipo, ¿tal vez alguna forma de cálculo lambda mecanografiado? algún autómata celular elemental?

Esto casi refutaría el "Principio de equivalencia computacional" de Wolfram:

Casi todos los procesos que obviamente no son simples pueden verse como cálculos de sofisticación equivalente

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

Respuestas:

18

Puede construir fácilmente modelos artificiales que no están completos, pero el problema para ellos es indecidible. Por ejemplo, tome todas las TM que no se detienen en nada más que .0

Con respecto a la declaración:

No puede refutar una declaración que no sea lo suficientemente precisa. Casi ninguna de las palabras en la declaración está bien definida (proporcione la definición para ellas si este no es el caso).

Kaveh
fuente
mmm, digamos que un modelo está completo de Turing si puede simular un UTM.
Diego de Estrada
1
Creo que el principio de equivalencia de Wolfram está más cerca de la física que de la lógica. Parece que a los lógicos les gusta atacarlo por varias razones: no es preciso, no se ha probado, podemos arreglar las cosas para que sea falso, etc. Pero, de hecho, Wolfram señala, a su manera, un hecho muy interesante sobre la computación , ya que surge "en la naturaleza".
Andrej Bauer
1
No sé sobre la selección de cerezas, el libro me parece bastante completo, especialmente todas esas notas. ¿Existe alguna razón a priori para no permitir cambios de definiciones estándar? Estás midiendo con el criterio equivocado aquí. Wolfram no está haciendo matemáticas, al menos no en el sentido tradicional de la palabra.
Andrej Bauer
44
@Andrej, mi principal problema es que la declaración es tan vaga que no veo cómo puede hacer predicciones verificables / refutables. Y sí, si alguien está cambiando las definiciones estándar solo para poder interpretar lo que no sería un soporte para un reclamo como un soporte para el reclamo, entonces creo que es problemático.
Kaveh
44
La afirmación es vaga, pero ¿y qué? No es lógica ni matemáticas. Es una observación, respaldada por un grueso libro lleno de ejemplos, que en la naturaleza los "sistemas computacionales" tienden a ser trivialmente simples o extremadamente sofisticados y "equivalentes" entre sí. En lugar de criticar a Wolfram por no hablar la jerga de la lógica y las matemáticas, sería más productivo ver que tiene un punto, y luego formular ese punto en cualquier formalismo que desee su corazón. Pero, por supuesto, si tu corazón no desea tal cosa, entonces no lo harás.
Andrej Bauer
4

Estoy bastante seguro de que el argumento de diagonalización se aplica a cualquier modelo de cálculo que:

  • puede representarse a sí mismo como una cadena, y
  • puede simular otra máquina, dada la representación anterior

Si tuviéramos un modelo que violara una de las condiciones anteriores, su poder computacional sería extremadamente limitado.

gabgoh
fuente
10
∀x.f(x)≠X
2

No estoy seguro de la conexión exacta, pero esto parece estar relacionado con el teorema de Friedberg-Muchnik (ver aquí ): hay un restablecimiento cuyo grado de Turing es menor que el problema de detención. Este resultado respondió una pregunta influyente de Post y condujo a la introducción del "método de prioridad" en la calculabilidad.

Super0
fuente
-2

Probablemente. Hay muchos problemas matemáticos que probablemente incluyen algunos entre ellos, que son indecidibles, es decir, la respuesta es "sí" pero no existe prueba de ello. Por ejemplo, el problema Collatz 3x + 1 me viene a la mente como candidato. O la pregunta de si pi contiene cadenas arbitrariamente largas de 9s consecutivos. Cualquier problema de este tipo podría considerarse como un "modelo de cómputo", presumiblemente mucho menos poderoso que un UTM, pero aún sería indecidible si "se detiene" o si "siempre se detiene".

Warren D. Smith
fuente
No creo que este enfoque pueda funcionar. Ver: para cualquier enunciado fijo, existe un algoritmo que decide si es "verdadero" o "falso" en un período de tiempo limitado, incluso cuando es indecidible en ZFC (ref: en.wikipedia.org/wiki/Busy_beaver # Aplicaciones ). Por otro lado, si considera como modelo de cómputo el problema "dada una declaración, decida si tiene una prueba en ZFC", creo que ese modelo es completo de Turing.
Diego de Estrada