Entscheidungsproblema

En matemáticas e informática, el Entscheidungsproblem (pronunciado [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm], alemán para &# 39;problema de decisión') es un desafío planteado por David Hilbert y Wilhelm Ackermann en 1928. El problema pide un algoritmo que considere, como entrada, una declaración y responda "Sí" o "No" según si el enunciado es universalmente válido, es decir, válido en toda estructura que satisfaga los axiomas.

Teorema de completitud

Según el teorema de completitud de la lógica de primer orden, un enunciado es universalmente válido si y solo si puede deducirse de los axiomas, por lo que Entscheidungsproblem también puede verse como pedir un algoritmo para decidir si una declaración dada es comprobable a partir de los axiomas usando las reglas de la lógica.

En 1936, Alonzo Church y Alan Turing publicaron artículos independientes que mostraban que una solución general al Entscheidungsproblem es imposible, asumiendo que la noción intuitiva de "efectivamente calculable" es capturado por las funciones computables por una máquina de Turing (o equivalentemente, por aquellas expresables en el cálculo lambda). Esta suposición ahora se conoce como la tesis de Church-Turing.

Historia del problema

El origen del Entscheidungsproblem se remonta a Gottfried Leibniz, quien en el siglo XVII, después de haber construido una máquina calculadora mecánica exitosa, soñaba con construir una máquina que pudiera manipular símbolos para determinar los valores de verdad de las declaraciones matemáticas. Se dio cuenta de que el primer paso tendría que ser un lenguaje formal limpio, y gran parte de su trabajo posterior se dirigió hacia ese objetivo. En 1928, David Hilbert y Wilhelm Ackermann plantearon la pregunta en la forma descrita anteriormente.

Como continuación de su "programa", Hilbert planteó tres preguntas en una conferencia internacional en 1928, la tercera de las cuales se conoció como "Hilbert's Entscheidungsproblem". En 1929, Moses Schönfinkel publicó un artículo sobre casos especiales del problema de decisión, que fue preparado por Paul Bernays.

Hasta 1930, Hilbert creía que no existirían los problemas irresolubles.

Respuesta negativa

Antes de que se pudiera responder a la pregunta, la noción de "algoritmo" había que definirlo formalmente. Esto fue hecho por Alonzo Church en 1935 con el concepto de "calculabilidad efectiva" basado en su cálculo λ, y por Alan Turing al año siguiente con su concepto de máquinas de Turing. Turing reconoció de inmediato que estos son modelos equivalentes de computación.

La respuesta negativa al Entscheidungsproblem fue dada por Alonzo Church en 1935-1936 ( el teorema de Church) e independientemente poco después por Alan Turing en 1936 (la prueba de Turing). Church demostró que no existe una función computable que decida, para dos expresiones de cálculo λ dadas, si son equivalentes o no. Se basó en gran medida en el trabajo anterior de Stephen Kleene. Turing redujo la cuestión de la existencia de un 'algoritmo' o 'método general' capaz de resolver el Entscheidungsproblem a la cuestión de la existencia de un 'método general' que decide si una determinada máquina de Turing se detiene o no (el problema de la detención). Si 'algoritmo' se entiende en el sentido de un método que se puede representar como una máquina de Turing, y con la respuesta a esta última pregunta negativa (en general), la pregunta sobre la existencia de un algoritmo para el Entscheidungsproblem también debe ser negativo (en general). En su artículo de 1936, Turing dice: "Correspondiendo a cada máquina de computación 'it' construimos una fórmula 'Un(it)' y mostramos que, si existe un método general para determinar si 'Un(it)' es demostrable, entonces hay un método general para determinar si 'it' alguna vez imprime 0".

El trabajo de Church y Turing estuvo fuertemente influenciado por el trabajo anterior de Kurt Gödel sobre su teorema de incompletitud, especialmente por el método de asignar números (una numeración de Gödel) a fórmulas lógicas para reducir la lógica a la aritmética.

El Entscheidungsproblem está relacionado con el décimo problema de Hilbert, que pide un algoritmo para decidir si las ecuaciones diofánticas tienen solución. La inexistencia de dicho algoritmo, establecida por el trabajo de Yuri Matiyasevich, Julia Robinson, Martin Davis y Hilary Putnam, con la pieza final de la prueba en 1970, también implica una respuesta negativa al Entscheidungsproblem. yo>.

Algunas teorías de primer orden son algorítmicamente decidibles; ejemplos de esto incluyen la aritmética de Presburger, campos cerrados reales y sistemas de tipo estático de muchos lenguajes de programación. Sin embargo, la teoría general de primer orden de los números naturales expresada en los axiomas de Peano no puede decidirse con un algoritmo.

Procedimientos de decisión práctica

Tener procedimientos de decisión prácticos para clases de fórmulas lógicas es de gran interés para la verificación de programas y circuitos. Las fórmulas lógicas booleanas puras generalmente se deciden utilizando técnicas de resolución de SAT basadas en el algoritmo DPLL. Las fórmulas conjuntivas sobre aritmética lineal real o racional se pueden decidir usando el algoritmo simplex, las fórmulas en aritmética entera lineal (aritmética de Presburger) se pueden decidir usando el algoritmo de Cooper o la prueba Omega de William Pugh. Las fórmulas con negaciones, conjunciones y disyunciones combinan las dificultades de la prueba de satisfacibilidad con la de decisión de las conjunciones; generalmente se deciden hoy en día utilizando técnicas de resolución SMT, que combinan la resolución SAT con procedimientos de decisión para conjunciones y técnicas de propagación. La aritmética de polinomios reales, también conocida como teoría de campos cerrados reales, es decidible; este es el teorema de Tarski-Seidenberg, que ha sido implementado en computadoras usando la descomposición algebraica cilíndrica.