Lógica de punto fijo

Concepto en lógica matemática

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 estado 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 fue presentada a los científicos informáticos en 1979, cuando Alfred Aho y Jeffrey Ullman sugirieron la lógica de punto fijo como un lenguaje expresivo de consulta de bases de datos. ^[2]

Lógica de punto fijo parcial

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

Sea k un entero, 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 de manera que y (es decir, φ con sustituye a la variable de segundo orden P ). Entonces, o bien hay un punto fijo, o bien la lista de s es cíclica. ^[3] ${\displaystyle x,y}$ ${\displaystyle (P_{i})_{i\in N}}$ ${\displaystyle P_{0}(x)=false}$ ${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$ ${\displaystyle P_{i-1}}$ ${\displaystyle (P_{i})}$

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

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

Lógica de mínimo punto fijo

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 tales fórmulas φ que solo contienen ocurrencias positivas de P (es decir, ocurrencias precedidas por un número par de negaciones). Esto garantiza la monotonía de la construcción del punto fijo (es decir, si la variable de segundo orden es P , entonces siempre implica ). ${\displaystyle P_{i}(x)}$ ${\displaystyle P_{i+1}(x)}$

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

La expresividad de la lógica del punto mínimo fijo 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]

Lógica inflacionaria de punto fijo

Otra forma de garantizar la monotonía de la construcción de punto fijo es agregar nuevas tuplas a en cada etapa de la iteración, sin eliminar las tuplas para las que ya no se cumple. Formalmente, definimos como donde . ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \operatorname {IFP} (\phi _{P,x})}$ ${\displaystyle \operatorname {PFP} (\psi _{P,x})}$ ${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$

Este punto fijo inflacionario concuerda con el punto menos fijo cuando este último se define. Aunque a primera vista parece como si la lógica de punto fijo inflacionario debería ser más expresiva que la lógica de punto menos fijo ya que admite una gama más amplia de argumentos de punto fijo, de hecho, cada FO[IFP]( X )-fórmula es equivalente a una FO[LFP]( X )-fórmula. ^[10]

Inducción simultánea

Si bien todos los operadores de punto fijo introducidos hasta ahora iteraban solo sobre la definición de un solo predicado, muchos programas informáticos se consideran más naturalmente como si iteraran sobre varios predicados simultáneamente. Ya sea aumentando la aridad de los operadores de punto fijo o anidándolos, cada operador de punto fijo mínimo, inflacionario o parcial simultáneo puede, de hecho, expresarse utilizando las construcciones de iteración única correspondientes analizadas anteriormente. ^[11]

Lógica de cierre transitivo

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

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

TC se define de la siguiente manera: Sea k un entero positivo y vectores de k variables. Entonces es verdadero si existen n vectores de variables tales que , y para todo , es verdadero. Aquí, φ es una fórmula escrita en FO(TC) y significa que las variables u y v se reemplazan por x e y . ${\displaystyle u,v,x,y}$ ${\displaystyle {\mathsf {TC}}(\phi _{u,v})(x,y)}$ ${\displaystyle (z_{i})}$ ${\displaystyle z_{1}=x,z_{n}=y}$ ${\displaystyle i<n}$ ${\displaystyle \phi (z_{i},z_{i+1})}$ ${\displaystyle \phi (x,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]

Lógica de cierre transitivo determinista

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 todo u , existe como máximo un v tal que . ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$ ${\displaystyle \phi (u,v)}$

Podemos suponer que es azúcar sintáctico para donde . ${\displaystyle \operatorname {DTC} (\phi _{u,v})}$ ${\displaystyle \operatorname {TC} (\psi _{u,v})}$ ${\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]

Iteraciones

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

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

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

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

• ${\displaystyle {\mathsf {FO}}[(\log n)^{i}]}$es igual a AC FO-uniforme ⁱ , y de hecho es AC FO-uniforme de profundidad . ^[15] ${\displaystyle {\mathsf {FO}}[t(n)]}$ ${\displaystyle t(n)}$
• ${\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]

Notas

1. Moschovakis, Yiannis N. (1974). "Inducción elemental sobre estructuras abstractas". Estudios de lógica y fundamentos de las matemáticas . 77. doi :10.1016/s0049-237x(08)x7092-2. ISBN. 9780444105370. ISSN  0049-237X.
2. Aho, Alfred V.; Ullman, Jeffrey D. (1979). "Universalidad de los lenguajes de recuperación de datos". Actas del 6º Simposio ACM SIGACT-SIGPLAN sobre Principios de Lenguajes de Programación - POPL '79 . Nueva York, Nueva York, EE. UU.: ACM Press: 110–119. doi : 10.1145/567752.567763 . S2CID  3242505.
3. Ebbinghaus y Flum, pág. 121
4. Ebbinghaus y Flum, pág. 121
5. Immerman 1999, pág. 161
6. Abiteboul, S.; Vianu, V. (1989). "Extensiones de punto fijo de la lógica de primer orden y lenguajes similares a los de registro de datos". [1989] Actas. Cuarto Simposio Anual sobre Lógica en Ciencias de la Computación . IEEE Comput. Soc. Press. págs. 71–79. doi :10.1109/lics.1989.39160. ISBN 0-8186-1954-6.S2CID206437693  .​
7. 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 .
8. Vardi, Moshe Y. (1982). "La complejidad de los lenguajes de consulta relacionales (Resumen ampliado)". Actas del decimocuarto simposio anual de la ACM sobre teoría de la computación - STOC '82 . Nueva York, NY, EE. UU.: ACM. pp. 137–146. CiteSeerX 10.1.1.331.6045 . doi :10.1145/800070.802186. ISBN .  978-0897910705.S2CID 7869248  .
9. Ebbinghaus y Flum, pág. 242
10. Yuri Gurevich y Saharon Shelah, Extensión de punto fijo de la lógica de primer orden, Annals of Pure and Applied Logic 32 (1986) 265--280.
11. Ebbinghaus y Flum, págs. 179, 193
12. Immerman, Neil (1983). "Lenguajes que capturan clases de complejidad". Actas del decimoquinto simposio anual de la ACM sobre teoría de la computación - STOC '83 . Nueva York, Nueva York, EE. UU.: ACM Press. pp. 347–354. doi :10.1145/800061.808765. ISBN 0897910990.S2CID 7503265  .
13. Immerman, Neil (1988). "El espacio no determinista está cerrado bajo complementación". Revista SIAM de Computación . 17 (5): 935–938. doi :10.1137/0217058. ISSN  0097-5397.
14. Immerman 1999, pág. 63
15. Immerman 1999, pág. 82
16. Immerman 1999, pág. 84
17. Immerman 1999, pág. 58
18. Immerman 1999, pág. 161

Referencias

• 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-6.OCLC 901297152  .