stringtranslate.com

Teoría existencial de los reales

En lógica matemática , teoría de la complejidad computacional y ciencias de la computación , la teoría existencial de los números reales es el conjunto de todas las oraciones verdaderas de la forma donde las variables se interpretan como si tuvieran valores de números reales , y donde es una fórmula sin cuantificadores que involucra igualdades y desigualdades de polinomios reales . Una oración de esta forma es verdadera si es posible encontrar valores para todas las variables que, cuando se sustituyen en la fórmula , la hacen verdadera. [1]

El problema de decisión para la teoría existencial de los números reales es el problema de encontrar un algoritmo que decida, para cada una de esas oraciones, si es verdadera o falsa. Equivalentemente, es el problema de probar si un conjunto semialgebraico dado no es vacío. [1] Este problema de decisión es NP-hard y se encuentra en PSPACE , [2] lo que le da una complejidad significativamente menor que el procedimiento de eliminación de cuantificadores de Alfred Tarski para decidir enunciados en la teoría de primer orden de los números reales sin la restricción a los cuantificadores existenciales. [1] Sin embargo, en la práctica, los métodos generales para la teoría de primer orden siguen siendo la opción preferida para resolver estos problemas. [3]

La clase de complejidad se ha definido para describir la clase de problemas computacionales que pueden traducirse en oraciones equivalentes de esta forma. En la teoría de la complejidad estructural , se encuentra entre NP y PSPACE. Muchos problemas naturales en la teoría de grafos geométricos , especialmente los problemas de reconocimiento de grafos de intersección geométrica y de enderezamiento de los bordes de los dibujos de grafos con cruces , pertenecen a , y son completos para esta clase. Aquí, completitud significa que existe una traducción en la dirección inversa, desde una oración arbitraria sobre los números reales a una instancia equivalente del problema dado. [4]

Fondo

En lógica matemática , una teoría es un lenguaje formal que consiste en un conjunto de oraciones escritas utilizando un conjunto fijo de símbolos. La teoría de primer orden de cuerpos reales cerrados tiene los siguientes símbolos: [5]

Una secuencia de estos símbolos forma una oración que pertenece a la teoría de primer orden de los números reales si está bien formada gramaticalmente, todas sus variables están cuantificadas apropiadamente y (cuando se interpreta como un enunciado matemático acerca de los números reales ) es un enunciado verdadero. Como mostró Tarski, esta teoría puede ser descrita por un esquema axiomático y un procedimiento de decisión que es completo y efectivo: para cada oración completamente cuantificada y gramatical, la oración o su negación (pero no ambas) pueden ser derivadas de los axiomas. La misma teoría describe cada cuerpo real cerrado , no solo los números reales. [6] Sin embargo, hay otros sistemas numéricos que no están descritos con precisión por estos axiomas; en particular, la teoría definida de la misma manera para números enteros en lugar de números reales es indecidible , incluso para oraciones existenciales ( ecuaciones diofánticas ) por el teorema de Matiyasevich . [5] [7]

La teoría existencial de los reales es el fragmento de la teoría de primer orden que consiste en oraciones en las que todos los cuantificadores son existenciales y aparecen antes de cualquiera de los otros símbolos. Es decir, es el conjunto de todas las oraciones verdaderas de la forma donde es una fórmula libre de cuantificadores que involucra igualdades y desigualdades de polinomios reales . El problema de decisión para la teoría existencial de los reales es el problema algorítmico de probar si una oración dada pertenece a esta teoría; equivalentemente, para cadenas que pasan las verificaciones sintácticas básicas (usan los símbolos correctos con la sintaxis correcta y no tienen variables no cuantificadas) es el problema de probar si la oración es una declaración verdadera sobre los números reales. El conjunto de -tuplas de números reales para las que es verdadera se llama conjunto semialgebraico , por lo que el problema de decisión para la teoría existencial de los reales puede reformularse equivalentemente como probar si un conjunto semialgebraico dado no está vacío. [1]

