Lógica de punto fijo

En lógica matemática , las lógicas de punto fijo son extensiones de la lógica de predicados clásica que se han introducido para expresar la recursión. Su desarrollo ha sido motivado por la teoría de la complejidad descriptiva y su relación con los lenguajes de consulta de bases de datos , en particular con Datalog .

La lógica de punto fijo mínimo fue estudiada sistemáticamente por primera vez por Yiannis N. Moschovakis en 1974, ^{[ 1 ]} y se introdujo a los científicos informáticos en 1979, cuando Alfred Aho y Jeffrey Ullman sugirieron la lógica de punto fijo como un lenguaje de consulta de bases de datos expresivo. ^{[ 2 ]}

Para una signatura relacional X , FO[PFP]( X ) es el conjunto de fórmulas formadas a partir de X utilizando conectores y predicados de primer orden , variables de segundo orden y un operador de punto fijo parcial.${\displaystyle \operatorname {PFP} }$utilizado para formar fórmulas de la forma${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$, dónde${\displaystyle P}$es una variable de segundo orden,${\displaystyle {\vec {x}}}$una tupla de variables de primer orden,${\displaystyle {\vec {t}}}$una tupla de términos y las longitudes de${\displaystyle {\vec {x}}}$y${\displaystyle {\vec {t}}}$coincidir con la aridad de${\displaystyle P}$.

Sea k un número entero,${\displaystyle x,y}$Sean vectores de k variables, P una variable de segundo orden de aridad k , y sea φ una función FO(PFP,X) que utiliza x y P como variables. Podemos definir iterativamente${\displaystyle (P_{i})_{i\in N}}$de tal manera que${\displaystyle P_{0}(x)=falso}$y${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$(que significa φ con${\displaystyle P_{i-1}}$sustituido por la variable de segundo orden P ). Entonces, o bien hay un punto fijo, o bien la lista de${\displaystyle (P_{i})}$s es cíclico. ^{[ 3 ]}

${\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}$se define como el valor del punto fijo de${\displaystyle (P_{i})}$en${\displaystyle {\vec {t}}}$si hay un punto fijo, de lo contrario es falso. ^{[ 4 ]} Dado que P s son propiedades de aridad k , hay como máximo${\displaystyle 2^{n^{k}}}$valores para el${\displaystyle P_{i}}$s, por lo que con un contador de espacio polinomial podemos comprobar si hay un bucle o no. ^{[ 5 ]}

Se ha demostrado que en estructuras finitas ordenadas, una propiedad es expresable en FO(PFP, X ) si y solo si se encuentra en PSPACE . ^{[ 6 ]}

Dado que los predicados iterados involucrados en el cálculo del punto fijo parcial no son en general monótonos, el punto fijo puede no existir siempre. FO(LFP,X), lógica de punto fijo mínimo , es el conjunto de fórmulas en FO(PFP,X) donde el punto fijo parcial se toma solo sobre aquellas fórmulas φ que solo contienen ocurrencias positivas de P (es decir, ocurrencias precedidas por un número par de negaciones). Esto garantiza la monotonicidad de la construcción del punto fijo (es decir, si la variable de segundo orden es P , entonces${\displaystyle P_{i}(x)}$siempre implica${\displaystyle P_{i+1}(x)}$).

Debido a la monotonicidad, solo agregamos vectores a la tabla de verdad de P , y como solo hay${\displaystyle n^{k}}$vectores posibles siempre encontraremos un punto fijo antes${\displaystyle n^{k}}$iteraciones. El teorema de Immerman-Vardi, demostrado independientemente por Immerman ^{[ 7 ]} y Vardi , ^{[ 8 ]} muestra que FO(LFP, X ) caracteriza P en todas las estructuras ordenadas.

La expresividad de la lógica de punto fijo mínimo coincide exactamente con la expresividad del lenguaje de consulta de bases de datos Datalog , lo que demuestra que, en estructuras ordenadas, Datalog puede expresar exactamente aquellas consultas ejecutables en tiempo polinomial. ^{[ 9 ]}

Otra forma de asegurar la monotonicidad de la construcción de punto fijo es agregando solo nuevas tuplas a${\displaystyle P}$en cada etapa de la iteración, sin eliminar tuplas para las cuales${\displaystyle P}$ya no es válido. Formalmente, definimos${\displaystyle \operatorname {IFP} (\phi _{P,x})}$como${\displaystyle \operatorname {PFP} (\psi _{P,x})}$dónde${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$.

Este punto fijo inflacionario coincide con el punto fijo mínimo donde este último está definido. Aunque a primera vista parece que la lógica de punto fijo inflacionario debería ser más expresiva que la lógica de punto fijo mínimo, ya que admite una gama más amplia de argumentos de punto fijo, de hecho, toda fórmula FO[IFP]( X ) es equivalente a una fórmula FO[LFP]( X ). ^{[ 10 ]}

Si bien todos los operadores de punto fijo introducidos hasta ahora iteraban únicamente sobre la definición de un solo predicado, muchos programas informáticos se conciben de forma más natural como iterando sobre varios predicados simultáneamente. Al aumentar la aridad de los operadores de punto fijo o al anidarlos, cualquier operador de punto fijo simultáneo, ya sea mínimo, inflacionario o parcial, puede expresarse utilizando las construcciones de una sola iteración correspondientes que se han comentado anteriormente. ^{[ 11 ]}

En lugar de permitir la inducción sobre predicados arbitrarios, la lógica de cierre transitivo solo permite que los cierres transitivos se expresen directamente.

FO[TC]( X ) es el conjunto de fórmulas formadas a partir de X utilizando conectores y predicados de primer orden, variables de segundo orden y un operador de cierre transitivo.${\displaystyle \operatorname {TC} }$utilizado para formar fórmulas de la forma${\displaystyle [\operatorname {TC} _{{\vec {x}},{\vec {y}}}\varphi ]{\vec {s}}{\vec {t}}}$, dónde${\displaystyle {\vec {x}}}$y${\displaystyle {\vec {y}}}$son tuplas de variables de primer orden distintas entre sí,${\displaystyle {\vec {t}}}$y${\displaystyle {\vec {s}}}$tuplas de términos y longitudes de${\displaystyle {\vec {x}}}$,${\displaystyle {\vec {y}}}$,${\displaystyle {\vec {s}}}$y${\displaystyle {\vec {t}}}$coincidir.

TC se define de la siguiente manera: Sea k un entero positivo y${\displaystyle u,v,x,y}$sean vectores de k variables. Entonces${\displaystyle {\mathsf {TC}}(\varphi _{u,v})(x,y)}$es cierto si existen n vectores de variables${\displaystyle (z_{i})}$de tal manera que${\displaystyle z_{1}=x,z_{n}=y}$y para todos${\displaystyle i<n}$,${\displaystyle \varphi (z_{i},z_{i+1})}$es cierto. Aquí, φ es una fórmula escrita en FO(TC) y${\displaystyle \varphi (x,y)}$significa que las variables u y v se reemplazan por x e y .

Sobre estructuras ordenadas, FO[TC] caracteriza la clase de complejidad NL . ^{[ 12 ]} Esta caracterización es una parte crucial de la prueba de Immerman de que NL es cerrada bajo complemento (NL = co-NL). ^{[ 13 ]}

FO[DTC]( X ) se define como FO(TC,X) donde el operador de cierre transitivo es determinista. Esto significa que cuando aplicamos${\displaystyle \operatorname {DTC} (\phi _{u,v})}$Sabemos que para todo u , existe como máximo un v tal que${\displaystyle \phi (u,v)}$.

Podemos suponer que${\displaystyle \operatorname {DTC} (\phi _{u,v})}$es azúcar sintáctico para${\displaystyle \operatorname {TC} (\psi _{u,v})}$dónde${\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x(x=v\vee \neg \phi (u,x))}$.

Sobre estructuras ordenadas, FO[DTC] caracteriza la clase de ^complejidad L. [ ^{12 ]}

Definir un vértice${\displaystyle x}$ser débil si, con como máximo una excepción${\displaystyle y}$, cada uno de sus vecinos${\displaystyle z}$es débil, según la fórmula de punto fijo${\displaystyle W(x)\leftarrow \exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee W(z)){\bigr )}}$Los vértices restantes forman el núcleo 2 del grafo.

La siguiente fórmula escrita en lógica de mínimos puntos fijos establece que el núcleo 2 de un grafo no está vacío: $${\displaystyle \exists t[\operatorname {LFP} _{x,P}\exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee P(z)){\bigr )}]t}$$

