Problema de resolución de problemas

En matemáticas y ciencias de la computación , el Entscheidungsproblem ( en alemán , "problema de decisión"; pronunciado [ɛntˈʃaɪ̯dʊŋspʁoˌbleːm] ) es un desafío planteado por David Hilbert y Wilhelm Ackermann en 1928. ^[1] Pide un algoritmo que considere una declaración ingresada y responda "sí" o "no" según sea universalmente válida, es decir, válida en todas las estructuras . Alonzo Church y Alan Turing demostraron que un algoritmo de este tipo era imposible en 1936.

Teorema de completitud

Según el teorema de completitud de la lógica de primer orden , un enunciado es universalmente válido si y sólo si puede deducirse utilizando reglas lógicas y axiomas, por lo que el Entscheidungsproblem también puede verse como la búsqueda de un algoritmo para decidir si un enunciado dado es demostrable utilizando las reglas de la lógica .

En 1936, Alonzo Church y Alan Turing publicaron artículos independientes ^[2] que demostraban que una solución general al Entscheidungsproblem es imposible, suponiendo que la noción intuitiva de " efectivamente calculable " está capturada 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

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

Continuando con su "programa", Hilbert planteó tres cuestiones en una conferencia internacional en 1928, la tercera de las cuales se conocería como " El problema de decisión de Hilbert ". ^[4] En 1929, Moses Schönfinkel publicó un artículo sobre casos especiales del problema de decisión, que fue preparado por Paul Bernays . ^[5]

Incluso en 1930, Hilbert creía que no existiría ningún problema irresoluble. ^[6]

Respuesta negativa

Antes de poder responder a la pregunta, era necesario definir formalmente el concepto de "algoritmo". Esto lo hizo Alonzo Church en 1935 con el concepto de "calculabilidad efectiva" basado en su cálculo λ , y Alan Turing al año siguiente con su concepto de máquinas de Turing . Turing reconoció inmediatamente que se trataba de modelos equivalentes de computación .

En 1935-36, Alonzo Church dio una respuesta negativa al Entscheidungsproblem ( teorema de Church ) y, poco después, de forma independiente, Alan Turing en 1936 ( prueba de Turing ). Church demostró que no existe una función computable que decida, para dos expresiones dadas de cálculo λ, si son equivalentes o no. Se basó en gran medida en trabajos anteriores 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 decida si una máquina de Turing dada se detiene o no (el problema de la detención ). Si se entiende por «algoritmo» un método que puede representarse como una máquina de Turing, y con la respuesta a la última pregunta negativa (en general), la pregunta sobre la existencia de un algoritmo para el Entscheidungsproblem también debe ser negativa (en general). En su artículo de 1936, Turing dice: "Correspondiente a cada máquina de computación 'it' construimos una fórmula 'Un(it)' y mostramos que, si hay 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 de 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 aritmética.

El problema de Entscheidung 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, establecido 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 problema de Entscheidung .

Generalizaciones

Utilizando el teorema de deducción , el Entscheidungsproblem abarca el problema más general de decidir si una oración de primer orden dada está implicada por un conjunto finito dado de oraciones, pero la validez en teorías de primer orden con infinitos axiomas no puede reducirse directamente al Entscheidungsproblem. Tales problemas de decisión más generales son de interés práctico. Algunas teorías de primer orden son decidibles algorítmicamente ; ejemplos de esto incluyen la aritmética de Presburger , los cuerpos reales cerrados y los sistemas de tipos estáticos de muchos lenguajes de programación . Por otro lado, la teoría de primer orden de los números naturales con adición y multiplicación expresada por los axiomas de Peano no puede decidirse con un algoritmo.

Fragmentos

De forma predeterminada, las citas en la sección son de Pratt-Hartmann (2023). ^[7]

El problema clásico de Entscheidungsproblem plantea la pregunta de si, dada una fórmula de primer orden, es verdadera en todos los modelos. El problema finitario plantea la pregunta de si es verdadera en todos los modelos finitos. El teorema de Trakhtenbrot muestra que esto también es indecidible. ^[8]^[7]

