Intuición detrás de sistemas de prueba

9

Estoy tratando de entender el documento sobre p-Optimal Proof Systems and Logic para PTIME . Hay una noción llamada sistemas de prueba en el documento y no entiendo:

Σ={0 0,1} ... Identificamos problemas con subconjuntos deQ enΣ .

Creo que la intuición es que codificamos una determinada estructura en (por ejemplo, gráficos no dirigidos) y los subconjuntos de estas estructuras son problemas (por ejemplo, gráficos planos).Σ

Un sistema de prueba para un problema es una función sobreyectiva computable en tiempo polinómico. P : Σ QQΣPAGS:ΣQ

Ahora, una posibilidad es decir es el conjunto de todos los modelos posibles en una determinada estructura (por ejemplo, todos los gráficos no dirigidos). Pero eso no tiene sentido porque ¿por qué deberían asignarse gráficos no dirigidos en un subconjunto? Podría codificarse en máquinas de turing, pero esto tampoco tiene sentido ...Σ

¿Algunas ideas?

Joaquín
fuente

Respuestas:

8

Piense en codifica algún tipo de objeto, y Q como el conjunto de todos los objetos que satisfacen alguna propiedad. Piense P como una función que acepta (la codificación de) un par ( x , p ) , donde x es un objeto y p se alega "prueba" de x Q . La función P es un "comprobador de pruebas": verifica que p realmente representa evidencia válida de queΣQPAGS(X,pags)XpxQPp . Si es así, devuelve x , de lo contrario, devuelve un elemento por defecto de Q .xQxQ

Como ejemplo, supongamos que codifica gráficos y deja que Q sea ​​el conjunto (de codificaciones) de gráficos hamiltonianos. Una posible P es esta: decodificar la entrada como ( G , ) donde G es un gráfico y es una lista de vértices de GΣQP(G,)GG ; verificar que es un ciclo hamiltoniano en G ; si es así, devuelva G; de lo contrario, devuelva el gráfico en un punto.GG

Consideraste el caso de los gráficos planos. Para obtener una adecuada , necesitamos una noción de evidencia de planaridad comprobable en el tiempo múltiple.P

En general, la entrada a no necesita codificar un par ( x , p ) . Lo importante es que P puede extraer dos datos de su entrada: el objeto en cuestión y la supuesta evidencia de que el objeto pertenece a QP(x,p)PQ . Por ejemplo, tomemos como el conjunto de todas las oraciones demostrables en alguna teoría de primer orden. Ahora P decodifica su entrada como una prueba formal. Si la codificación no es válida, devuelve QP. Si la codificación representa una prueba válida, devuelve la declaración que fue probada por la prueba (que probablemente sea la raíz del árbol de prueba, o la última fórmula en una secuencia de declaraciones, dependiendo de cómo formalice las pruebas).

Andrej Bauer
fuente
5

Usted debe pensar en la entrada del sistema de prueba como el texto de una prueba de π de un elemento q Q . Si el texto es válido que P ( π ) = q , de lo contrario P ( π ) es algunos fijo q 0Q . Queremos que P sea ​​polytime ya que eso significa que la prueba es fácil de verificar.PπqQP(π)=qP(π)q0QP

Como ejemplo, supongamos que es el conjunto de tautologías proposicionales, y P es cualquier sistema de prueba de estilo Hilbert, que consiste en un conjunto de líneas , cada una de las cuales es un axioma o se sigue de líneas anteriores a través de una regla de derivación (generalmente Modus Ponens). Si la prueba es válida, esa P debería mostrar la última línea de la prueba. De lo contrario, genere alguna tautología fija como p ¬ p .QPPp¬p

Volviendo a su primera pregunta, es una codificación de todas las estructuras de cierto tipo que satisfacen alguna propiedad. Un ejemplo son las tautologías. Otro ejemplo es el conjunto de todos los gráficos no coloreables en 3, que tienen un sistema de prueba conocido como cálculo de Hajós.Q

Yuval Filmus
fuente