Teoría de modelos finitos

La teoría de modelos finitos es una subárea de la teoría de modelos . La teoría de modelos es la rama de la lógica que estudia la relación entre un lenguaje formal (sintaxis) y sus interpretaciones (semántica). La teoría de modelos finitos es una restricción de la teoría de modelos a las interpretaciones sobre estructuras finitas , que tienen un universo finito.

Dado que muchos teoremas centrales de la teoría de modelos no se sostienen cuando se restringen a estructuras finitas, la teoría de modelos finitos es bastante diferente de la teoría de modelos en sus métodos de prueba. Los resultados centrales de la teoría de modelos clásica que fallan para estructuras finitas bajo la teoría de modelos finitos incluyen el teorema de compacidad , el teorema de completitud de Gödel y el método de ultraproductos para lógica de primer orden (FO). Si bien la teoría de modelos tiene muchas aplicaciones para el álgebra matemática , la teoría de modelos finitos se convirtió en un instrumento "inusualmente efectivo" ^[1] en la ciencia de la computación. En otras palabras: "En la historia de la lógica matemática, la mayor parte del interés se ha concentrado en las estructuras infinitas. [...] Sin embargo, los objetos que las computadoras tienen y sostienen son siempre finitos. Para estudiar la computación necesitamos una teoría de estructuras finitas". ^[2] Por lo tanto, las principales áreas de aplicación de la teoría de modelos finitos son: teoría de la complejidad descriptiva , teoría de bases de datos y teoría del lenguaje formal .

Axiomatización

Una pregunta motivadora común en la teoría de modelos finitos es si una clase dada de estructuras puede describirse en un lenguaje dado. Por ejemplo, uno podría preguntar si la clase de grafos cíclicos puede distinguirse entre grafos mediante una oración FO, que también puede formularse como si la ciclicidad es expresable mediante FO.

Una única estructura finita siempre puede axiomatizarse en lógica de primer orden , donde axiomatizada en un lenguaje L significa descrita de forma única hasta el isomorfismo por una única oración L. De manera similar, cualquier colección finita de estructuras finitas siempre puede axiomatizarse en lógica de primer orden. Algunas, pero no todas, colecciones infinitas de estructuras finitas también pueden axiomatizarse mediante una única oración de primer orden.

Caracterización de una estructura única

¿Es un lenguaje L lo suficientemente expresivo como para axiomatizar una única estructura finita S ?

Grafos individuales (1) y (1') que tienen propiedades comunes.

Problema

Una estructura como (1) en la figura puede describirse mediante oraciones FO en la lógica de gráficos como

1. Cada nodo tiene un borde con otro nodo: ${\displaystyle \forall _{x}\exists _{y}G(x,y).}$
2. Ningún nodo tiene una arista en sí mismo: ${\displaystyle \forall _{x,y}(G(x,y)\Rightarrow x\neq y).}$
3. Hay al menos un nodo que está conectado a todos los demás : ${\displaystyle \exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).}$

Sin embargo, estas propiedades no axiomatizan la estructura, ya que para la estructura (1') las propiedades anteriores también se cumplen, aunque las estructuras (1) y (1') no son isomorfas.

De manera informal, la pregunta es si al agregar suficientes propiedades, estas propiedades juntas describen exactamente (1) y no son válidas (todas juntas) para ninguna otra estructura (salvo el isomorfismo).

Acercarse

En el caso de una estructura finita única, siempre es posible describir con precisión la estructura mediante una única oración FO. El principio se ilustra aquí para una estructura con una relación binaria y sin constantes: ${\displaystyle R}$

1. digamos que hay al menos elementos: ${\displaystyle n}$ ${\displaystyle \varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})}$
2. digamos que hay como máximo elementos: ${\displaystyle n}$ ${\displaystyle \varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)}$
3. Indica cada elemento de la relación : ${\displaystyle R}$ ${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$
4. Indicar cada no elemento de la relación : ${\displaystyle R}$ ${\displaystyle \varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})}$

todo para la misma tupla , produciendo la oración FO . ${\displaystyle x_{1}..x_{n}}$ ${\displaystyle \exists _{x_{1}}\dots \exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})}$

Extensión a un número fijo de estructuras

