Teoría existencial de los números reales

La teoría existencial de los números reales es el conjunto de todos los enunciados verdaderos de la forma

donde es una fórmula sin cuantificadores , que incluye igualdades y desigualdades de polinomios reales [1] .

El problema de solución para la teoría existencial de los números reales es el problema de encontrar un algoritmo que decida para cada fórmula si es verdadera o no. De manera equivalente, este es el problema de verificar que un conjunto semialgebraico dado no esté vacío [1] . Este problema de resolución es NP-difícil y se encuentra en PSPACE [2] . Así, el problema es mucho menos complejo que el procedimiento de eliminación de los cuantificadores de Alfred Tarski en teorías reales de primer orden [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 este tipo de problemas [3] .

Muchos problemas naturales de la teoría de grafos geométricos , especialmente problemas de reconocimiento de gráficos de intersección geométrica y enderezamiento de bordes de dibujos de gráficos con intersecciones , pueden resolverse convirtiéndolos en una variante de la teoría existencial de números reales y están completos para esta teoría. Para describir estas tareas se define una clase de complejidad , que se encuentra entre NP y PSPACE [4] .

Antecedentes

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

La secuencia de estos símbolos forma una oración que pertenece a la teoría del primer orden de los reales, si es gramaticalmente correcta, todas sus variables tienen cuantificadores apropiados y (cuando se interpreta como una declaración matemática sobre los reales ) es una declaración válida. Como ha demostrado Tarski, esta teoría puede describirse mediante un esquema axiomático y un procedimiento de decisión que es completo y eficiente, es decir: para cualquier enunciado gramaticalmente correcto con un conjunto completo de cuantificadores, el enunciado mismo o su negación (pero no ambos) ) puede deducirse de los axiomas . La misma teoría describe cualquier campo cerrado real , no solo números reales [6] . Sin embargo, existen otros sistemas numéricos que estos axiomas no describen exactamente. La teoría, definida de la misma manera para números enteros en lugar de números reales, según el teorema de Matiyasevich , es indecidible incluso para enunciados de existencia para ecuaciones diofánticas [5] [7] .

La teoría existencial de los números reales es un subconjunto de la teoría de primer orden y consiste en declaraciones en las que cada cuantificador es un cuantificador existencial y todos aparecen antes que cualquier otro símbolo. Es decir, es un conjunto de enunciados verdaderos de la forma

donde es una fórmula sin cuantificadores que contiene igualdades y desigualdades con polinomios sobre números reales . El problema de decidibilidad para la teoría existencial de los números reales es el problema algorítmico de verificar si una oración dada pertenece a esta teoría. De manera equivalente, para las cadenas que pasan las verificaciones de sintaxis básicas (es decir, la oración usa los caracteres correctos, tiene la sintaxis correcta y no tiene variables sin cuantificadores), es la tarea de verificar que la declaración sea verdadera sobre números reales. . El conjunto de n -tuplas de números reales para los que es verdadero se denomina conjunto semialgebraico, por lo que el problema de la resolución de la teoría existencial de los números reales se puede reformular de manera equivalente como verificar que un conjunto semialgebraico dado no esté vacío [ 1] .

Para determinar la complejidad temporal de los algoritmos para el problema de resolución de la teoría existencial de los números reales, es importante tener una forma de medir el tamaño de la entrada. La forma más sencilla de medir este tipo es la longitud de la oración, es decir, el número de caracteres incluidos en el enunciado [5] . Sin embargo, para obtener 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, destacando el número de variables con cuantificadores, el número de polinomios en la oración, y los grados de estos polinomios [8] .

Ejemplos

La proporción áurea se puede definir como la raíz de un 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 proposición

Dado que existe la proporción áurea, la afirmación es verdadera y pertenece a la teoría existencial de los números reales. La respuesta al problema de solución para la teoría existencial de los números reales, dada esta oración como entrada, es el valor booleano true ( verdadero ).

