problema de entscheidung

Tarea imposible en informática

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. ^[1] El problema pide un algoritmo que considere, como entrada, una enunciado y responde “sí” o “no” según si el enunciado es universalmente válido , es decir, válido en toda estructura .

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 se puede deducir utilizando reglas y axiomas lógicos, por lo que también se puede considerar que el problema de Entscheidungs ​​pide un algoritmo para decidir si un enunciado determinado es demostrable utilizando las reglas de la lógica .

En 1936, Alonzo Church y Alan Turing publicaron artículos independientes ^[2] que mostraban que una solución general al problema de Entscheidungs ​​es imposible, suponiendo que la noción intuitiva de " efectivamente calculable " sea capturada por las funciones computables por una máquina de Turing (o equivalentemente, por los expresables en el cálculo lambda ). Esta suposición se conoce ahora 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 con éxito una máquina calculadora mecánica , soñaba 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 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 Entscheidungsproblem 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 un problema sin solución. ^[6]

Respuesta negativa

Antes de poder responder a la pregunta, era necesario definir formalmente la noción 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 trata de modelos de computación equivalentes .

Luego, Alonzo Church dio una respuesta negativa al problema de Entscheidungs ​​en 1935-1936 ( 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 de cálculo λ dadas, 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 determinada máquina de Turing se detiene o no (el problema de la detención ). Si por "algoritmo" se entiende un método que puede representarse como una máquina de Turing, y si la respuesta a esta última pregunta es negativa (en general), la pregunta sobre la existencia de un algoritmo para el Entscheidungsproblem también debe ser negativa (en general). general). En su artículo de 1936, Turing dice: "Para cada máquina informática '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".

El trabajo tanto de Church como 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 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 tal algoritmo, establecida por el trabajo de Yuri Matiyasevich , Julia Robinson , Martin Davis y Hilary Putnam , con la prueba final en 1970, implica también una respuesta negativa al Entscheidungsproblem .

Generalizaciones

Utilizando el teorema de deducción , el problema de Entscheidungs ​​abarca el problema más general de decidir si una oración dada de primer orden 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 problema de Entscheidung. Sin embargo, estos problemas de decisión más generales son de interés práctico. 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 . Por otro lado, la teoría de primer orden de los números naturales con suma y multiplicación expresada por los axiomas de Peano no puede decidirse con un algoritmo.

Fragmentos

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

El clásico Entscheidungsproblem pregunta si, dada una fórmula de primer orden, es cierta en todos los modelos. El problema finito pregunta si esto es cierto 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 o no. ${\displaystyle {\rm {{Sat}(\Phi )}}}$ ${\displaystyle \Phi }$ ${\displaystyle {\rm {{FinSat}(\Phi )}}}$ ${\displaystyle {\rm {Sat}}}$ ${\displaystyle \Phi }$ ${\displaystyle {\rm {{Sat}(\Phi )}}}$

Hay una jerarquía de decidibilidad. En la cima están los problemas indecidibles. Debajo están 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", "Algún p es q", "Algún p no es q". Podemos formalizar este tipo de oraciones como un fragmento de lógica de primer orden:

$${\displaystyle \forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)}$$

NLOGSPACE ${\displaystyle p,q}$ ${\displaystyle +q:=q,\;-q:=\neg q}$ ${\displaystyle {\rm {Sat}}}$ ${\displaystyle {\rm {Sat}}}$

$${\displaystyle \forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)}$$

La lógica relacional ${\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}$

$${\displaystyle {\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}}}$$

NLOGSPACEEXPTIME ${\displaystyle {\rm {Sat}}}$ ${\displaystyle \pm p,\pm q}$

arity

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

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

Prefijo cuantificador

Cualquier fórmula de primer orden tiene una forma normal prenexa. Para cada posible prefijo cuantificador de la forma normal del prenexo, 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 . ${\displaystyle [\exists ^{*}\forall ^{*}]_{=}}$ ${\displaystyle \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 para cada máquina de Turing es equivalente a una fórmula lógica de primer orden de la forma , el problema es indecidible. ${\displaystyle \forall \exists \forall \exists ^{6}}$ ${\displaystyle {\rm {{Sat}(\forall \exists \forall \exists ^{6})}}}$

Los límites precisos se conocen claramente:

• ${\displaystyle {\rm {{Sat}(\forall \exists \forall )}}}$y son co-RE-completos, y los problemas son RE-completos (Teorema 5.2). ${\displaystyle {\rm {{Sat}([\forall \exists \forall ]_{=})}}}$ ${\displaystyle {\rm {FinSat}}}$
• Lo mismo ocurre con (Teorema 5.3). ${\displaystyle \forall ^{3}\exists }$
• ${\displaystyle \exists ^{*}\forall ^{2}\exists ^{*}}$es decidible, demostrado independientemente por Gödel, Schütte y Kalmár.
• ${\displaystyle [\forall ^{2}\exists ]_{=}}$es indecidible.
• Para any , ambos y son NEXPTIME-completos (Teorema 5.1). ${\displaystyle n\geq 0}$ ${\displaystyle {\rm {{Sat}(\exists ^{n}\forall ^{*})}}}$ ${\displaystyle {\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}}$
  • Esto implica que es decidible, un resultado publicado por primera vez por Bernays y Schönfinkel. ^[9] ${\displaystyle {\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}}$
• Para cualquiera , EXPTIME está completo (Sección 5.4.1). ${\displaystyle n\geq 0,m\geq 2}$ ${\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}}$
• Para cualquiera , es NEXPTIME-completo (Sección 5.4.2). ${\displaystyle n\geq 0}$ ${\displaystyle {\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}}$
  • Esto implica que es decidible, un resultado publicado por primera vez por Ackermann. ^[10] ${\displaystyle {\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}}$