Algunas notaciones: significa el problema de decidir si existe un modelo para un conjunto de fórmulas lógicas . es el mismo problema, pero para modelos finitos . El problema de un fragmento lógico se llama decidible si existe un programa que puede decidir, para cada conjunto finito de fórmulas lógicas en el fragmento, si existe o no. ${\rm {{sábado}(\Phi )}}$ ${\estilo de visualización \Phi}$ ${\rm {{FinSat}(\Phi )}}$ ${\rm {sábado}}$ ${\estilo de visualización \Phi}$ ${\rm {{sábado}(\Phi )}}$

Existe una jerarquía de decidibilidades. En la parte superior se encuentran los problemas indecidibles. Debajo de ellos se encuentran los problemas decidibles. Además, los problemas decidibles se pueden dividir en una jerarquía de complejidad.

Aristotélico y relacional

La lógica aristotélica considera 4 tipos de oraciones: "Todos los p son q", "Todos los p no son q", "Algunos p son q", "Algunos p no son q". Podemos formalizar estos tipos de oraciones como un fragmento de lógica de primer orden: donde son predicados atómicos, y . Dado un conjunto finito de fórmulas lógicas aristotélicas, es NLOGSPACE -completo decidir su . También es NLOGSPACE-completo decidir para una ligera extensión (Teorema 2.7): La lógica relacional extiende la lógica aristotélica al permitir un predicado relacional. Por ejemplo, "Todo el mundo ama a alguien" se puede escribir como . En general, tenemos 8 tipos de oraciones: Es NLOGSPACE -completo decidir su (Teorema 2.15). La lógica relacional se puede extender a 32 tipos de oraciones al permitir , pero esta extensión es EXPTIME -completa (Teorema 2.24). $\para todo x,p(x)\a \pm q(x),\quad \existe x,p(x)\wedge \pm q(x)$ ${\estilo de visualización p,q}$ $+q:=q,\;-q:=\neg q$ ${\rm {Sat}}$ ${\rm {Sat}}$ $\forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)$ ${\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}$ ${\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}$ ${\rm {Sat}}$ $\pm p,\pm q$

Aridad

El fragmento de lógica de primer orden donde los únicos nombres de variable son es NEXPTIME -completo (Teorema 3.18). Con , es RE -completo decidir su , y co-RE-completo decidir (Teorema 3.15), por lo tanto indecidible. $x,y$ $x,y,z$ ${\rm {Sat}}$ ${\rm {FinSat}}$

El cálculo de predicados monádicos es el fragmento en el que cada fórmula contiene solo predicados 1-arios y ningún símbolo de función. Es NEXPTIME-completo (Teorema 3.22). ${\rm {Sat}}$

Prefijo cuantificador

Toda fórmula de primer orden tiene una forma normal prenexa. Para cada posible prefijo cuantificador de la forma normal prenexa, tenemos un fragmento de lógica de primer orden. Por ejemplo, la clase de Bernays–Schönfinkel , , es la clase de fórmulas de primer orden con prefijo cuantificador , símbolos de igualdad y sin símbolos de función . $[\exists ^{*}\forall ^{*}]_{=}$ $\exists \cdots \exists \forall \cdots \forall$

Por ejemplo, el artículo de Turing de 1936 (p. 263) observó que, dado que el problema de detención de cada máquina de Turing es equivalente a una fórmula lógica de primer orden de forma , el problema es indecidible. $\forall \exists \forall \exists ^{6}$ ${\rm {{Sat}(\forall \exists \forall \exists ^{6})}}$

Los límites precisos se conocen claramente:

${\rm {{Sat}(\forall \exists \forall )}}$ y son co-RE-completos, y los problemas son RE-completos (Teorema 5.2). ${\rm {{Sat}([\forall \exists \forall ]_{=})}}$ ${\rm {FinSat}}$
Lo mismo ocurre con el Teorema 5.3. $\forall ^{3}\exists$
$\exists ^{*}\forall ^{2}\exists ^{*}$ es decidible, como lo demostraron independientemente Gödel, Schütte y Kalmár.
$[\forall ^{2}\exists ]_{=}$ es indecidible.
Para cualquier , tanto como son NEXPTIME-completos (Teorema 5.1). $n\geq 0$ ${\rm {{Sat}(\exists ^{n}\forall ^{*})}}$ ${\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}$
- Esto implica que es decidible, un resultado publicado por primera vez por Bernays y Schönfinkel. ^[9] ${\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}$
Para cualquier , es EXPTIME-completo (Sección 5.4.1). $n\geq 0,m\geq 2$ ${\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}$
Para cualquier , es NEXPTIME-completo (Sección 5.4.2). $n\geq 0$ ${\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}$
- Esto implica que es decidible, un resultado publicado por primera vez por Ackermann. ^[10] ${\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}$
Para cualquier , y son PSPACE-completos (Sección 5.4.3). $n\geq 0$ ${\rm {{Sat}(\exists ^{n}\forall \exists )}}$ ${\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}$

Börger et al. (2001) ^[11] describe el nivel de complejidad computacional para cada fragmento posible con cada combinación posible de prefijo cuantificador, aridad funcional, aridad predicada e igualdad/no igualdad.

Procedimientos prácticos de decisión

Disponer de procedimientos prácticos de decisión para clases de fórmulas lógicas es de considerable interés para la verificación de programas y circuitos. Las fórmulas lógicas booleanas puras se suelen decidir utilizando técnicas de resolución SAT basadas en el algoritmo DPLL .

Para problemas de decisión más generales de teorías de primer orden, las fórmulas conjuntivas sobre aritmética lineal real o racional se pueden decidir utilizando el algoritmo simplex , las fórmulas en aritmética lineal entera ( aritmética de Presburger ) se pueden decidir utilizando el algoritmo de Cooper o la prueba Omega de William Pugh . Las fórmulas con negaciones, conjunciones y disyunciones combinan las dificultades de las pruebas de satisfacibilidad con las de la decisión de 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 la teoría de cuerpos cerrados reales , es decidible; este es el teorema de Tarski-Seidenberg , que se ha implementado en computadoras utilizando la descomposición algebraica cilíndrica .

Véase también

Notas

^ David Hilbert y Wilhelm Ackermann. Grundzüge der Theoretischen Logik. Springer, Berlín, Alemania, 1928. Traducción al inglés: David Hilbert y Wilhelm Ackermann. Principios de la lógica matemática. AMS Chelsea Publishing, Providence, Rhode Island, EE. UU., 1950
^ El artículo de Church fue presentado a la American Mathematical Society el 19 de abril de 1935 y publicado el 15 de abril de 1936. Turing, que había hecho un progreso sustancial en la redacción de sus propios resultados, se sintió decepcionado al enterarse de la prueba de Church tras su publicación (véase la correspondencia entre Max Newman y Church en los artículos de Alonzo Church). Turing completó rápidamente su artículo y se apresuró a publicarlo; fue recibido por las Actas de la London Mathematical Society el 28 de mayo de 1936, leído el 12 de noviembre de 1936 y publicado en la serie 2, volumen 42 (1936-7); apareció en dos secciones: en la Parte 3 (páginas 230-240), publicada el 30 de noviembre de 1936 y en la Parte 4 (páginas 241-265), publicada el 23 de diciembre de 1936; Turing añadió correcciones en el volumen 43 (1937), pp. 544-546. Véase la nota al final de Soare: 1996.
^ Davis 2001, págs. 3-20
^ Hodges 1983, pág. 91
^ Kline, GL; Anovskaa, SA (1951), "Revisión de Fundamentos de las matemáticas y la lógica matemática por SA Yanovskaya", Journal of Symbolic Logic , 16 (1): 46–48, doi :10.2307/2268665, JSTOR 2268665, S2CID 119004002
^ Hodges 1983, p. 92, citando a Hilbert
^ ab Pratt-Hartmann, Ian (30 de marzo de 2023). Fragmentos de lógica de primer orden. Oxford University Press. ISBN 978-0-19-196006-2.
^ B. Trakhtenbrot. La imposibilidad de un algoritmo para el problema de decisión para modelos finitos . Doklady Akademii Nauk, 70:572–596, 1950. Traducción al inglés: AMS Translations Series 2, vol. 33 (1963), pp. 1–6.
^ Bernays, Pablo; Schönfinkel, Moisés (diciembre de 1928). "Zum Entscheidungsproblem der mathematischen Logik". Mathematische Annalen (en alemán). 99 (1): 342–372. doi :10.1007/BF01459101. ISSN 0025-5831. S2CID 122312654.
^ Ackermann, Wilhelm (1 de diciembre de 1928). "Über die Erfüllbarkeit gewisser Zählausdrücke". Mathematische Annalen (en alemán). 100 (1): 638–649. doi :10.1007/BF01448869. ISSN 1432-1807. S2CID 119646624.
^ Börger, Egon; Grädel, Erich; Gurevič, Jurij; Gurevich, Yuri (2001). El problema de decisión clásico . Universitext (2. impresión de la 1. ed.). Berlín: Springer. ISBN 978-3-540-42324-9.

