Problema de decisión

En matemáticas e informática , 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. ^[¹^] Requiere un algoritmo que considere una afirmación de entrada y responda «sí» o «no» según sea universalmente válida, es decir, válida en cualquier estructura . Alonzo Church y Alan Turing demostraron en 1936 que tal algoritmo era imposible.

Teorema de completitud

Según el teorema de completitud de la lógica de primer orden , una afirmación es universalmente válida si y solo si puede deducirse utilizando reglas y axiomas lógicos, por lo que el problema de decisión también puede verse como una solicitud de un algoritmo para decidir si una afirmación dada 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 problema de decisión 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 se conoce ahora como la tesis de Church-Turing .

Historia

El origen del problema de decisión se remonta a Gottfried Leibniz , quien en el siglo XVII, tras haber construido una exitosa máquina de calcular mecánica , soñó con construir una máquina que pudiera manipular símbolos para determinar los valores de verdad de las proposiciones matemáticas. ^{[ 3 ]} Comprendió que el primer paso debía ser un lenguaje formal claro , 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 " 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 ]}

Todavía 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 lambda , y Alan Turing al año siguiente con su concepto de máquinas de Turing . Turing reconoció de inmediato que se trataba de modelos de computación equivalentes .

Alonzo Church dio una respuesta negativa al problema de decisión ( en 1935-1936) ( teorema de Church ) y, poco después, Alan Turing lo hizo de forma independiente en 1936 ( prueba de Turing ). Church demostró que no existe ninguna función computable que determine, para dos expresiones dadas del cálculo λ, si son equivalentes o no. Se basó en gran medida en trabajos previos de Stephen Kleene . Turing redujo la cuestión de la existencia de un «algoritmo» o «método general» capaz de resolver el problema de decisión a la cuestión de la existencia de un «método general» que determine si una máquina de Turing dada se detiene o no (el problema de la parada ). Si por «algoritmo» se entiende un método que puede representarse como una máquina de Turing, y dado que la respuesta a esta última pregunta es negativa (en general), la cuestión de la existencia de un algoritmo para el problema de decisión también debe ser negativa (en general). En su artículo de 1936, Turing dice: "Para cada máquina de computación 'it', construimos una fórmula 'Un(it)' y demostramos que, si existe un método general para determinar si 'Un(it)' es demostrable, entonces existe un método general para determinar si 'it' alguna vez imprime 0".

La obra tanto de Church como de Turing estuvo fuertemente influenciada por el trabajo previo 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 problema de decisión está relacionado con el décimo problema de Hilbert , que plantea la necesidad de un algoritmo para determinar si las ecuaciones diofánticas tienen solución. La inexistencia de dicho algoritmo, demostrada por Yuri Matiyasevich , Julia Robinson , Martin Davis y Hilary Putnam con la última parte de la prueba en 1970, implica también una respuesta negativa al problema de decisión .

Generalizaciones

Utilizando el teorema de deducción , el problema de decisión abarca el problema más general de determinar si una sentencia de primer orden dada es una consecuencia lógica de un conjunto finito de sentencias, pero la validez en teorías de primer orden con infinitos axiomas no puede reducirse directamente al problema de decisión . Estos 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 ello son 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 suma y multiplicación expresadas por los axiomas de Peano no puede resolverse mediante un algoritmo.

Fragmentos

Por defecto, las citas en esta sección son de Pratt-Hartmann (2023). ^{[ 7 ]}

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

Algunas anotaciones: ${\rm {{Sat}(\Phi )}}$ significa el problema de decidir si existe un modelo para un conjunto de fórmulas lógicas. $\Phi$ . ${\rm {{FinSat}(\Phi )}}$ es el mismo problema, pero para modelos finitos . ${\rm {Sat}}$ -un problema para un fragmento lógico se llama decidible si existe un programa que puede decidir, para cada $\Phi$ conjunto finito de fórmulas lógicas en el fragmento, ya sea ${\rm {{Sat}(\Phi )}}$ O no.

Existe una jerarquía de decidibilidad. En la cúspide se encuentran los problemas indecidibles. Debajo, los problemas decidibles. Además, los problemas decidibles pueden dividirse en una jerarquía de complejidad.

Aristóteles y relacional

La lógica aristotélica considera cuatro tipos de oraciones: "Todas las p son q", "Todas las p no son q", "Alguna p es q", "Alguna p no es q". Podemos formalizar estos tipos de oraciones como un fragmento de lógica de primer orden: $\forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)$ dónde $p,q$ son predicados atómicos y $+q:=q,\;-q:=\neg q$ Dado un conjunto finito de fórmulas de lógica aristotélica, es NLOGSPACE -completo decidir su ${\rm {Sat}}$ También es NLOGSPACE-completo decidir ${\rm {Sat}}$ para una ligera extensión (Teorema 2.7): $\forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)$ La lógica relacional extiende la lógica aristotélica al permitir un predicado relacional. Por ejemplo, "Todos aman a alguien" se puede escribir como ${\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}$ En general, tenemos 8 tipos de oraciones: ${\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}}$ Es NLOGSPACE -completo para decidir su ${\rm {Sat}}$ (Teorema 2.15). La lógica relacional puede extenderse a 32 tipos de oraciones permitiendo $\pm p,\pm q$ , pero esta extensión es EXPTIME -completa (Teorema 2.24).

Aridad

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

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

prefijo cuantificador