• Para cualquiera , y son PSPACE completos (Sección 5.4.3). ${\displaystyle n\geq 0}$ ${\displaystyle {\rm {{Sat}(\exists ^{n}\forall \exists )}}}$ ${\displaystyle {\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 de predicado e igualdad/no igualdad.

Procedimientos prácticos de decisión.

Tener procedimientos de decisión prácticos 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 suelen decidirse 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 las pruebas de satisfacibilidad con las de decisión de conjunciones; hoy en día generalmente se deciden 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 polinomial real, también conocida como teoría de campos cerrados reales , es decidible; este es el teorema de Tarski-Seidenberg , que se ha implementado en computadoras mediante el uso de la descomposición algebraica cilíndrica .

Ver también

• Demostración automatizada de teoremas
• El segundo problema de Hilbert
• máquina oráculo
• La prueba de Turing

Notas

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 se presentó a la Sociedad Estadounidense de Matemáticas el 19 de abril de 1935 y se publicó el 15 de abril de 1936. Turing, que había logrado avances sustanciales en la redacción de sus propios resultados, se sintió decepcionado al enterarse de la prueba de Church tras su publicación (ver correspondencia entre Max Newman y Church en los artículos de Alonzo Church). Turing completó rápidamente su artículo y lo apresuró a publicarlo; 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 a 240), publicada el 30 de noviembre de 1936, y en la Parte 4 (páginas 241 a 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 al pie al final de Soare: 1996.
3. Davis 2001, págs. 3-20
4. Hodges 1983, pág. 91
5. Kline, GL; Anovskaa, SA (1951), "Revisión de los 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
6. Hodges 1983, pág. 92, citando a Hilbert
7. Pratt-Hartmann, Ian (30 de marzo de 2023). Fragmentos de lógica de primer orden. Prensa de la Universidad de Oxford. 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), págs. 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.

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 elemental ", American Journal of Mathematics, 58 (1936), págs.
• Alonzo Church , "Una nota sobre el Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), págs.
• Davis, Martín (2001). Motores de la lógica: los matemáticos y el origen de la computadora . Libro de bolsillo de Norton (1. publicado como edición de bolsillo de Norton). Nueva York, NY Londres: Norton. ISBN 978-0-393-32229-3.
• Alan Turing , " Sobre números computables, con una aplicación al Entscheidungsproblem ", Actas de la Sociedad Matemática de Londres , Serie 2, 42 (1936–7), págs. Versiones en línea: del sitio web de la revista, de Turing Digital Archive, de abelard.org. Errata apareció en la Serie 2, 43 (1937), págs. 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 ocupa el tercer lugar en este volumen. Los artículos incluyen los de Gödel, Church, Rosser, Kleene y Post.
• Hodges, Andrés (1983). Alan Turing: el enigma . Nueva York: Simon y Schuster. ISBN 978-0-671-49207-6.Biografía de Alan M. Turing. Cf. Capítulo "El Espíritu de la Verdad" para una historia que conduce a su prueba y una discusión sobre ella.
• Soare, Robert I. , "Computabilidad y recursividad", Bull. Lógica simbólica 2 (1996), núm. 3, 284–321.
• Toulmin, Stephen , "Fall of a Genius", reseña del libro " Alan Turing: The Enigma by Andrew Hodges", en The New York Review of Books, 19 de enero de 1984, p. 3 y siguientes.
• Whitehead, Alfred Norte ; Russell, Bertrand , Principia Mathematica to *56, Cambridge at the 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ítulo 1 p. 24 "...dificultades que surgen en la lógica formal", y Capítulo 2.I. "El principio del círculo vicioso" p. 37ff, y Capítulo 2.VIII. "Las Contradicciones" p. 60 y siguientes.

enlaces externos

• La definición del diccionario de entscheidungsproblem en Wikcionario