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 recursividad. Su desarrollo ha sido motivado por la teoría descriptiva de la complejidad y su relación con los lenguajes de consulta de bases de datos , en particular con Datalog .

La lógica de punto mínimo fue estudiada sistemáticamente por primera vez por Yiannis N. Moschovakis en 1974, ^[1] y se presentó 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 expresivo de bases de datos. ^[2]

Lógica parcial de punto fijo

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 y 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 número entero, sean vectores de k variables, P sea una variable de segundo orden de aridad k y sea φ una función FO(PFP,X) que utilice x y P como variables. Podemos definir iterativamente tal que y (es decir, φ sustituido por la variable de segundo orden P ). Entonces, o hay un punto fijo o 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 en y si hay un punto fijo; en caso contrario, es falso. ^[4] Dado que P s son propiedades de la 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 punto mínimo fijo

Dado que los predicados iterados involucrados en el cálculo del punto fijo parcial no son en general monótonos, es posible que el punto fijo no siempre exista. FO(LFP,X), lógica de punto mínimo fijo , es el conjunto de fórmulas en FO(PFP,X) donde el punto fijo parcial se toma sólo sobre aquellas fórmulas φ que sólo contienen ocurrencias positivas de P (es decir, ocurrencias precedidas por un número par de negaciones). Esto garantiza la monotonicidad de la construcción de 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 monotonicidad, solo agregamos vectores a la tabla de verdad de P , y como solo hay vectores posibles siempre encontraremos un punto fijo antes de las iteraciones. El teorema de Immerman-Vardi, mostrado 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 de 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 monotonicidad de la construcción de punto fijo es agregando solo nuevas tuplas en cada etapa de la iteración, sin eliminar las tuplas que ya no son válidas. Formalmente, definimos como dónde . ${\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 coincide con el punto menos fijo donde se define este último. Aunque a primera vista parece que la lógica inflacionaria de punto fijo 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, cada fórmula FO[IFP]( X ) es equivalente a una fórmula FO[LFP]( X ). ^[10]

Inducción simultánea

Si bien todos los operadores de punto fijo introducidos hasta ahora iteran sólo sobre la definición de un único predicado, es más natural pensar que muchos programas de computadora iteran sobre varios predicados simultáneamente. Ya sea aumentando la aridad de los operadores de punto fijo o anidándolos, cada punto fijo mínimo, inflacionario o parcial simultáneo puede de hecho expresarse utilizando las correspondientes construcciones de iteración única discutidas 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 expresar directamente cierres transitivos .

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 y un operador de cierre transitivo utilizado para formar fórmulas de la forma , donde y son tuplas de primeros pares distintos -variables de orden, 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 número entero positivo y sean vectores de k variables. Entonces es cierto si existen n vectores de variables tales que y para todos 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 cerrado bajo complemento (NL = co-NL). ^[13]

Lógica de cierre transitiva 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 dónde . ${\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 definimos hasta ahora iteran las definiciones inductivas de los predicados mencionados en la fórmula indefinidamente, 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 pueden usarse para caracterizar clases de complejidad.

Definiremos el primer orden con iteración ; Aquí hay una (clase de) funciones de enteros a 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 significar y significar . Primero necesitamos definir bloques cuantificadores (QB), un bloque cuantificador es una lista donde las s son fórmulas FO sin cuantificadores y las s son o . Si Q es un bloque de cuantificadores, llamaremos al operador de iteración, que se define como Q tiempo escrito . Hay que prestar atención 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 que son 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 FO- AC uniforme ⁱ , y de hecho es FO-AC uniforme de profundidad . ^[15] ${\displaystyle {\mathsf {FO}}[t(n)]}$ ${\displaystyle t(n)}$
• ${\displaystyle {\mathsf {FO}}[(\log n)^{O(1)}]}$es igual a NC. ^[dieciséis]
• ${\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. Ah, Alfred V.; Ullman, Jeffrey D. (1979). "Universalidad de los lenguajes de recuperación de datos". Actas del sexto simposio ACM SIGACT-SIGPLAN sobre principios de lenguajes de programación - POPL '79 . Nueva York, Nueva York, Estados Unidos: ACM Press: 110–119. doi : 10.1145/567752.567763 . S2CID  3242505.
3. Ebbinghaus y Flum, pag. 121
4. Ebbinghaus y Flum, pag. 121
5. Immerman 1999, pag. 161
6. Abiteboul, S.; Vianu, V. (1989). "Extensiones de Fixpoint de lógica de primer orden y lenguajes similares a registros de datos". [1989] Actas. Cuarto Simposio Anual sobre Lógica en Informática . Computación IEEE. Soc. Prensa. págs. 71–79. doi :10.1109/lics.1989.39160. ISBN 0-8186-1954-6. S2CID  206437693.
7. Immerman, Neil (1986). "Consultas relacionales computables en tiempo polinómico". 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 ACM sobre teoría de la informática - STOC '82 . Nueva York, NY, Estados Unidos: ACM. págs. 137-146. CiteSeerX 10.1.1.331.6045 . doi :10.1145/800070.802186. ISBN  978-0897910705. S2CID  7869248.
9. Ebbinghaus y Flum, pag. 242
10. Yuri Gurevich y Saharon Shelah, Extensión de punta fija 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 ACM sobre teoría de la informática - STOC '83 . Nueva York, Nueva York, Estados Unidos: ACM Press. págs. 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, pag. 63
15. Immerman 1999, pag. 82
16. Immerman 1999, pag. 84
17. Immerman 1999, pag. 58
18. Immerman 1999, pag. 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. Saltador. ISBN 0-387-98600-6. OCLC  901297152.