resultados de complejidad no asintótica

Question

Recuerdo haber oído hablar de un resultado, o tal vez un grupo de resultados, en algún área de la teoría de la complejidad, probablemente algebraica, en el sentido de que hay fórmulas conocidas, específicas y cortas, cuya derivación mínima se sabe que es excesivamente larga. O tal vez se trate de una función específica que requiere un circuito excesivamente profundo. La "filosofía" parecía ser que tales ejemplos amenazarían con hacer obsoleta la antigua cuestión asintótica: "A quién le importa la asintótica si las constantes son enormes". ¿Puede alguien, dadas estas pistas, describir ( y dirigirme a) el resultado que escuché?

Answer 1

El hecho general que rodea a algunas de las otras respuestas es lo siguiente:

Toda teoría consistente axiomatizable computacionalmente $T$ que contiene aritmética trivial admite teoremas muy cortos que requieren pruebas extremadamente largas.

El hecho básico es que no puede haber un límite total computable en la longitud de la prueba requerida. Para ver esto supongamos que existe una función total computable $f$ tal que siempre que la declaración $\psi$ es una declaración de tamaño más $n$ demostrable a partir de $T$ entonces hay una prueba de tamaño como máximo $f(n)$ . En este caso, la cuestión de si $T$ prueba $\psi$ será decidible, ya que podemos simplemente inspeccionar todas las pruebas de longitud $f(n)$ , donde $n=|\psi|$ y comprobar si alguno de ellos es una prueba de $\psi$ . Pero es imposible que $T$ prueba $\psi$ es decidible, ya que podría entonces producir una terminación consistente de $T$ por el proceso habitual de completar una teoría, que es eficaz para las teorías decidibles. Esto produciría una teoría computable teoría completa consistente de la aritmética, en contradicción al teorema de incompletitud.

Se puede llegar a una conclusión bastante concreta a través de la detención problema. Si $T$ es verdadera y contiene alguna aritmética trivial aritmética, entonces $T$ demostrará todas las instancias verdaderas de la afirmación programa $p$ se detiene en la entrada $m$ y no pruebe ninguna casos falsos. Si existiera una función total computable $f(p,m)$ de manera que siempre que $p$ se detiene en la entrada $m$ entonces había una prueba de esto de la longitud a lo sumo $f(p,m)$ entonces podríamos decidir el problema de detención: en la entrada $(p,m)$ , calcula $f(p,m)$ y luego mirar todas las pruebas de esa longitud y determinar si hay una prueba de detención o no.

En conclusión:

Teorema. Para cualquier teoría verdadera computablemente axiomatizable $T$ y para cualquier función total computable función $f$ Hay un programa $p$ y la entrada $m$ tal que $T$ demuestra que $p$ se detiene en la entrada $m$ pero no hay prueba de ello en menos de $f(p,m)$ pasos.

Dado que, como todos sabemos, las funciones computables pueden crecer bastante escandaloso, esto significa que para cualquier teoría habrá habrá teoremas cortos que requieran pruebas extremadamente largas.

Answer 2

Se trata de un resultado debido a Godel en su artículo de 1936 "Uber die Lange von Beweisen" (sobre las longitudes de las pruebas), reeditado en traducción inglesa en el volumen 1 de sus obras recopiladas. A grandes rasgos, muestra que hay teoremas cortos que tienen pruebas extremadamente largas en ciertos sistemas formales, pero pruebas mucho más cortas en sistemas más potentes. Harvey Friedman encontró algunos ejemplos explícitos bastante espectaculares, descritos por Smorynski en Las variedades de la experiencia arbórea

Answer 3

Tal vez le hablaron de

Larry J. Stockmeyer, Albert R. Meyer: Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM 49(6): 753-784 (2002)

Del resumen: "Se demuestra una cota inferior exponencial en la complejidad de los circuitos para decidir la teoría débil monádica de segundo orden de un sucesor (WS1S). Los circuitos se construyen a partir de operaciones binarias, o puertas de 2 entradas, que computan funciones booleanas arbitrarias. En particular, para decidir la verdad de fórmulas lógicas de longitud a lo sumo 610 en este lenguaje de segundo orden se requiere un circuito que contenga al menos $10^{125}$ puertas. Así que aunque cada puerta tuviera el tamaño de un protón, el circuito no cabría en el universo conocido.

Esto demuestra una función específica para la que no se pueden determinar todas las entradas de tamaño 610 dentro del universo físico. La prueba es esencialmente un argumento de diagonalización, pero se ejecuta con mucho cuidado para tener en cuenta todas las constantes.

(Obsérvese que esto se basa en realidad en un resultado asintótico, pero ha sido necesario trabajar para obtener un límite inferior concreto).

Answer 4

¿Se refiere por casualidad a ejemplos como la prueba de Haken de que el principio de encasillamiento requiere pruebas de resolución exponencialmente largas?

Answer 5

De los teoremas de jerarquía espacial y temporal en complejidad computacional, y más concretamente de los teoremas de jerarquía temporal no determinista, se desprende que hay enunciados con pruebas extremadamente largas en cualquier sistema formal que (1) pueda describir máquinas de Turing o autómatas celulares o similares; (2) pueda describir números grandes; y (3) tenga pruebas que puedan comprobarse en un tiempo razonable, como el tiempo polinómico o incluso el exponencial. El teorema de la jerarquía no determinista dice que $\text{NTIME}(f(n)) \ne \text{NTIME}(g(n))$ si $f(n)$ y $g(n)$ son funciones razonablemente separadas. Una versión bastante precisa de este resultado se debe a Cook, pero si $f(n)$ y $g(n)$ están lo suficientemente alejados, se puede concluir que existe una separación sólo por comparación con el tiempo determinista. El corolario entonces es que puedes convertir los casos de un problema computacional tan lento en una afirmación que no puede tener una prueba corta; si tuviera una prueba corta, podrías encontrarla rápidamente para responder a la pregunta computacional.

Por ejemplo, para cada fijo $n$ se puede plantear una pregunta del tipo "¿pueden los siguientes cuadrados unitarios con dientes y muescas añadidos embaldosar un cuadrado de tamaño $A(n)$ la función de Ackermann?" La respuesta es siempre demostrablemente sí o demostrablemente no, porque es una pregunta finita. Se puede utilizar un argumento de diagonalización en el sentido de la teoría de la complejidad para demostrar que a veces la prueba tiene una longitud similar a la de Ackermann.

En realidad, Mike me envió su pregunta por correo electrónico, pero entonces no se me ocurrió esta respuesta y le sugerí que publicara la pregunta aquí. No sé si este es el resultado buscado, o simplemente un resultado similar. Tampoco veo la manera de argumentar de forma convincente que los resultados asintóticos son obsoletos. Es cierto que como algunos problemas computacionales son asintóticamente lentos, se puede hacer una secuencia de problemas computacionales que sean todos asintóticamente rápidos, pero con un factor constante cada vez peor.