Cualquier 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 , $[\exists ^{*}\forall ^{*}]_{=}$ , es la clase de fórmulas de primer orden con prefijo cuantificador $\exists \cdots \exists \forall \cdots \forall$ , símbolos de igualdad y relación, y ningún símbolo de función .

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

Los límites precisos se conocen con exactitud:

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

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

Procedimientos prácticos de toma de decisiones

Disponer de procedimientos prácticos de decisión 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 se suelen resolver mediante 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 usando el algoritmo simplex , las fórmulas en aritmética lineal entera ( 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 la decisión de conjunciones; generalmente se deciden hoy en día usando 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 polinomial real, 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 usando 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 Sociedad Matemática Estadounidense el 19 de abril de 1935 y publicado el 15 de abril de 1936. Turing, quien había avanzado considerablemente en la redacción de sus propios resultados, se sintió decepcionado al enterarse de la demostración de Church tras su publicación (véase la correspondencia entre Max Newman y Church en los documentos de Alonzo Church ). Turing completó rápidamente su artículo y lo publicó con urgencia; fue recibido por las Actas de la Sociedad Matemática de Londres el 28 de mayo de 1936, leído el 12 de noviembre de 1936 y publicado en la serie 2, volumen 42 (1936-1937); 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), págs. 544-546. Véase la nota a pie de página al final de Soare: 1996.
↑ Davis 2001 , págs. 3–20
↑ Hodges 1983 , pág. 91
↑ Kline, GL; Anovskaa, SA (1951), "Reseña de Fundamentos de matemáticas y lógica matemática de SA Yanovskaya", Journal of Symbolic Logic , 16 (1): 46–48 , doi : 10.2307/2268665 , JSTOR 2268665 , S2CID 119004002
↑ Hodges 1983 , pág. 92 , citando a Hilbert
1 2 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.{{cite book}}: Incompatibilidad de ISBN/Fecha ( ayuda )
Ackermann, Wilhelm (1954). Casos resolubles del problema de decisión . Ámsterdam: North-Holland.
Alonzo Church , "Un problema irresoluble de la teoría elemental de números ", American Journal of Mathematics , 58 (1936), pp. 345-363
Alonzo Church , "Una nota sobre el problema de la decisión", Journal of Symbolic Logic, 1 (1936), pp. 40-41.
Davis, Martin (2001). Motores de la lógica: matemáticos y el origen de la computadora . Edición de bolsillo de Norton (1.ª ed .). Nueva York, NY Londres: Norton. ISBN 978-0-393-32229-3.
Alan Turing , « Sobre los números computables, con una aplicación al problema de decisión », Actas de la Sociedad Matemática de Londres , Serie 2, n.º 42 (1936-1937), págs. 230-265. Versiones en línea: del sitio web de la revista , del Archivo Digital Turing , de abelard.org . Las erratas aparecieron en la Serie 2, n.º 43 (1937), págs. 544-546.
Davis, Martin , «Lo indecidible: Artículos básicos sobre proposiciones indecidibles, problemas irresolubles y funciones computables», 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 un análisis histórico de su demostración y una discusión sobre la misma.
Soare, Robert I. , "Computabilidad y recursión", Bull. Symbolic Logic 2 (1996), n.º 3, 284–321.
Toulmin, Stephen , "La caída de un genio", reseña del libro " Alan Turing: El enigma " de Andrew Hodges, en The New York Review of Books, 19 de enero de 1984, pág. 3 y siguientes.
Whitehead, Alfred North ; Russell, Bertrand , Principia Mathematica hasta *56, Cambridge en University Press, 1962. Re: 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ág. 24 "...dificultades que surgen en la lógica formal", y Cap. 2.I. "El principio del círculo vicioso" pág. 37 y ss., y Cap. 2.VIII. "Las contradicciones" pág. 60 y ss.

Enlaces externos

Definición de entscheidungsproblem en Wikcionario

[1] 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

[2] El artículo de Church fue presentado a la Sociedad Matemática Estadounidense el 19 de abril de 1935 y publicado el 15 de abril de 1936. Turing, quien había avanzado considerablemente en la redacción de sus propios resultados, se sintió decepcionado al enterarse de la demostración de Church tras su publicación (véase la correspondencia entre Max Newman y Church en los documentos de Alonzo Church ). Turing completó rápidamente su artículo y lo publicó con urgencia; fue recibido por las Actas de la Sociedad Matemática de Londres el 28 de mayo de 1936, leído el 12 de noviembre de 1936 y publicado en la serie 2, volumen 42 (1936-1937); 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), págs. 544-546. Véase la nota a pie de página al final de Soare: 1996.

[3] Davis 2001 , págs. 3–20

[4] Hodges 1983 , pág. 91

[Kline-5] Kline, GL; Anovskaa, SA (1951), "Reseña de Fundamentos de matemáticas y lógica matemática de SA Yanovskaya", Journal of Symbolic Logic , 16 (1): 46–48 , doi : 10.2307/2268665 , JSTOR 2268665 , S2CID 119004002

[6] Hodges 1983 , pág. 92 , citando a Hilbert

[:0-7] 1 2 Pratt-Hartmann, Ian (30 de marzo de 2023). Fragmentos de lógica de primer orden . Oxford University Press. ISBN 978-0-19-196006-2.

[8] 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.

[9] 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 .

[10] 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 .

[11] 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.

[

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]