En la complejidad descriptiva , una rama de la complejidad computacional , FO es una clase de complejidad de estructuras que pueden ser reconocidas por fórmulas de lógica de primer orden , y también es igual a la clase de complejidad AC 0 . La complejidad descriptiva usa el formalismo de la lógica, pero no usa varias nociones clave asociadas con la lógica, como la teoría de la prueba o la axiomatización.
Restringir predicados para que sean de un conjunto X produce una clase FO [ X ] más pequeña . Por ejemplo, FO [<] es el conjunto de idiomas sin estrellas . Las dos definiciones diferentes de FO [<], en términos de lógica y en términos de expresiones regulares, sugieren que esta clase puede ser matemáticamente interesante más allá de su papel en la complejidad computacional, y que los métodos tanto de la lógica como de las expresiones regulares pueden ser útiles en su estudio.
De manera similar, las extensiones de la lógica de primer orden formadas por la adición de operadores dan lugar a otras clases de complejidad bien conocidas. [1] Esto permite establecer la complejidad de algunos problemas sin referencia a algoritmos .
Definición y ejemplos
La idea
Cuando usamos el formalismo lógico para describir un problema computacional, la entrada es una estructura finita y los elementos de esa estructura son el dominio del discurso . Por lo general, la entrada es una cadena (de bits o sobre un alfabeto) y los elementos de la estructura lógica representan las posiciones de la cadena, o la entrada es un gráfico y los elementos de la estructura lógica representan sus vértices. La longitud de la entrada se medirá por el tamaño de la estructura respectiva. Cualquiera que sea la estructura, podemos asumir que hay relaciones que se pueden probar, por ejemplo "es cierto si y sólo si existe un borde de x a y "(en el caso de la estructura de ser un gráfico), o"es cierto si y sólo si el n º letra de la cadena es de 1." Estas relaciones son los predicados para el sistema de la lógica de primer orden. También tenemos constantes, que son elementos especiales de la estructura respectiva, por ejemplo, si queremos comprobar la accesibilidad de un gráfico, tendremos que elegir dos constantes s (inicio) y t (terminal).
En la teoría de la complejidad descriptiva casi siempre suponemos que existe un orden total sobre los elementos y que podemos comprobar la igualdad entre los elementos. Esto nos permite considerar los elementos como números: el elemento x representa el número n sielementos y con. Gracias a esto también podemos tener el predicado primitivo "bit", dondees cierto si solo el k- ésimo bit de la expansión binaria de n es 1. (Podemos reemplazar la suma y la multiplicación por relaciones ternarias tales que es cierto si y es cierto si ).
Formalmente
Sea X un conjunto de predicados en. El lenguaje FO [ X ] se define como el cierre por conjunción (), negación () y cuantificación universal () sobre elementos de las estructuras. Cuantificación existencial () y disyunción () también se utilizan con frecuencia, pero pueden definirse mediante los tres primeros símbolos. El caso base son los predicados de X aplicados a algunas variables. Uno siempre tiene implícitamente un predicadopara cada letra a de un alfabeto, indicando que la letra en la posición x es una a .
La semántica de las fórmulas en FO es sencilla, es verdadero si A es falso,es verdadero si A es verdadero y B es verdadero, y es cierto si es cierto para todos los valores v que puede tomar x en el universo subyacente. Para P un predicado c -ary, es cierto si y solo si cuando se interpreta como es verdad.
Propiedad
Advertencia
Una consulta en FO será entonces para verificar si una fórmula de primer orden es verdadera sobre una estructura dada que representa la entrada al problema. No se debe confundir este tipo de problema con verificar si una fórmula booleana cuantificada es verdadera, que es la definición de QBF , que es PSPACE-complete . La diferencia entre esos dos problemas es que en QBF el tamaño del problema es el tamaño de la fórmula y los elementos son solo variables booleanas, mientras que en FO el tamaño del problema es el tamaño de la estructura y la fórmula es fija.
Esto es similar a la complejidad parametrizada, pero el tamaño de la fórmula no es un parámetro fijo.
Forma normal
Sin tener en cuenta las estructuras vacías, cada fórmula es equivalente a una fórmula en forma normal prenex (donde todos los cuantificadores se escriben primero, seguidos de una fórmula sin cuantificadores).
Operadores
FO sin operadores
En la complejidad del circuito , FO (ARB) donde ARB es el conjunto de todos los predicados, la lógica en la que podemos usar predicados arbitrarios, se puede demostrar que es igual a AC 0 , la primera clase en la jerarquía de AC . De hecho, existe una traducción natural de los símbolos de FO a nodos de circuitos, con ser y de tamaño n .
FO (BIT) es la restricción de la familia de circuitos AC 0 construible en tiempo logarítmico alterno . FO (<) es el conjunto de idiomas sin estrellas .
El punto fijo parcial es PSPACE
FO (PFP, X ) es el conjunto de consultas booleanas definibles en FO (X) donde agregamos un operador de punto fijo parcial.
Sea k un número entero,ser vectores de k variables, P ser una variable de segundo orden de aridad k , y φ ser una función FO (PFP, X) usando x y P como variables. Podemos definir iterativamente tal que y (que significa φ consustituida por la variable de segundo orden P ). Entonces, hay un punto fijo o la lista des es cíclico.
se define como el valor del punto fijo de en y si hay un punto fijo, de lo contrario como falso. Dado que P s son propiedades de aridad k , hay como máximo valores para el s, por lo que con un contador de espacio polinomial podemos verificar si hay un bucle o no.
Se ha comprobado que FO (PFP, BIT) es igual a PSPACE . Esta definición es equivalente a.
El punto mínimo fijo es P
FO (LFP, X) es el conjunto de consultas booleanas definibles en FO (PFP, X) donde el punto fijo parcial se limita a ser monótono. Es decir, si la variable de segundo orden es P , entonces siempre implica .
Podemos garantizar la monotonicidad restringiendo la fórmula φ para que solo contenga apariciones positivas de P (es decir, apariciones precedidas por un número par de negaciones). Alternativamente podemos describir como dónde .
Debido a la monotonicidad, solo agregamos vectores a la tabla de verdad de P , y dado que solo hay posibles vectores siempre encontraremos un punto fijo antes iteraciones. El teorema Immerman-Vardi, que se muestra de forma independiente por Immerman [2] y Vardi , [3] muestra que FO (LFP, BIT) = P . Esta definición es equivalente a.
El cierre transitivo es NL
FO (TC, X) es el conjunto de consultas booleanas definibles en FO (X) con un operador de cierre transitivo (TC).
TC se define de esta manera: sea k un entero positivo yser vector de k variables. Luegoes cierto si existen n vectores de variables tal que y para todos , es verdad. Aquí, φ es una fórmula escrita en FO (TC) ysignifica que las variables u y v se reemplazan por x e y .
FO (TC, BIT) es igual a NL .
El cierre transitivo determinista es L
FO (DTC, X) se define como FO (TC, X) donde el operador de cierre transitivo es determinista. Esto significa que cuando aplicamos, sabemos que para todas las u , existe a lo sumo una v tal que.
Podemos suponer que es azúcar sintáctico para dónde .
Se ha demostrado que FO (DTC, BIT) es igual a L .
Forma normal
Cualquier fórmula con un operador de punto fijo (resp. Cierre transitivo) puede escribirse sin pérdida de generalidad con exactamente una aplicación de los operadores aplicada a 0 (resp. )
Iterando
Definiremos el primer orden con iteración, ; aquí es una (clase de) funciones de enteros a enteros, y para diferentes clases de funciones obtendremos diferentes clases de complejidad .
En esta sección escribiremos significar y significar . Primero necesitamos definir bloques cuantificadores (QB), un bloque cuantificador es una lista donde el s son fórmulas de FO libres de cuantificadores ys son o o . Si Q es un bloque de cuantificadores, llamaremosel operador de iteración, que se define como Q escritohora. Hay que prestar atención a que aquí haycuantificadores en la lista, pero solo se usan k variables y cada una de esas variables veces.
Ahora podemos definir para ser las fórmulas FO con un operador de iteración cuyo exponente está en la clase , y obtenemos esas igualdades:
Lógica sin relaciones aritméticas
Sea la relación sucesora, succ , una relación binaria tal que es cierto si y solo si .
Sobre la lógica de primer orden, succ es estrictamente menos expresivo que <, que es menos expresivo que +, que es menos expresivo que bit , mientras que + y × son tan expresivos como bit .
Usando sucesor para definir bit
Es posible definir las relaciones más y luego las de bit con un cierre transitivo determinista.
y
con
Esto solo significa que cuando consultamos el bit 0, verificamos la paridad y vamos a (1,0) si a es impar (que es un estado de aceptación), de lo contrario, lo rechazamos. Si revisamos un poco, dividimos a entre 2 y comprobamos el bit.
Por tanto, no tiene sentido hablar de operadores con sucesor solo, sin los otros predicados.
Lógicas sin sucesor
FO [LFP] y FO [PFP] son dos lógicas sin predicados, aparte de los predicados de igualdad entre variables y los predicados de letras. Son iguales, respectivamente, a relacional-P y FO (PFP) es relacional-PSPACE , las clases P y PSPACE sobre máquinas relacionales . [4]
El Teorema de Abiteboul-Vianu establece que FO (LFP) = FO (PFP) si y solo si FO (<, LFP) = FO (<, PFP), por lo tanto, si y solo si P = PSPACE. Este resultado se ha extendido a otros puntos fijos. [4] Esto muestra que el problema de orden en primer orden es más un problema técnico que fundamental.
Referencias
- Ronald Fagin , Espectros de primer orden generalizados y conjuntos reconocibles de tiempo polinómico . Complejidad de la Computación , ed. R. Karp, SIAM-AMS Proceedings 7, págs. 27–41. 1974.
- Ronald Fagin, teoría del modelo finito: una perspectiva personal . Informática teórica 116, 1993, págs. 3-31.
- Neil Immerman. Idiomas que capturan clases de complejidad . 15º Simposio ACM STOC , págs. 347–354. 1983.
- ^ Immerman, Neil (1999). Complejidad descriptiva . Saltador. ISBN 978-0-387-98600-5.
- ^ Immerman, Neil (1986). "Consultas relacionales computables en tiempo polinomial" . Información y control . 68 (1-3): 86-104. doi : 10.1016 / s0019-9958 (86) 80029-8 .
- ^ Vardi, Moshe Y. (1982). La complejidad de los lenguajes de consulta relacionales (resumen extendido) . Actas del Decimocuarto Simposio Anual ACM sobre Teoría de la Computación . STOC '82. Nueva York, NY, EE.UU .: ACM. págs. 137-146. CiteSeerX 10.1.1.331.6045 . doi : 10.1145 / 800070.802186 . ISBN 978-0897910705.
- ^ a b Serge Abiteboul, Moshe Y. Vardi , Victor Vianu : Lógicas de puntos de fijación, máquinas relacionales y complejidad computacional Revista del archivo ACM, Volumen 44, Número 1 (enero de 1997), Páginas: 30-56, ISSN 0004-5411
enlaces externos
- Página de complejidad descriptiva de Neil Immerman , que incluye un diagrama
- Complexity zoo about FO , ver también las siguientes clases