¿Qué sabemos sobre las versiones restringidas del problema de detención?

( ACTUALIZACIÓN : aquí se plantea una pregunta mejor formada ya que los comentarios para la respuesta aceptada a continuación muestran que esta pregunta no está bien definida)

La prueba clásica de la imposibilidad del problema de detención depende de demostrar una contradicción al intentar aplicar el algoritmo de detección de detención a sí mismo como entrada. Consulte los antecedentes a continuación para obtener más información.

La contradicción demostrada se aplica debido a una paradoja autorreferencial (como la oración "Esta oración no es verdadera"). Pero si prohibimos estrictamente tales auto-referencias (es decir, aceptamos el hecho de que tales auto-referencias no pueden detenerse), ¿qué resultado nos queda? ¿Se puede detener o no el problema de detención para el conjunto restante de máquinas sin autorreferencia?

La pregunta es:

Si consideramos un subconjunto de todas las máquinas de Turing posibles, que no son autorreferenciadas (es decir, no se toman como entrada), ¿qué sabemos sobre el problema de detención de este subconjunto?

ACTUALIZAR

Quizás una mejor reformulación de lo que busco es una mejor comprensión de lo que define un conjunto decidible. Estaba tratando de aislar la prueba clásica de indecidibilidad porque no agrega ninguna información sobre la indecidibilidad, excepto en los casos en que ejecuta HALT en sí mismo.

Antecedentes: Suponiendo que existe una contradicción de que hay una máquina Turing $Q$ que puede decidir sobre la entrada $M$ que es una codificación para una máquina Turing y $X$ , independientemente de si $M(X)$ detiene o no . Luego considere una máquina de Turing $K$ que toma $M$ y $X$ y usa $Q$ para decidir si $M(X)$ detiene o no, y luego hace lo contrario, es decir, $K$ detiene si $M(X)$ no se detiene, y no se detiene si $M(X)$ se detiene Entonces $K(K)$ demuestra una contradicción, ya que $K$ debería detenerse si no se detiene, y no se detiene cuando se detiene.

Motivación: un colega está trabajando en la verificación formal de los sistemas de software (especialmente cuando el sistema ya está probado a nivel de código fuente y queremos reprobarlo para su versión compilada, para neutralizar los problemas del compilador), y en su caso se preocupa por un conjunto especial de programas de control integrados para el que sabemos con certeza que no se autoreferenciarán. Un aspecto de la verificación que desea llevar a cabo es si se garantiza que el programa compilado se detendrá si se demuestra que el código fuente de entrada termina.

ACTUALIZAR

En base a los comentarios a continuación, aclaro el significado de las máquinas de Turing sin autorreferencia.

El objetivo es definirlo como el conjunto que no conduce a la contradicción planteada en la prueba (cf. "Antecedentes" arriba). Se podría definir de la siguiente manera:

Suponiendo que hay una máquina Turing que decide el problema de detención para un conjunto de máquinas de Turing , entonces no hace referencia a sí mismo con respecto a si excluye todas las máquinas que invocan en (directa o indirectamente). (Claramente, eso significa que no puede ser miembro de ). $Q$ $S$ $S$ $Q$ $Q$ $S$ $Q$ $S$

Para aclarar qué se entiende al invocar sobre indirectamente: $Q$ $S$

La invocación de en se denota mediante una máquina Turing con un conjunto de estados y ciertas posibles entradas iniciales en la cinta (correspondientes a cualquier miembro de ), con el cabezal inicialmente al comienzo de esa entrada. Una máquina invoca en "indirectamente" si hay una secuencia (finita) de pasos que tomaría para hacer su configuración "homomórfica" a la configuración inicial de . $Q$ $S$ $Q$ $S$ $W$ $Q$ $S$ $W$ $Q(S)$

ACTUALIZACIÓN 2

De una respuesta a continuación que argumenta que hay infinitas máquinas de Turing que realizan la misma tarea, y por lo tanto no es único, cambiamos la definición anterior al decir que no es una sola máquina de Turing, sino el conjunto (infinito) de todas las máquinas que computan la misma función (HALT), donde HALT es la función que decide si una máquina de Turing se detiene en una entrada en particular. $Q$ $Q$

