¿Existe una lógica sin inducción que capture gran parte de P?

38

El teorema de Immerman-Vardi establece que PTIME (o P) es precisamente la clase de lenguajes que puede describirse mediante una oración de lógica de primer orden junto con un operador de punto fijo, sobre la clase de estructuras ordenadas. El operador de punto fijo puede ser punto menos fijo (según lo considerado por Immerman y Vardi), o punto fijo inflacionario. (Stephan Kreutzer, equivalencia expresiva de la lógica de punto fijo mínimo e inflacionario , Annals of Pure and Applied Logic 130 61–78, 2004).

Yuri Gurevich conjeturó que no hay lógica que capture PTIME ( Logic and the Challenge of Computer Science , in Current Trends in Theoretical Computer Science, ed. Egon Boerger, 1–57, Computer Science Press, 1988), mientras que Martin Grohe ha declarado que es menos seguro ( The Quest for a Logic Capturing PTIME , FOCS 2008).

El operador de punto fijo está destinado a capturar el poder de la recursividad. Los puntos fijos son poderosos, pero no es obvio para mí que sean necesarios.

¿Existe un operador X que no se base en puntos fijos, de modo que FOL + X capture un fragmento (grande) de PTIME?

Editar: Hasta donde entiendo, la lógica lineal solo puede expresar declaraciones sobre estructuras que tienen una forma bastante restrictiva. Idealmente, me gustaría ver una referencia a, o un bosquejo de, una lógica que pueda expresar propiedades de conjuntos arbitrarios de estructuras relacionales, evitando al mismo tiempo puntos fijos. Si me equivoco sobre el poder expresivo de la lógica lineal, un puntero o sugerencia sería bienvenido.

András Salamon
fuente
2
Con "lógica" me refiero a lo que Grohe quiere decir: un conjunto decidible de oraciones sobre el vocabulario, y una relación "es un modelo de" entre estructuras finitas y oraciones, con la propiedad de que el conjunto de modelos de una oración siempre está cerrado bajo isomorfismo .
András Salamon
Consulte también cstheory.stackexchange.com/questions/174/… para saber si existe una lógica que capture PTIME.
András Salamon
La lógica lineal es una lógica proposicional que contiene la lógica proposicional clásica. Se puede ampliar para permitir cuantificadores. Pero si recuerdo correctamente la relación entre la lógica lineal (proposicional) y las clases de complejidad es diferente de lo que Grohe tiene en mente, al menos no veo cómo relacionar la lógica lineal con las consultas sobre estructuras finitas.
Kaveh
Hay teorías de conjuntos construidas en lógica lineal, como la Teoría de conjuntos afines a la luz de Terui, que tienen la propiedad de que una función puede demostrarse como total, si y solo si la función es computable en tiempo polinómico. Ver citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730
Neel Krishnaswami
1
Kaveh, es por eso que le otorgué la recompensa a Slimton. Una respuesta más detallada aún sería agradable.
András Salamon

Respuestas:

23

Desea echar un vistazo a lo que algunas personas llaman el Teorema de Grädel. Puede encontrarlo en el libro de Papadimitriou "Complejidad computacional" (es el Teorema 8.4 en la página 176) o en el artículo original de Grädel .

En pocas palabras, el Teorema de Grädel es para P lo que el Teorema de Fagin es para NP. Establece que en la clase de estructuras finitas con una relación sucesora, la colección de propiedades decidibles de tiempo polinomial coincide con las que se expresan en el fragmento Horn de la lógica existencial de segundo orden. Estas son las oraciones de lógica de segundo orden de la forma donde R es una secuencia de variables de relación de segundo orden,

(R)(X)(ϕ)
R es una secuencia de variables de primer orden y ϕ es un cuantificador libre de fórmula que, cuando está escrita en forma CNF, es una conjunción de RXϕR- Cláusulas de claxon (es decir, cláusulas que tienen como máximo un átomo no negado que involucra las variables en ).R
Slimton
fuente
3
Vaya, ahora que leí tu pregunta nuevamente, me di cuenta de que es un poco diferente de la versión anterior. Ahora solicita un operador X para que FOL + X capture un gran fragmento de P. En ese caso, debería echar un vistazo a <a href=" logcom.oxfordjournals.org/content/5/2/…> de Dawar . muestra que si hay una lógica para P, entonces hay una extendiendo FOL con cuantificadores generalizados.
slimton
3
Debo agregar que el fragmento Horn de la lógica existencial de segundo orden en estructuras desnudas es bastante débil: un subconjunto adecuado de LFP en estructuras desnudas. Necesitamos al sucesor para obtener el teorema de Grädel. El resultado de Dawar es para estructuras desnudas.
slimton
8
Hasta donde entiendo, la lógica lineal solo puede expresar declaraciones sobre estructuras que tienen una forma bastante restrictiva. Idealmente, me gustaría ver una referencia a, o un bosquejo de, una lógica que pueda expresar propiedades de conjuntos arbitrarios de estructuras relacionales, al tiempo que evita puntos fijos. Si me equivoco sobre el poder expresivo de la lógica lineal, un puntero o sugerencia sería bienvenido.