Para determinar la complejidad temporal de los algoritmos del problema de decisión de la teoría existencial de los números reales, es importante contar con una medida del tamaño de la entrada. La medida más simple de este tipo es la longitud de una oración: es decir, el número de símbolos que contiene. [5] Sin embargo, para lograr un análisis más preciso del comportamiento de los algoritmos para este problema, es conveniente descomponer el tamaño de la entrada en varias variables, separando el número de variables a cuantificar, el número de polinomios dentro de la oración y el grado de estos polinomios. [8]

Ejemplos

La proporción áurea puede definirse como la raíz del polinomio . Este polinomio tiene dos raíces, de las cuales solo una (la proporción áurea) es mayor que uno. Por lo tanto, la existencia de la proporción áurea puede expresarse mediante la oración Como la proporción áurea no es trascendental , esta es una oración verdadera y pertenece a la teoría existencial de los reales. La respuesta al problema de decisión para la teoría existencial de los reales, dada esta oración como entrada, es el valor booleano verdadero.

La desigualdad de las medias aritmética y geométrica establece que, para cada dos números no negativos y , se cumple la siguiente desigualdad: Como se dijo anteriormente, es una oración de primer orden sobre los números reales, pero con cuantificadores universales en lugar de existenciales, y que utiliza símbolos adicionales para la división, raíces cuadradas y el número 2 que no están permitidos en la teoría de primer orden de los reales. Sin embargo, al elevar al cuadrado ambos lados se puede transformar en la siguiente declaración existencial que puede interpretarse como una pregunta sobre si la desigualdad tiene contraejemplos:

La respuesta al problema de decisión de la teoría existencial de los reales, dada esta oración como entrada, es el valor booleano falso: no hay contraejemplos. Por lo tanto, esta oración no pertenece a la teoría existencial de los reales, a pesar de tener la forma gramatical correcta.

Algoritmos

El método de eliminación de cuantificadores de Alfred Tarski (1948) mostró que la teoría existencial de los reales (y más generalmente la teoría de primer orden de los reales) se puede resolver algorítmicamente, pero sin un límite elemental en su complejidad. [9] [6] El método de descomposición algebraica cilíndrica , de George E. Collins (1975), mejoró la dependencia del tiempo a doblemente exponencial , [9] [10] de la forma donde es el número de bits necesarios para representar los coeficientes en la oración cuyo valor se va a determinar, es el número de polinomios en la oración, es su grado total y es el número de variables. [8] En 1988, Dima Grigoriev y Nicolai Vorobjov habían demostrado que la complejidad era exponencial en un polinomio de , [8] [11] [12] y en una secuencia de artículos publicados en 1992, James Renegar mejoró esto a una dependencia exponencial simple en , [8] [13] [14] [15] Mientras tanto, en 1988, John Canny describió otro algoritmo que también tiene dependencia temporal exponencial, pero solo complejidad espacial polinomial; es decir, demostró que el problema podía resolverse en PSPACE . [2] [9]

La complejidad computacional asintótica de estos algoritmos puede ser engañosa, porque en la práctica solo se pueden ejecutar en entradas de tamaño muy pequeño. En una comparación de 1991, Hoon Hong estimó que el procedimiento doblemente exponencial de Collins podría resolver un problema cuyo tamaño se describe estableciendo todos los parámetros anteriores a 2, en menos de un segundo, mientras que los algoritmos de Grigoriev, Vorbjov y Renegar tomarían más de un millón de años. [8] En 1993, Joos , Roy y Solernó sugirieron que debería ser posible realizar pequeñas modificaciones a los procedimientos de tiempo exponencial para hacerlos más rápidos en la práctica que la decisión algebraica cilíndrica, así como más rápidos en teoría. [16] Sin embargo, a partir de 2009, todavía era el caso de que los métodos generales para la teoría de primer orden de los números reales seguían siendo superiores en la práctica a los algoritmos exponenciales simples especializados en la teoría existencial de los números reales. [3]

Problemas completos