El método de describir una estructura única mediante una oración de primer orden se puede extender fácilmente a cualquier número fijo de estructuras. Se puede obtener una descripción única mediante la disyunción de las descripciones para cada estructura. Por ejemplo, para dos estructuras y con oraciones definitorias y esto sería ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle \varphi _{A}}$ ${\displaystyle \varphi _{B}}$

${\displaystyle \varphi _{A}\lor \varphi _{B}.}$

Extensión a una estructura infinita

Por definición, un conjunto que contiene una estructura infinita queda fuera del área que aborda la FMT. Nótese que las estructuras infinitas nunca pueden discriminarse en FO, debido al teorema de Löwenheim-Skolem , que implica que ninguna teoría de primer orden con un modelo infinito puede tener un modelo único hasta el isomorfismo.

El ejemplo más famoso es probablemente el teorema de Skolem , que sostiene que existe un modelo aritmético contable y no estándar.

Caracterización de una clase de estructuras

¿Es un lenguaje L lo suficientemente expresivo para describir exactamente (hasta el isomorfismo) aquellas estructuras finitas que tienen cierta propiedad P ?

Conjunto de hasta n estructuras.

Problema

Las descripciones dadas hasta ahora especifican el número de elementos del universo. Desafortunadamente, la mayoría de los conjuntos de estructuras interesantes no están restringidos a un tamaño determinado, como todos los grafos que son árboles, están conectados o son acíclicos. Por lo tanto, discriminar un número finito de estructuras es de especial importancia.

Acercarse

En lugar de una declaración general, lo que sigue es un esbozo de una metodología para diferenciar entre estructuras que se pueden y no se pueden discriminar.

1. La idea central es que siempre que se quiera comprobar si una propiedad P puede expresarse en FO, se eligen las estructuras A y B , donde A sí tiene P y B no. Si para A y B se cumplen las mismas oraciones en FO, entonces P no puede expresarse en FO. En resumen:

   ${\displaystyle A\in P,B\not \in P}$y ${\displaystyle A\equiv B,}$

   donde es una abreviatura de para todas las oraciones FO α, y P representa la clase de estructuras con la propiedad P . ${\displaystyle A\equiv B}$ ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$
2. La metodología considera una cantidad contable de subconjuntos del lenguaje, cuya unión forma el lenguaje en sí. Por ejemplo, para FO, considere las clases FO[ m ] para cada m . Para cada m, entonces, debe demostrarse la idea central anterior, es decir:

   ${\displaystyle A\in P,B\not \in P}$y ${\displaystyle A\equiv _{m}B}$

   con un par para cada uno y α (en ≡) de FO[ m ]. Puede ser apropiado elegir las clases FO[ m ] para formar una partición del lenguaje. ${\displaystyle A,B}$ ${\displaystyle m}$
3. Una forma común de definir FO[ m ] es por medio del rango de cuantificador qr(α) de una fórmula FO α, que expresa la profundidad de anidamiento de cuantificadores . Por ejemplo, para una fórmula en forma normal prenex , qr es simplemente el número total de sus cuantificadores. Entonces FO[ m ] puede definirse como todas las fórmulas FO α con qr(α) ≤ m (o, si se desea una partición, como aquellas fórmulas FO con rango de cuantificador igual a m ).
4. Por lo tanto, todo se reduce a mostrar en los subconjuntos FO[ m ]. El enfoque principal aquí es utilizar la caracterización algebraica proporcionada por los juegos de Ehrenfeucht–Fraïssé . De manera informal, estos toman un solo isomorfismo parcial en A y B y lo extienden m veces, para probar o refutar , dependiendo de quién gane el juego. ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ ${\displaystyle A\equiv _{m}B}$

Ejemplo

Queremos demostrar que la propiedad de que el tamaño de una estructura ordenada A = (A, ≤) es par, no se puede expresar en FO.