ACTUALIZACIÓN 3

La definición del homomorfismo de la máquina de Turing:

A TM A es homomórfico a TM B si el gráfico de transición de A es homomórfico al de B, en el sentido estándar de homomorfismos de gráficos con nodos etiquetados Y bordes. Un gráfico de transición (V, E) de una TM es tal que V = estados, E = arcos de transición entre estados. Cada arco está etiquetado con el (S, W, D), S = símbolo leído de la cinta y W = el símbolo que se va a escribir en él, y D = la dirección a la que se mueve el espectáculo.

computability lo.logic M. Alaggan
fuente

"el conjunto restante de no autorreferencia" Antes de que pueda discutir este conjunto con sensatez, me gustaría una definición de "autorreferencia". Sin embargo, creo que será algo difícil de definir.

Sam Nead

Hay estudios de programas de detención probables (sin embargo, esta clase no incluye todos los programas de detención). Básicamente son un par de programas y una prueba de que se detiene. Por ejemplo, si no me equivoco, Agda solo permite programas que se detienen. Creo que las personas que trabajan en lenguajes de lógica y programación tienen más que decir al respecto.

Tsuyoshi Ito

@METRO. Alaggan. Ahora me gustaría una definición de "invoca

indirectamente", que sospecho que es tan difícil de definir como la "autorreferencia" original :)

Q

$Q$

S

$S$

Rob Simmons

Esto plantea una pregunta interesante: ¿son todas las pruebas de inconfundibilidad (indecidibilidad) trazables al método de diagonalización de Cantor? ¿Hay alguna prueba de indecidibilidad que no se base directa o indirectamente en el método de diagonalización?

Mohammad Al-Turkistany

Posiblemente preguntas relacionadas: ¿existe una teoría de la complejidad análoga al teorema del arroz en la teoría de la computabilidad? , MO: completitud, problemas más difíciles .

Kaveh

Respuestas:

Creo que tomará un poco más de trabajo llegar a una pregunta "bien definida". En particular, esto es problemático:

La invocación de Q en S se denota mediante una máquina Q de Turing con un conjunto de estados y ciertas posibles entradas iniciales en la cinta (correspondientes a cualquier miembro de S), con el cabezal inicialmente al comienzo de esa entrada. Una máquina W invoca Q en S "indirectamente" si hay una secuencia (finita) de pasos que W tomaría para hacer su configuración "homomórfica" a la configuración inicial de Q (S).

Un problema es que hay infinitas máquinas de Turing que calculan la misma función. En el argumento de diagonalización estándar, puedo reemplazar la subrutina Q con otro decisor para HALT, ya que hay infinitos de ellos. O una función que es computablemente equivalente a HALT. Por lo tanto, no está del todo claro para mí cómo definir su noción de "invocación indirecta".

Una pregunta diferente podría ser: ¿para qué conjuntos de máquinas de Turing es decidible el problema de detención? Aquí hay una gran cantidad de respuestas: TM restringidas de recursos (por ejemplo, use solo espacio f (n), donde f es alguna función computable específica), TM que están operacionalmente restringidas de alguna manera en particular (por ejemplo, el cabezal de lectura solo se mueve en una dirección), etc. Pero, otra pregunta interesante es si la membresía en ese conjunto restringido es decidible, o si tiene que restringirse a "problemas de promesa", donde solo garantiza una respuesta correcta en algún subconjunto de entradas "prometidas", pero no verifica afiliación.

Mark Reitblatt
fuente

Q

$Q$

H

$H$

No es tan simple. Su definición es paradójica ahora, ya que está buscando un HALT computable. Pero si esto es computable, cualquier función computable es computablemente equivalente a ella. Pero si su conjunto de entrada contenía problemas semi-computables (TM), tendría una contradicción ya que decidir el problema de detención para tal TM le daría un procedimiento de decisión para ese problema.

