Teoría de modelos finitos

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

• Dado que muchos teoremas centrales de MT no se cumplen cuando se restringen a estructuras finitas, FMT es bastante diferente de MT en sus métodos de demostración. Los resultados centrales de la teoría de modelos clásicos que fallan para estructuras finitas bajo FMT 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).
• Como la MT está estrechamente relacionada con el álgebra matemática , la FMT se convirtió en un instrumento "inusualmente eficaz" ^[1] en informática. En otras palabras: "En la historia de la lógica matemática, la mayor parte del interés se ha concentrado en estructuras infinitas ... Sin embargo, los objetos que las computadoras tienen y sostienen son siempre finitos. Para estudiar computación necesitamos una teoría de estructuras finitas". ^[2] Así, las principales áreas de aplicación de FMT son: teoría de la complejidad descriptiva , teoría de bases de datos y teoría del lenguaje formal .
• FMT se trata principalmente de discriminación de estructuras. La pregunta motivadora habitual es si una clase determinada de estructuras se puede describir (hasta el isomorfismo ) en un idioma determinado. Por ejemplo, ¿se pueden discriminar todos los gráficos cíclicos (de los no cíclicos) mediante una oración de la lógica de gráficos de primer orden ? Esto también puede expresarse como: ¿es la propiedad "cíclica" FO expresable?

Desafíos básicos

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

Caracterización de una sola estructura

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

Gráficos simples (1) y (1 ') que tienen propiedades comunes.

Problema

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

1. Cada nodo tiene un borde a otro nodo: ${\displaystyle \forall _{x}\exists _{y}G(x,y).}$
2. Ningún nodo tiene una ventaja para 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 son válidas, sin embargo, 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 son válidas (todas juntas) para ninguna otra estructura (hasta el isomorfismo).

Acercamiento

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

1. decir que hay al menos elementos:${\displaystyle n}$${\displaystyle \varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})}$
2. decir que hay como máximo elementos:${\displaystyle n}$${\displaystyle \varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)}$
3. declare cada elemento de la relación :${\displaystyle R}$${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$
4. enuncie 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})}$

Ampliación a un número fijo de estructuras

El método de describir una sola estructura por medio de una oración de primer orden puede extenderse fácilmente a cualquier número fijo de estructuras. Se puede obtener una descripción única mediante la disyunción de las descripciones de cada estructura. Por ejemplo, para dos estructuras y con la definición de frases 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 trata FMT. Tenga en cuenta que las estructuras infinitas nunca se pueden discriminar 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 , de que existe un modelo aritmético no estándar contable.

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

Todas las descripciones dadas hasta ahora especifican el número de elementos del universo. Desafortunadamente, los conjuntos de estructuras más interesantes no están restringidos a un cierto tamaño, como todos los gráficos que son árboles, están conectados o son acíclicos. Por tanto, discriminar un número finito de estructuras es de especial importancia.

Acercamiento

En lugar de una declaración general, lo siguiente es un bosquejo de una metodología para diferenciar entre estructuras que pueden y no pueden ser discriminadas.

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

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