La desigualdad entre la media aritmética y la media geométrica establece que para cualesquiera dos números no negativos se cumple la siguiente desigualdad:

La declaración es una declaración de primer orden sobre los números reales, pero es universal (no contiene cuantificadores existenciales) y usa símbolos adicionales para la división, la raíz cuadrada y el número 2, que no están permitidos en la teoría de primer orden de los numeros reales Sin embargo, después de elevar al cuadrado ambas partes, la oración se puede transformar en la siguiente declaración existencial, que se puede interpretar como preguntando si hay un contraejemplo a la desigualdad:

La respuesta al problema de solucionabilidad para la teoría existencial de los números reales, cuya entrada es esta ecuación, es el valor booleano false ( falso ), es decir, no hay contraejemplo. Así, esta oración no pertenece a la teoría existencial de los números reales, aunque es correcta desde el punto de vista de la gramática.

Algoritmos

El método de eliminación de cuantificadores de Alfred Tarski (1948) muestra que la teoría existencial de los reales (y más generalmente la teoría de los reales de primer orden) es algorítmicamente decidible, pero sin límites elementales de complejidad [9] [6] . El método de descomposición algebraica cilíndrica de Collins (1975) mejoró la dependencia del tiempo al doble de la exponencialidad [9] , [10] de la forma

donde es el número de bits necesarios para representar los coeficientes en el enunciado cuyo valor se va a determinar, es el número de polinomios en el enunciado, es su grado común y es el número de variables [8] En 1988 , Dmitry Grigoriev y Nikolai Vorobyov demostraron que la complejidad es exponencial y que el grado es un polinomio en [8] [11] [12] ,

y en una serie de artículos publicados en 1992, James Renegar mejoró la estimación ligeramente por encima del exponente on [8] [13] [14] [15] .

Mientras tanto, en 1988 John Canny describió otro algoritmo que también depende exponencialmente en el tiempo, pero solo tiene una complejidad de memoria polinomial. Es decir, demostró que el problema se puede resolver en la clase PSPACE [2] [9] .

La complejidad computacional asintótica de estos algoritmos puede ser engañosa, ya que los algoritmos solo pueden funcionar con tamaños de entrada muy pequeños. Comparando los algoritmos en 1991, Hong Hong estimó que el tiempo del procedimiento de Collins (con evaluación exponencial doble) para un problema cuyo tamaño se describe estableciendo todos los parámetros anteriores en 2 en menos de dos segundos, mientras que los algoritmos de Grigoriev, Vorobyov y Renegar gastaría en resolver el problema durante más de un millón de años [8] . En 1993, Yos, Roy y Solerno sugirieron que debería ser posible modificar ligeramente los procedimientos de tiempo exponencial para hacerlos más rápidos en la práctica que la solución algebraica cilíndrica, lo que sería consistente con la teoría [16] . Sin embargo, a partir de 2009, los métodos generales para la teoría de números reales de primer orden siguen siendo los mejores en la práctica en comparación con los algoritmos con evaluación exponencial simple diseñados específicamente para la teoría existencial de números reales [3] .

Completar tareas

Algunos problemas de complejidad computacional y teoría de grafos geométricos pueden clasificarse como completos para la teoría existencial de números reales. Es decir, cualquier problema de la teoría existencial de los números reales tiene una reducción polinomial multivaluada a una variante de uno de estos problemas y, a la inversa, 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 gráficos de intersección de cierto tipo. En estos problemas, la entrada es un gráfico no dirigido . El objetivo es determinar si es posible asociar geometrías de una determinada clase con vértices de gráficos de tal manera que dos vértices en el gráfico sean adyacentes si y solo si las geometrías asociadas tienen una intersección no vacía. Los problemas completos de este tipo para la teoría existencial de los números reales incluyen