Un grafo es conexo si existe un camino entre cada par de vértices. El hecho de que exista un camino entre dos vértices constituye el cierre transitivo de la relación de adyacencia. Por lo tanto, la siguiente fórmula, escrita en lógica de cierre transitivo, establece que un grafo es conexo: $${\displaystyle \forall s\forall t[\operatorname {TC} _{x,y}x\sim y]st}$$

Las operaciones de punto fijo que hemos definido hasta ahora iteran indefinidamente las definiciones inductivas de los predicados mencionados en la fórmula, hasta alcanzar un punto fijo. En las implementaciones, puede ser necesario limitar el número de iteraciones para reducir el tiempo de cálculo. Los operadores resultantes también son de interés desde un punto de vista teórico, ya que pueden utilizarse para caracterizar clases de complejidad.

Definiremos el primer orden con iteración,${\displaystyle {\mathsf {FO}}[t(n)]}$; aquí${\displaystyle t(n)}$es una (clase de) funciones de enteros a enteros, y para diferentes clases de funciones${\displaystyle t(n)}$obtendremos diferentes clases de complejidad${\displaystyle {\mathsf {FO}}[t(n)]}$.

En esta sección escribiremos ${\displaystyle (\forall xP)Q}$significar${\displaystyle (\forall x(P\Rightarrow Q))}$y${\displaystyle (\exists xP)Q}$significar${\displaystyle (\exists x(P\wedge Q))}$. Primero necesitamos definir los bloques cuantificadores (QB), un bloque cuantificador es una lista${\displaystyle (Q_{1}x_{1},\phi _{1})...(Q_{k}x_{k},\phi _{k})}$donde el${\displaystyle \phi _{i}}$s son fórmulas FO sin cuantificador y${\displaystyle Q_{i}}$s son o${\displaystyle \forall }$o${\displaystyle \exists }$. Si Q es un bloque de cuantificadores, entonces lo llamaremos${\displaystyle [Q]^{t(n)}}$el operador de iteración, que se define como Q escrito${\displaystyle t(n)}$tiempo. Hay que prestar atención a que aquí hay${\displaystyle k*t(n)}$cuantificadores en la lista, pero solo k variables y cada una de esas variables se utiliza${\displaystyle t(n)}$veces. ^{[ 14 ]}

Ahora podemos definir${\displaystyle {\mathsf {FO}}[t(n)]}$ser las fórmulas FO con un operador de iteración cuyo exponente está en la clase${\displaystyle t(n)}$y obtenemos las siguientes igualdades:

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$es igual a FO-uniform AC ⁱ , y de hecho${\displaystyle {\mathsf {FO}}[t(n)]}$es FO-AC uniforme de profundidad${\displaystyle t(n)}$. ^{[ 15 ]}
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$es igual a NC. ^{[ 16 ]}
• ${\displaystyle {\mathsf {FO}}[n^{O(1)}]}$es igual a PTIME . También es otra forma de escribir FO(IFP). ^{[ 17 ]}
• ${\displaystyle {\mathsf {FO}}[2^{n^{O(1)}}]}$es igual a PSPACE . También es otra forma de escribir FO(PFP). ^{[ 18 ]}

• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1999). Teoría de modelos finitos . Perspectivas en lógica matemática (2  ed.). Saltador. doi : 10.1007/978-3-662-03182-7 . ISBN 978-3-662-03184-1.
• Neil, Immerman (1999). Complejidad descriptiva . Springer. ISBN 0-387-98600-6OCLC 901297152​​