Mark Reitblatt el

1) ¿No significaría una HALT inconfundible la indecidibilidad? Estaba suponiendo que existe una HALT computable, esperando contradicciones. 2) No estoy familiarizado con el concepto de que todas las funciones computables sean equivalentes de manera computacional entre sí, lo estaba citando, y lo que significa que es una función que resuelve el problema de HALT. Aparentemente, λx.1 es computable pero no decide HALT. Corrígeme si me equivoco, por favor. Acerca de los problemas semi-computables, HALT puede tomar un número infinito de pasos, lo que aún no conduciría a una contradicción en la prueba original de que HALT no es decidible.

M. Alaggan el

1) correcto. Pero el problema es tratar de definir su noción de "no autorreferencia". O bien es una restricción débil, que permite la diagonalización como dije, o es una restricción fuerte que elimina todo. 2) es simple. "Computablemente equivalente" significa aproximadamente que hay un mapeo computable de uno a otro que conserva las respuestas. Pero si puedo calcular una respuesta, puedo hacer trampa y hacer que el mapeo sea trivial. 3) Si el TM que decide HALT no termina por sí mismo, no es un factor decisivo para HALT.

Mark Reitblatt el

Otra cosa que es un poco confusa es la combinación de TM con el problema de decisión calculado por ellos. No es normal hablar de que una TM sea computacionalmente equivalente entre sí. Por el contrario, las funciones calculadas por ellos pueden ser equivalentes (o iguales). El problema es que tratar de decir que una TM no simula otra TM es difícil de definir en general, sin dar algo concreto para separar las funciones calculadas por ellos. Por ejemplo, un Log-space TM no puede simular a un TM resolviendo un problema de EXP-space.

Mark Reitblatt el

Si entiendo su motivación correctamente, parece que este es un problema de "corrección del compilador" más que un problema de "problema de detención restringida". Tiene una propiedad (terminación) que ha probado para algún programa Prog de nivel de origen que desea extender al código compilado para obtener la misma propiedad de compilado (Prog) . Pero el compilador puede (en general) hacer cosas arbitrariamente tontas como implementar un tiempo de ejecución completo (por ejemplo, JVM), compilar su programa de terminación en un código de bytes JVM y luego descargar un ejecutable que inicie el JVM y lo alimente con su código de bytes compilado.

En la práctica , es probable que sea posible utilizar el conocimiento implícito que tiene sobre cómo funciona su compilador para implementar algún procedimiento de verificación que demuestre que los programas compilados son correctos dados los programas fuente correctos (de hecho, muchas herramientas de verificación automática para programas están utilizando conocimiento implícito del "compilador" de algoritmo a código en los cerebros de los programadores). Sin embargo, en general probablemente estés viendo un problema de corrección del compilador. Según tengo entendido, hay dos formas clásicas de hacerlo.

Una opción es tener un compilador que tome como entrada el programa Prog y la prueba termina (Prog) y las salidas compiladas (Prog) y termina (compiladas (Prog)) ; esta última es una prueba que luego se puede verificar dos veces independientemente de El compilador. El artículo clásico sobre esto es Necula y Lee. El diseño y la implementación de un compilador certificador , creo.

Alternativamente, puede probar un hecho sobre la función compiles () , que cada vez que compiles () está dando una entrada de terminación produce una salida de terminación. Una introducción accesible a esta forma de pensar sobre la corrección del compilador es el artículo CACM de Xavier Leroy, Verificación formal de un compilador realista .

(PD: Espero que esta respuesta sea útil; reconozco que es un poco divergente de la pregunta que hizo, así que avíseme si estoy fuera de lugar y / o repito algo que ya sabe).

Rob Simmons
fuente

Gracias por la gran respuesta. Esto definitivamente sería útil para mi colega. Sin embargo, (independientemente de mi colega) estoy más interesado en las implicaciones teóricas sobre la prueba del problema de detención, que si nos deshacemos del caso que mostró la contradicción, ¿qué más sabemos sobre la capacidad de resolución del problema de detención?

M. Alaggan el