Varios problemas de complejidad computacional y teoría de grafos geométricos pueden clasificarse como completos para la teoría existencial de los números reales. Es decir, cada problema en la teoría existencial de los números reales tiene una reducción de muchos a uno en tiempo polinomial a una instancia de uno de estos problemas, y a su vez estos problemas son reducibles a la teoría existencial de los números reales. [4] [17]

Varios problemas de este tipo se refieren al reconocimiento de grafos de intersección de un tipo determinado. En estos problemas, la entrada es un grafo no dirigido ; el objetivo es determinar si las formas geométricas de una determinada clase de formas pueden asociarse con los vértices del grafo de tal manera que dos vértices sean adyacentes en el grafo si y solo si sus formas asociadas tienen una intersección no vacía. Los problemas de este tipo que son completos para la teoría existencial de los números reales incluyen el reconocimiento de grafos de intersección de segmentos de línea en el plano, [4] [18] [5] el reconocimiento de grafos de disco unitario , [19] y el reconocimiento de grafos de intersección de conjuntos convexos en el plano. [4]

Para los grafos dibujados en el plano sin cruces, el teorema de Fáry establece que se obtiene la misma clase de grafos planos independientemente de si los bordes del grafo se dibujan como segmentos de línea recta o como curvas arbitrarias. Pero esta equivalencia no es válida para otros tipos de dibujo. Por ejemplo, aunque el número de cruces de un grafo (el número mínimo de cruces en un dibujo con bordes arbitrariamente curvados) puede determinarse en NP, es completo para la teoría existencial de los reales determinar si existe un dibujo que logre un límite dado en el número de cruces rectilíneos (el número mínimo de pares de bordes que se cruzan en cualquier dibujo con bordes dibujados como segmentos de línea recta en el plano). [4] [20] También es completo para la teoría existencial de los reales comprobar si un grafo dado puede dibujarse en el plano con bordes de línea recta y con un conjunto dado de pares de bordes como sus cruces, o equivalentemente, si un dibujo curvo con cruces puede enderezarse de una manera que preserve sus cruces. [21]

Otros problemas completos para la teoría existencial de los reales incluyen:

En base a esto, la clase de complejidad ha sido definida como el conjunto de problemas que tienen una reducción muchos-uno en tiempo polinomial a la teoría existencial de los reales. [4]

Véase también