Esto no está bien: todas las redes monoidales conmutadas residuales son modelos de lógica lineal. Aquí hay una manera fácil de crear una red de este tipo a partir de gráficos finitos. Comienza con el set

METRO={(sol,norte)El |sol es un gráfico finito y nortenorteoremis(sol)}

Entonces, nuestra relación forzada será , y la intuición es que n es el conjunto de nodos "propiedad" de la fórmula ϕ . Hay una operación parcial ( ) : M × M M , definida como: ( g , n ) ( g , n ) = { ( g , n n ) cuando  g = g(sol,norte)ϕnorteϕ():METRO×METROMETRO

(sol,norte)(sol,norte)={(sol,nortenorte)cuando sol=solnortenorte=tunorteremiFyonortemirede otra manera

Esto combina dos elementos fusionando sus conjuntos propios, si los gráficos son iguales y los conjuntos propios son disjuntos.

Ahora, podemos dar un modelo de lógica lineal de la siguiente manera:

(sol,norte)yonorte=(sol,norte)ϕψnorte1,norte2.norte=norte1norte2 y (sol,norte1)ϕ y (sol,norte2)ψ(sol,norte)ϕψnorte.Si nortenorte= y (sol,norte)ϕ luego (sol,nortenorte)ψ(sol,norte)siempre(sol,norte)ϕψ(sol,norte)ϕ y (sol,norte)ψ

Este modelo es en realidad una variante de los utilizados en la lógica de separación, que se utiliza ampliamente en la verificación de programas de manipulación de montón. (Si lo desea, piense en el gráfico como la estructura de puntero del montón, ¡y la analogía es exacta!)

Sin embargo, esta no es realmente la forma correcta de pensar sobre la lógica lineal: sus intuiciones reales son teóricas de prueba, y la conexión con la complejidad se produce a través de la complejidad computacional del teorema de eliminación de cortes. La teoría modelo de la lógica lineal es la sombra proyectada por su teoría de la prueba.

Neel Krishnaswami
fuente
¿Qué papel juega la estructura gráfica en el modelo anterior? La definición anterior parece funcionar bien si decimos que g se extiende sobre los gráficos discretos.
Charles Stewart
nortenorte
8

Hay resultados recientes interesantes sobre la búsqueda de una lógica que capture PTIME. Sin embargo, el famoso ejemplo de Cai, Fürer e Immerman que muestra que LFP + C no captura PTIME se basó en una clase de gráficos aparentemente artificiales. Por supuesto, fue construido para la tarea particular de demostrar las restricciones de LFP + C. Recientemente, Dawar demostró que la clase no es artificial en absoluto. ¡Más bien puede verse como un ejemplo del hecho de que LFP + C no puede resolver sistemas de ecuaciones lineales!

Por lo tanto , Dawar, Grohe, Holm y Laubner extendieron las lógicas de los operadores de álgebra lineal, por ejemplo, de un operador para definir el rango de una matriz definible. El rango LFP + lógico resultante puede expresar estrictamente más que LFP + C, de hecho, no hay propiedad PTIME conocida que el rango LFP + no pueda expresar.

Incluso FO + rk es sorprendentemente poderoso, puede expresar cierre transitivo determinista y simétrico. Todavía está abierto si puede expresar el cierre transitivo general de un gráfico.

Sebastian Siebertz
fuente
1
Tenga en cuenta que Anderson / Dawar / Holm demostró recientemente que FP + C puede expresar programación lineal ( arxiv.org/abs/1304.6870 ). Esto socava una interpretación del resultado anterior de Dawar en la línea de "FP + C no puede resolver sistemas de ecuaciones lineales"; Dawar solo afirmó que algunos "problemas naturales que involucran sistemas de ecuaciones lineales no son definibles en esta lógica" con lo que parece haber significado cálculos de rango.
András Salamon
7

Dependiendo de lo que quiera decir con "captura", la lógica lineal suave y el tiempo polinómico de Yves Lafont pueden ser de interés. Hay una correspondencia de 1-1 con las pruebas en esta lógica y algoritmos PTIME que toman una cadena como entrada y salida 0 o 1.

do

Aaron Sterling
fuente
1
Creo que András quiere una lógica en el sentido de la complejidad descriptiva.
Kaveh
7

Algunos trabajos anteriores sobre este problema, nuevamente en la línea de lógica lineal, son Jean-Yves Girard, Andre Scedrov y Philip Scott. Lógica lineal limitada: un enfoque modular para la computabilidad en tiempo polinomial. Informática teórica, 97 (1): 1–66, 1992.

El trabajo más reciente incluye Bounded Linear Logic, revisitado por Ugo Dal Lago y Martin Hofmann.

Dave Clarke
fuente