1. La idea es elegir A ∈ PAR y B ∉ PAR , donde PAR es la clase de todas las estructuras de tamaño par.
2. Partimos de dos estructuras ordenadas A ₂ y B ₂ con universos A ₂ = {1, 2, 3, 4} y B ₂ = {1, 2, 3}. Obviamente A ₂ ∈ EVEN y B ₂ ∉ EVEN .
3. Para m = 2, ahora podemos demostrar* que en un juego Ehrenfeucht–Fraïssé de 2 movimientos en A ₂ y B ₂ el duplicador siempre gana, y por lo tanto A ₂ y B ₂ no pueden discriminarse en FO[2], es decir, para cada α ∈ FO[2] . ${\displaystyle \mathbf {A} _{2}\models \alpha \iff \mathbf {B} _{2}\models \alpha }$
4. A continuación, tenemos que aumentar la escala de las estructuras incrementando m . Por ejemplo, para m = 3, debemos encontrar un A ₃ y un B ₃ tales que el duplicador siempre gane el juego de 3 movimientos. Esto se puede lograr mediante A ₃ = {1, ..., 8} y B ₃ = {1, ..., 7}. De manera más general, podemos elegir A _m = {1, ..., 2 ^m } y B _m = {1, ..., 2 ^m −1}; para cualquier m, el duplicador siempre gana el juego de m movimientos para este par de estructuras*.
5. Por lo tanto, INCLUSO en estructuras ordenadas finitas no se puede expresar en FO.

(*) Nótese que se ha omitido la prueba del resultado del juego Ehrenfeucht–Fraïssé , ya que no es el foco principal aquí.

Leyes de cero-uno

Glebskiĭ et al. (1969) e, independientemente, Fagin (1976) demostraron una ley cero-uno para oraciones de primer orden en modelos finitos; la prueba de Fagin utilizó el teorema de compacidad . Según este resultado, cada oración de primer orden en una firma relacional es casi siempre verdadera o casi siempre falsa en estructuras finitas. Es decir, sea S una oración fija de primer orden y elija una estructura aleatoria con dominio , de manera uniforme entre todas las estructuras con dominio . Entonces, en el límite cuando n tiende a infinito, la probabilidad de que G _n modele S tenderá a cero o a uno: ${\displaystyle \sigma }$ ${\displaystyle \sigma }$ ${\displaystyle \sigma }$ ${\displaystyle G_{n}}$ ${\displaystyle \{1,\dots ,n\}}$ ${\displaystyle \sigma }$ ${\displaystyle \{1,\dots ,n\}}$

${\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}$

El problema de determinar si una oración dada tiene una probabilidad que tiende a cero o a uno es PSPACE-completo . ^[3]

Se ha realizado un análisis similar para lógicas más expresivas que la lógica de primer orden. Se ha demostrado que la ley 0-1 es válida para oraciones en FO(LFP) , lógica de primer orden aumentada con un operador de punto fijo mínimo, y de manera más general para oraciones en la lógica infinitaria , que permite conjunciones y disyunciones potencialmente arbitrarias. Otra variante importante es la ley 0-1 no etiquetada, donde en lugar de considerar la fracción de estructuras con dominio , se considera la fracción de clases de isomorfismo de estructuras con n elementos. Esta fracción está bien definida, ya que dos estructuras isomorfas cualesquiera satisfacen las mismas oraciones. La ley 0-1 no etiquetada también es válida para y, por lo tanto, en particular para FO(LFP) y la lógica de primer orden. ^[4] ${\displaystyle L_{\infty \omega }^{\omega }}$ ${\displaystyle \{1,\dots ,n\}}$ ${\displaystyle L_{\infty \omega }^{\omega }}$

Teoría de la complejidad descriptiva

Un objetivo importante de la teoría de modelos finitos es la caracterización de las clases de complejidad por el tipo de lógica necesaria para expresar los lenguajes que las componen. Por ejemplo, PH , la unión de todas las clases de complejidad en la jerarquía polinómica, es precisamente la clase de lenguajes expresables por enunciados de lógica de segundo orden . Esta conexión entre la complejidad y la lógica de las estructuras finitas permite transferir fácilmente los resultados de un área a otra, facilitando nuevos métodos de prueba y proporcionando evidencia adicional de que las principales clases de complejidad son de alguna manera "naturales" y no están ligadas a las máquinas abstractas específicas utilizadas para definirlas.

En concreto, cada sistema lógico produce un conjunto de consultas que se pueden expresar en él. Las consultas, cuando se limitan a estructuras finitas, corresponden a los problemas computacionales de la teoría de la complejidad tradicional.

Algunas clases de complejidad bien conocidas son capturadas por lenguajes lógicos de la siguiente manera:

• En presencia de un orden lineal, la lógica de primer orden con un operador de cierre transitivo y conmutativo agregado produce L , problemas resolubles en el espacio logarítmico.
• En presencia de un orden lineal, la lógica de primer orden con un operador de cierre transitivo produce NL , los problemas se pueden resolver en el espacio logarítmico no determinista.
• En presencia de un orden lineal, la lógica de primer orden con un operador de punto mínimo fijo da P , los problemas son solucionables en tiempo polinomial determinista.
• En todas las estructuras finitas (independientemente de si están ordenadas), la lógica existencial de segundo orden da NP ( teorema de Fagin ). ^[5]

Aplicaciones

Teoría de bases de datos

Un fragmento sustancial de SQL (a saber, lo que es efectivamente álgebra relacional ) se basa en lógica de primer orden (que se puede traducir más precisamente en cálculo relacional de dominio mediante el teorema de Codd ), como ilustra el siguiente ejemplo: Piense en una tabla de base de datos "GIRLS" con las columnas "FIRST_NAME" y "LAST_NAME". Esto corresponde a una relación binaria, digamos G(f, l) en FIRST_NAME × LAST_NAME. La consulta FO , que devuelve todos los apellidos donde el nombre es 'Judy', se vería en SQL así: ${\displaystyle {l:G({\text{'Judy'}},l)}}$

Seleccione APELLIDO de CHICAS donde NOMBRE = 'Judy'      

Tenga en cuenta que aquí asumimos que todos los apellidos aparecen solo una vez (o deberíamos usar SELECT DISTINCT ya que asumimos que las relaciones y las respuestas son conjuntos, no bolsas).

A continuación, queremos realizar una declaración más compleja. Por lo tanto, además de la tabla "GIRLS", tenemos una tabla "BOYS" también con las columnas "FIRST_NAME" y "LAST_NAME". Ahora queremos consultar los apellidos de todas las niñas que tengan el mismo apellido que al menos uno de los niños. La consulta FO es y la declaración SQL correspondiente es: ${\displaystyle {(f,l):\exists h(G(f,l)\land B(h,l))}}$

seleccione NOMBRE , APELLIDO de NIÑAS donde APELLIDO EN ( seleccione APELLIDO de NIÑOS );            

Observe que para expresar "∧" introdujimos el nuevo elemento de lenguaje "IN" con una declaración de selección posterior. Esto hace que el lenguaje sea más expresivo a cambio de una mayor dificultad para aprender e implementar. Esta es una compensación común en el diseño de lenguajes formales. La forma que se muestra arriba ("IN") no es ni mucho menos la única para extender el lenguaje. Una forma alternativa es, por ejemplo, introducir un operador "JOIN", es decir:

seleccionar distinto g.NOMBRE , g.APELLIDO de NIÑAS g , NIÑOS b donde g.APELLIDO = b.APELLIDO ;​​​​​​​​         

La lógica de primer orden es demasiado restrictiva para algunas aplicaciones de bases de datos, por ejemplo, debido a su incapacidad para expresar clausura transitiva . Esto ha llevado a que se agreguen construcciones más poderosas a los lenguajes de consulta de bases de datos, como el recursivo WITH en SQL:1999 . Por lo tanto, se han estudiado lógicas más expresivas, como las lógicas de punto fijo , en la teoría de modelos finitos debido a su relevancia para la teoría y las aplicaciones de bases de datos.

Consulta y búsqueda

Los datos narrativos no contienen relaciones definidas. Por lo tanto, la estructura lógica de las consultas de búsqueda de texto se puede expresar en lógica proposicional , como en:

("Java" Y NO "isla") O ("C#" Y NO "música")

Tenga en cuenta que los desafíos en la búsqueda de texto completo son diferentes a los de la consulta de bases de datos, como la clasificación de los resultados.

Historia