Referencias

Hilbert, David ; Ackermann, Wilhelm (1928). Grundzüge der theoretischen Logik [ Principios de lógica matemática ] (en alemán). Springer-Verlag . ISBN 0821820249.
Alonzo Church , "Un problema irresoluble de la teoría de números elementales ", American Journal of Mathematics, 58 (1936), pp 345–363
Alonzo Church , "Una nota sobre el Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), págs. 40-41.
Davis, Martin (2001). Motores de lógica: matemáticos y el origen de la computadora . Norton paperback (1.ª edición publicada como Norton paperback ed.). Nueva York, NY Londres: Norton. ISBN 978-0-393-32229-3.
Alan Turing , " Sobre números computables, con una aplicación al problema de la endoscopia ", Actas de la London Mathematical Society , Serie 2, 42 (1936-1937), pp. 230-265. Versiones en línea: del sitio web de la revista, del Turing Digital Archive, de abelard.org. Las erratas aparecieron en la Serie 2, 43 (1937), pp. 544-546.
Davis, Martin , "The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions", Raven Press, Nueva York, 1965. El artículo de Turing es el número 3 de este volumen. Entre los artículos se incluyen los de Gödel, Church, Rosser, Kleene y Post.
Hodges, Andrew (1983). Alan Turing: el enigma . Nueva York: Simon and Schuster. ISBN 978-0-671-49207-6.Biografía de Alan M. Turing. Véase el capítulo "El espíritu de la verdad" para conocer la historia que condujo a su demostración y su análisis.
Soare, Robert I. , "Computabilidad y recursión", Bull. Symbolic Logic 2 (1996), núm. 3, 284–321.
Toulmin, Stephen , "La caída de un genio", reseña del libro " Alan Turing: The Enigma de Andrew Hodges", en The New York Review of Books, 19 de enero de 1984, pág. 3ff.
Whitehead, Alfred North ; Russell, Bertrand , Principia Mathematica to *56, Cambridge at the University Press, 1962. En relación con el problema de las paradojas, los autores discuten el problema de que un conjunto no sea un objeto en ninguna de sus "funciones determinantes", en particular "Introducción, Cap. 1 p. 24 "...dificultades que surgen en la lógica formal", y Cap. 2.I. "El principio del círculo vicioso" p. 37ff, y Cap. 2.VIII. "Las contradicciones" p. 60 ff.

Enlaces externos

La definición del diccionario de entscheidungsproblem en Wikcionario