donde es la abreviatura de para todos los FO-frases alpha, y P representa la clase de las estructuras con la propiedad P .${\displaystyle A\equiv B}$${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$

2. La metodología considera innumerables subconjuntos del lenguaje, cuya unión forma el lenguaje mismo. Por ejemplo, para FO considere las clases FO [ m ] para cada m . Para cada m se debe mostrar la idea central anterior. Eso es:

${\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 idioma.${\displaystyle A,B}$${\displaystyle m}$

3. Una forma común de definir FO [ m ] es mediante el rango de cuantificador qr (α) de una fórmula de FO α, que expresa la profundidad de anidamiento del cuantificador . Por ejemplo, para una fórmula en forma normal prenex , qr es simplemente el número total de sus cuantificadores. Entonces FO [ m ] se puede definir como todas las fórmulas de FO α con qr (α) ≤ m (o, si se desea una partición, como aquellas fórmulas de FO con rango de cuantificador igual am ).

4. Por lo tanto, todo se reduce a mostrar 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 mostrar 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 ∈ EVEN y B ∉ EVEN, donde EVEN es la clase de todas las estructuras de tamaño uniforme.

2. Comenzamos con dos estructuras ordenadas A ₂ y B ₂ con universos A ₂ = {1, 2, 3, 4} y B ₂ = {1, 2, 3}. Obviamente A ₂ ∈ PAR y B ₂ ∉ PAR.

3. Para m = 2, ahora podemos mostrar * que en una partida 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 A ₂ α ⇔ B ₂ α para cada α ∈ FO [2].${\displaystyle \models }$ ${\displaystyle \models }$

4. A continuación, tenemos que escalar las estructuras aumentando m . Por ejemplo, para m = 3 debemos encontrar un A ₃ y un B _{3 de} manera 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 m -move para este par de estructuras *.

5. Por 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 aquí no es el foco principal.

Aplicaciones

Teoría de la base de datos

Un fragmento sustancial de SQL (es decir, el que es efectivamente álgebra relacional ) se basa en la lógica de primer orden (más precisamente se puede traducir al cálculo relacional de dominio mediante el teorema de Codd ), como lo 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 X LAST_NAME. La consulta FO {l: G ('Judy', l)} , que devuelve todos los apellidos donde el nombre es 'Judy', se vería en SQL así:

seleccione LAST_NAME de NIÑASdonde FIRST_NAME = 'Judy'

Observe, asumimos aquí, 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 hacer una declaración más compleja. Por lo tanto, además de la tabla "NIÑAS", tenemos una tabla "NIÑOS" también con las columnas "NOMBRE_ PRIMER" y "NOMBRE_LTIMO". Ahora queremos consultar los apellidos de todas las chicas que tienen el mismo apellido que al menos uno de los chicos. La consulta FO es {(f, l): ∃h (G (f, l) ∧ B (h, l))} , y la declaración SQL correspondiente es:

seleccione FIRST_NAME, LAST_NAME de NIÑASdonde LAST_NAME IN (seleccione LAST_NAME de BOYS);

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

seleccione distinto g.FIRST_NAME, g.LAST_NAME de NIÑAS g, NIÑOS bdonde g.LAST_NAME = b.LAST_NAME;

La lógica de primer orden es demasiado restrictiva para algunas aplicaciones de bases de datos, por ejemplo, debido a su incapacidad para expresar un cierre transitivo . 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, las lógicas más expresivas, como las lógicas de puntos fijos , se han estudiado en la teoría de modelos finitos debido a su relevancia para la teoría y las aplicaciones de las 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 de las consultas en bases de datos, como la clasificación de resultados.

Historia

• Trakhtenbrot 1950 : falla del teorema de completitud en 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 lógica de primer orden de punto fijo para lenguajes de consulta de bases de datos capaz 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 bases de datos"
• Immerman 1999: libro " Complejidad descriptiva "
• Kuper, Libkin, Paredaens 2000: libro "Bases de datos de 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) . Informática Teórica . 116 : 3-31. doi : 10.1016 / 0304-3975 (93) 90218-I .
2. Immerman, Neil (1999). Complejidad descriptiva . Nueva York: Springer-Verlag. pag. 6 . ISBN 0-387-98600-6.

Referencias

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

• 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

Wikilibros tiene un libro sobre el tema: Teoría de modelos finitos

• 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 los principios de los sistemas de bases de datos . págs. 65–76. doi : 10.1145 / 1559795.1559807 . También es adecuado como introducción general y descripción general.
• Leonid Libkin. Capítulo introductorio de "Elementos de la teoría de modelos finitos" . Motiva tres áreas principales de aplicación: bases de datos, complejidad y lenguajes formales.
• Jouko Väänänen. Un curso corto sobre teoría de modelos finitos . Departamento de Matemáticas, Universidad de Helsinki. Basado en conferencias de 1993-1994.
• Anuj Dawar. Teoría de modelos infinitos y finitos , diapositivas, Universidad de Cambridge, 2002.
• "Teoría de modelos algorítmicos" . RWTH Aquisgrán. Archivado desde el original el 17 de julio de 2012 . Consultado el 7 de noviembre de 2013 . Incluye una lista de problemas abiertos de FMT.