Para los gráficos dibujados en el plano sin intersecciones, el teorema de Farey establece que obtenemos la misma clase de gráficos planos ya sea que los bordes del gráfico se deban dibujar como segmentos de línea o se puedan dibujar como curvas. Pero esta equivalencia de clase no es cierta para otros tipos de representación gráfica. Por ejemplo, aunque el número de intersección de un gráfico (el número mínimo de intersecciones de aristas para aristas curvilíneas) puede definirse como perteneciente a la clase NP, para la teoría existencial de los números reales el problema de determinar si existen patrones sobre los que límite dado del número de intersección rectilínea (el número mínimo de pares de aristas que se intersecan en cualquier figura con aristas en forma de segmentos de línea recta en el plano) es completo [4] [20] . El problema completo para la teoría existencial de los números reales es también el problema de comprobar si un gráfico dado se puede dibujar en un plano con segmentos en forma de aristas rectas y con un conjunto dado de pares de aristas que se cortan o, de manera equivalente, si un dibujo con bordes curvilíneos con intersecciones se puede enderezar de tal manera que se conserven las intersecciones [21] .

Otros problemas completos para la teoría existencial de los números reales:

[31] ;

Con base en esto, la clase de complejidad se define como un conjunto de problemas que tienen reducción de tiempo polinomial según Karp a la teoría existencial de los números reales [4] .

Notas

  1. ↑ 1 2 3 4 Basu, Pollack, Roy, 2006 , pág. 505–532.
  2. ↑ 1 2 Canny, 1988 , pág. 460–467.
  3. ↑ 1 2 Passmore, Jackson, 2009 , pág. 122–137.
  4. ↑ 1 2 3 4 5 6 7 Schaefer, 2010 , pág. 334–344.
  5. ↑ 1 2 3 4 Matousek, 2014 .
  6. ↑ 12 Tarski , 1948 .
  7. ↑ Matiyasevich, 2006 , pág. 185–213.
  8. ↑ 1 2 3 4 5 Hong, 1991 .
  9. ↑ 1 2 3 4 Schaefer, 2013 , pág. 461–482.
  10. ↑ Collins, 1975 , pág. 134–183.
  11. ↑ Grigor'ev, 1988 , p. 65–108.
  12. ↑ Grigor'ev, Vorobjov, 1988 , p. 37–64.
  13. ↑ Renegar, 1992 , pág. 255–299.
  14. ↑ Renegar, 1992 , pág. 301–327.
  15. ↑ Renegar, 1992 , pág. 329–352.
  16. ↑ Heintz, Roy, Solerno, 1993 , pág. 427–431.
  17. ↑ 1 2 3 4 Cardenal, 2015 , p. 69–78.
  18. ↑ Kratochvíl, Matousek, 1994 , p. 289–315.
  19. ↑ Kang, Müller, 2011 , pág. 308–314.
  20. ↑ Bienstock, 1991 , pág. 443–459.
  21. ↑ Kynčl, 2011 , pág. 383–399.
  22. ↑ Abrahamsen, Adamaszek, Miltzow, 2017 .
  23. ↑ Mnev, 1988 , pág. 527–543.
  24. ↑ Shor, 1991 , pág. 531–554.
  25. ↑ Herrmann, Ziegler, 2016 .
  26. ↑ Björner, Las Vergnas, Sturmfels, White, Ziegler, 1993 .
  27. ↑ Richter-Gebert y Ziegler 1995 , pág. 403–412.
  28. ↑ Dobbins, Holmsen, Hubard, 2014 .
  29. ↑ Garg, Mehta, Vazirani, Yazdanbod, 2015 , pág. 554–566.
  30. ↑ Bilo, Mavronicolas, 2016 , pág. 17:1–17:13.
  31. ↑ Bilo, Mavronicolas, 2017 , pág. 13:1–13:14.
  32. ↑ Herrmann, Sokoli, Ziegler, 2013 .
  33. ↑ Hoffman, 2016 .

Literatura