• Trakhtenbrot 1950 : el fracaso del teorema de completitud en la lógica de primer orden
• Scholz 1952: caracterización de espectros en lógica de primer orden
• Fagin 1974 : el conjunto de todas las propiedades expresables en la lógica existencial de segundo orden es precisamente la clase de complejidad NP
• Chandra, Harel 1979/80: extensión de lógica de primer orden de punto fijo para lenguajes de consulta de bases de datos capaces de expresar cierre transitivo -> consultas como objetos centrales de FMT
• Immerman , Vardi 1982: la lógica de punto fijo sobre estructuras ordenadas captura PTIME -> complejidad descriptiva ( teorema de Immerman–Szelepcsényi )
• Ebbinghaus , Flum 1995: primer libro completo "Teoría de modelos finitos"
• Abiteboul , Hull, Vianu 1995: libro "Fundamentos de las bases de datos"
• Immerman 1999: libro “ Complejidad descriptiva ”
• Kuper, Libkin, Paredaens 2000: libro "Bases de datos con restricciones"
• Darmstadt 2005/ Aachen 2006: primeros talleres internacionales sobre "Teoría de modelos algorítmicos"

Citas

1. Fagin, Ronald (1993). «Teoría de modelos finitos: una perspectiva personal» (PDF) . Theoretical Computer Science . 116 : 3–31. doi : 10.1016/0304-3975(93)90218-I . Archivado desde el original el 23 de junio de 2021. Consultado el 20 de julio de 2023 .{{cite journal}}: CS1 maint: bot: original URL status unknown (link)
2. Immerman, Neil (1999). Complejidad descriptiva . Nueva York: Springer-Verlag. pág. 6. ISBN. 0-387-98600-6.
3. Grandjean, Etienne (1983). "Complejidad de la teoría de primer orden de casi todas las estructuras finitas". Información y Control . 57 (2–3): 180–204. doi : 10.1016/S0019-9958(83)80043-6 .
4. Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995). "4". Teoría de modelos finitos. Perspectivas en lógica matemática. doi :10.1007/978-3-662-03182-7. ISBN 978-3-662-03184-1.
5. Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995). "7". Teoría de modelos finitos. Perspectivas en lógica matemática. doi :10.1007/978-3-662-03182-7.

Referencias

• Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995). Teoría de modelos finitos . Saltador . ISBN 978-3-540-60149-4.

• Fagin, Ronald (1976). "Probabilidades en modelos finitos". Revista de lógica simbólica . 41 (1): 50–58. doi :10.2307/2272945. JSTOR  2272945.
• Glebskiĭ, Yu V.; Kogan, DI; Liogon'kiĭ, MI; Talanov, VA (1969). "Объем и доля выполнимости формул узкого исчисления предикатов" [Volumen y fracción de satisfacibilidad de fórmulas del cálculo de predicados de primer orden]. Kibernética . 5 (2): 17–27.También disponible como; "Rango y grado de realizabilidad de fórmulas en el cálculo de predicados restringido". Cibernética . 5 (2): 142–154. 1972. doi :10.1007/BF01071084.
• Libkin, Leonid (2004). Elementos de la teoría de modelos finitos . Springer . ISBN . 3-540-21202-7.

• Abiteboul, Serge ; Hull, Richard; Vianu, Victor (1995). Fundamentos de bases de datos . Addison-Wesley . ISBN 0-201-53771-0.

• Immerman, Neil (1999). Complejidad descriptiva . Nueva York: Springer . ISBN . 0-387-98600-6.

Lectura adicional

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos en informática teórica. Una serie EATCS. ​​Berlín: Springer-Verlag . ISBN. 978-3-540-00428-8.Zbl 1133.03001  .

Enlaces externos

• Libkin, Leonid (2009). "La caja de herramientas de la teoría de modelos finitos de un teórico de bases de datos". PODS 2009: Actas del vigésimo octavo simposio ACM SIGACT–SIGMOD sobre Principios de sistemas de bases de datos . págs. 65–76. doi :10.1145/1559795.1559807. También es adecuado como introducción y visión general.
• Leonid Libkin. Capítulo introductorio de "Elementos de la teoría de modelos finitos" Archivado el 24 de septiembre de 2015 en Wayback Machine . Motiva tres áreas de aplicación principales: bases de datos, complejidad y lenguajes formales.
• Jouko Väänänen. Un curso breve sobre teoría de modelos finitos. Departamento de Matemáticas, Universidad de Helsinki. Basado en clases de 1993-1994.
• Anuj Dawar. Teoría de modelos finitos e infinitos, diapositivas, Universidad de Cambridge, 2002.
• "Teoría de modelos algorítmicos". RWTH Aachen. Archivado desde el original el 17 de julio de 2012. Consultado el 7 de noviembre de 2013 .Incluye una lista de problemas FMT abiertos.