Referencias

  1. ^ abcd Basu, Saugata; Pollack, Richard ; Roy, Marie-Françoise (2006), "Teoría existencial de los reales", Algorithms in Real Algebraic Geometry , Algorithms and Computation in Mathematics, vol. 10 (2.ª ed.), Springer-Verlag, págs. 505–532, doi :10.1007/3-540-33099-2_14, ISBN 978-3-540-33098-1.
  2. ^ ab Canny, John (1988), "Algunos cálculos algebraicos y geométricos en PSPACE", Actas del Vigésimo Simposio Anual de la ACM sobre Teoría de la Computación (STOC '88, Chicago, Illinois, EE. UU.) , Nueva York, NY, EE. UU.: ACM, págs. 460–467, doi : 10.1145/62212.62257 , ISBN 0-89791-264-0, Número de identificación del sujeto  14535463
  3. ^ ab Passmore, Grant Olney; Jackson, Paul B. (2009), "Técnicas de decisión combinadas para la teoría existencial de los reales", Intelligent Computer Mathematics: 16.º Simposio, Calculemus 2009, 8.ª Conferencia Internacional, MKM 2009, celebrada como parte de la CICM 2009, Grand Bend, Canadá, del 6 al 12 de julio de 2009, Actas, Parte II, Lecture Notes in Computer Science , vol. 5625, Springer-Verlag, págs. 122–137, doi :10.1007/978-3-642-02614-0_14, hdl : 20.500.11820/b2cc91c8-6b87-4146-bab6-a2021b3006b2 , ISBN 978-3-642-02613-3, S2CID1160351 ​.
  4. ^ abcdefg Schaefer, Marcus (2010), "Complejidad de algunos problemas geométricos y topológicos" (PDF) , Graph Drawing, 17th International Symposium, GD 2009, Chicago, IL, EE. UU., septiembre de 2009, Documentos revisados ​​, Lecture Notes in Computer Science, vol. 5849, Springer-Verlag, págs. 334–344, doi : 10.1007/978-3-642-11805-0_32 , ISBN 978-3-642-11804-3.
  5. ^ abcd Matoušek, Jiří (2014), "Gráficos de intersección de segmentos y ", arXiv : 1406.2636 [cs.CG]
  6. ^ ab Tarski, Alfred (1948), Un método de decisión para álgebra y geometría elemental , RAND Corporation, Santa Mónica, California, MR  0028796.
  7. ^ Matiyasevich, Yu. V. (2006), "El décimo problema de Hilbert: ecuaciones diofánticas en el siglo XX", Acontecimientos matemáticos del siglo XX , Berlín: Springer-Verlag, pp. 185–213, Bibcode :2006metc.book.....A, doi :10.1007/3-540-29462-7_10, ISBN 978-3-540-23235-3, Sr.  2182785.
  8. ^ abcde Hong, Hoon (11 de septiembre de 1991), Comparación de varios algoritmos de decisión para la teoría existencial de los reales, Informe técnico, vol. 91–41, RISC Linz[ enlace muerto permanente ] .
  9. ^ abcd Schaefer, Marcus (2013), "Realizabilidad de grafos y vínculos", en Pach, János (ed.), Treinta ensayos sobre teoría geométrica de grafos , Springer-Verlag, págs. 461–482, doi :10.1007/978-1-4614-0110-0_24, ISBN 978-1-4614-0109-4.
  10. ^ Collins, George E. (1975), "Eliminación de cuantificadores para campos reales cerrados mediante descomposición algebraica cilíndrica", Teoría de autómatas y lenguajes formales (Segunda conferencia de GI, Kaiserslautern, 1975) , Lecture Notes in Computer Science , vol. 33, Berlín: Springer-Verlag, págs. 134-183, MR  0403962.
  11. ^ Grigor'ev, D. Yu. (1988), "Complejidad de la decisión sobre el álgebra de Tarski", Journal of Symbolic Computation , 5 (1–2): 65–108, doi : 10.1016/S0747-7171(88)80006-3 , MR  0949113.
  12. ^ Grigor'ev, D. Yu. ; Vorobjov, NN Jr. (1988), "Resolución de sistemas de desigualdades polinómicas en tiempo subexponencial" (PDF) , Journal of Symbolic Computation , 5 (1–2): 37–64, doi :10.1016/S0747-7171(88)80005-1, MR  0949112, S2CID  39376619.
  13. ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los números reales. I. Introducción. Preliminares. La geometría de los conjuntos semialgebraicos. El problema de decisión para la teoría existencial de los números reales", Journal of Symbolic Computation , 13 (3): 255–299, doi : 10.1016/S0747-7171(10)80003-3 , MR  1156882.
  14. ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los números reales. II. El problema de decisión general. Preliminares para la eliminación de cuantificadores", Journal of Symbolic Computation , 13 (3): 301–327, doi : 10.1016/S0747-7171(10)80004-5 , MR  1156883.
  15. ^ Renegar, James (1992), "Sobre la complejidad computacional y la geometría de la teoría de primer orden de los números reales. III. Eliminación de cuantificadores", Journal of Symbolic Computation , 13 (3): 329–352, doi : 10.1016/S0747-7171(10)80005-7 , MR  1156884.
  16. ^ Heintz, Joos ; Roy, Marie-Françoise ; Solernó, Pablo (1993), "Sobre la complejidad teórica y práctica de la teoría existencial de los reales", The Computer Journal , 36 (5): 427–431, doi : 10.1093/comjnl/36.5.427 , MR  1234114.
  17. ^ abcd Cardinal, Jean (diciembre de 2015), "Columna 62 de geometría computacional", SIGACT News , 46 (4): 69–78, doi :10.1145/2852040.2852053, S2CID  17276902.
  18. ^ Kratochvíl, enero ; Matoušek, Jiří (1994), "Gráficos de intersección de segmentos", Journal of Combinatorial Theory, Serie B , 62 (2): 289–315, doi : 10.1006/jctb.1994.1071 , MR  1305055.
  19. ^ Kang, Ross J.; Müller, Tobias (2011), "Representaciones de grafos mediante productos esféricos y escalares", Actas del Vigésimo Séptimo Simposio Anual sobre Geometría Computacional (SCG'11), 13-15 de junio de 2011, París, Francia , pp. 308-314.
  20. ^ Bienstock, Daniel (1991), "Algunos problemas de cruce de números demostrablemente difíciles", Geometría discreta y computacional , 6 (5): 443–459, doi : 10.1007/BF02574701 , MR  1115102, S2CID  38465081.
  21. ^ Kynčl, Jan (2011), "Realización simple de gráficos topológicos abstractos completos en P", Geometría discreta y computacional , 45 (3): 383–399, doi : 10.1007/s00454-010-9320-x , MR  2770542, S2CID  12419381.
  22. ^ Abrahamsen, Mikkel; Adamaszek, Anna; Miltzow, Tillmann (2022), "El problema de la galería de arte está completo", Journal of the ACM , 69 (1): A4:1–A4:70, doi :10.1145/3486220, hdl : 1874/424939 , MR  4402363
  23. ^ Abrahamsen, Mikkel; Kleist, Linda; Miltzow, Tillmann (2021), "El entrenamiento de redes neuronales es ∃ R {\displaystyle \exists \mathbb {R} } -completo", en Ranzato, Marc'Aurelio; Beygelzimer, Alina; Dauphin, Yann N.; Liang, Percy; Vaughan, Jennifer Wortman (eds.), Avances en sistemas de procesamiento de información neuronal 34: Conferencia anual sobre sistemas de procesamiento de información neuronal 2021, NeurIPS 2021, 6-14 de diciembre de 2021, virtual , págs. 18293–18306, arXiv : 2102.09798
  24. ^ Abrahamsen, Mikkel; Miltzow, Tillmann; Seiferth, Nadja (2020), "Framework for -completeness of two-dimensional packaging issues", 61.º Simposio anual del IEEE sobre fundamentos de la informática, FOCS 2020, Durham, Carolina del Norte, EE. UU., 16 al 19 de noviembre de 2020 , IEEE, págs. 1014–1021, arXiv : 2004.07558 , doi :10.1109/FOCS46700.2020.00098, ISBN 978-1-7281-9621-3, Número de identificación del sujeto  216045462
  25. ^ Mnëv, NE (1988), "Los teoremas de universalidad en el problema de clasificación de variedades de configuración y variedades de politopos convexos", Topología y geometría — Seminario Rohlin , Lecture Notes in Mathematics , vol. 1346, Berlín: Springer-Verlag, págs. 527–543, doi :10.1007/BFb0082792, ISBN 978-3-540-50237-1, Sr.  0970093.
  26. ^ Shor, Peter W. (1991), "La capacidad de estiramiento de las pseudolíneas es NP-dura", Geometría aplicada y matemáticas discretas , Serie DIMACS en matemáticas discretas y ciencias de la computación teóricas, vol. 4, Providence, RI: American Mathematical Society , págs. 531–554, MR  1116375.
  27. ^ Herrmann, Christian; Ziegler, Martin (2016), "Complejidad computacional de la satisfacibilidad cuántica", Journal of the ACM , vol. 63, págs. 1–31, arXiv : 1004.1696 , doi :10.1145/2869073, S2CID  2253943.
  28. ^ Benedikt, Michael; Lenhardt, Rastislav; Worrell, James (2013), "Verificación del modelo LTL de cadenas de Markov de intervalos", Herramientas y algoritmos para la construcción y análisis de sistemas. TACAS 2013 , Lecture Notes in Computer Science, vol. 7795, págs. 32–46, doi :10.1007/978-3-642-36742-7_3, ISBN 978-3-642-36741-0
  29. ^ Björner, Anders ; Las Vergnas, Michel ; Sturmfels, Bernd ; White, Neil; Ziegler, Günter M. (1993), Matroides orientadas , Enciclopedia de matemáticas y sus aplicaciones, vol. 46, Cambridge: Cambridge University Press, Corolario 9.5.10, pág. 407, ISBN 0-521-41836-4, Sr.  1226888.
  30. ^ Richter-Gebert, Jürgen; Ziegler, Günter M. (1995), "Los espacios de realización de 4-politopos son universales", Boletín de la American Mathematical Society , Nueva serie, 32 (4): 403–412, arXiv : math/9510217 , Bibcode :1995math.....10217R, doi :10.1090/S0273-0979-1995-00604-X, MR  1316500, S2CID  7940964.
  31. ^ Dobbins, Michael Gene; Holmsen, Andreas; Hubard, Alfredo (2017), "Espacios de realización de disposiciones de cuerpos convexos", Geometría discreta y computacional , 58 (1): 1–29, arXiv : 1412.0371 , doi :10.1007/s00454-017-9869-8, MR  3658327, S2CID  39856606.
  32. ^ Garg, Jugal; Mehta, Ruta; Vazirani, Vijay V .; Yazdanbod, Sadra (2015), "Completitud ETR para versiones de decisión de equilibrios de Nash multijugador (simétricos)", Proc. 42.º Coloquio internacional sobre autómatas, lenguajes y programación (ICALP) , Lecture Notes in Computer Science, vol. 9134, Springer, págs. 554–566, doi :10.1007/978-3-662-47672-7_45, ISBN 978-3-662-47671-0.
  33. ^ Bilo, Vittorio; Mavronicolas, Marios (2016), "Un catálogo de problemas de decisión ETR-Completos sobre equilibrios de Nash en juegos multijugador", Actas del 33.° Simposio internacional sobre aspectos teóricos de la informática , LIPIcs, vol. 47, Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik, págs. 17:1–17:13, doi : 10.4230/LIPIcs.STACS.2016.17 , ISBN 978-3-95977-001-9.
  34. ^ Bilo, Vittorio; Mavronicolas, Marios (2017), "Problemas de decisión ETR-Complete sobre equilibrios de Nash simétricos en juegos multijugador simétricos", Actas del 34.º Simposio internacional sobre aspectos teóricos de la informática, LIPIcs, vol. 66, Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik, págs. 13:1–13:14, doi : 10.4230/LIPIcs.STACS.2017.13 , ISBN 978-3-95977-028-6.
  35. ^ Herrmann, Christian; Sokoli, Johanna; Ziegler, Martin (2013), "La satisfacibilidad de los términos del producto cruzado es completa para las máquinas politemporales Blum-Shub-Smale no deterministas reales", Actas de la 6.ª Conferencia sobre máquinas, cálculos y universalidad (MCU'13) , vol. 128, arXiv : 1309.1043 , doi : 10.4204/EPTCS.128 , S2CID  2151889.
  36. ^ Hoffmann, Udo (2016), "El número de pendiente planar", Actas de la 28.ª Conferencia Canadiense sobre Geometría Computacional (CCCG 2016).
  37. ^ Schaefer, Marcus (2021), "RAC-drawability is -complete", Actas del 29º Simposio Internacional sobre Dibujo de Gráficos y Visualización de Redes (GD 2021) , arXiv : 2107.11663
  38. ^ Brijder, Robert; Geerts, Floris; Van den Bussche, enero; Weerwag, Timmy (2019), "Sobre el poder expresivo de los lenguajes de consulta para matrices", Transacciones ACM en sistemas de bases de datos , 44 (4), ACM: 15:1–15:31, doi :10.1145/3331445, hdl : 1942 /30378 , S2CID  204714822.
  39. ^ Bertsimas, Dimitris; Cory-Wright, Ryan; Pauphilet, Jean (2021), "Optimización cónica de proyección mixta: un nuevo paradigma para modelar restricciones de rango", Investigación de operaciones , 70 (6): 3321–3344, arXiv : 2009.10395 , doi :10.1287/opre.2021.2182, S2CID  221836263.