Teoria do modelo finito - Finite model theory

A teoria do modelo finito ( FMT ) é uma subárea da teoria do modelo (TM). MT é o ramo da lógica que trata da relação entre uma linguagem formal (sintaxe) e suas interpretações (semântica). FMT é uma restrição de MT para interpretações em estruturas finitas , que possuem um universo finito.

• Uma vez que muitos teoremas centrais de MT não são válidos quando restritos a estruturas finitas, FMT é bastante diferente de MT em seus métodos de prova. Os resultados centrais da teoria do modelo clássico que falham para estruturas finitas sob FMT incluem o teorema de compactação , o teorema de completude de Gödel e o método de ultraprodutos para lógica de primeira ordem (FO).
• Como a MT está intimamente relacionada à álgebra matemática , o FMT se tornou um instrumento "excepcionalmente eficaz" na ciência da computação. Em outras palavras: "Na história da lógica matemática, a maior parte do interesse se concentrou em estruturas infinitas ... No entanto, os objetos que os computadores têm e mantêm são sempre finitos. Para estudar computação, precisamos de uma teoria das estruturas finitas." Assim, as principais áreas de aplicação do FMT são: teoria descritiva da complexidade , teoria do banco de dados e teoria da linguagem formal .
• O FMT trata principalmente da discriminação de estruturas. A questão motivadora usual é se uma determinada classe de estruturas pode ser descrita (até o isomorfismo ) em uma determinada linguagem. Por exemplo, todos os gráficos cíclicos podem ser discriminados (dos não cíclicos) por uma sentença da lógica de primeira ordem dos gráficos ? Isso também pode ser expresso como: a propriedade FO "cíclica" pode ser expressa?

Desafios básicos

Uma única estrutura finita pode sempre ser axiomatizada na lógica de primeira ordem, onde axiomatizada em uma linguagem L significa descrita exclusivamente até o isomorfismo por uma única frase L. Da mesma forma, qualquer coleção finita de estruturas finitas pode sempre ser axiomatizada na lógica de primeira ordem. Algumas, mas não todas, coleções infinitas de estruturas finitas também podem ser axiomatizadas por uma única frase de primeira ordem.

Caracterização de uma única estrutura

Uma linguagem L é expressiva o suficiente para axiomatizar uma única estrutura finita S ?

Problema

Uma estrutura como (1) na figura pode ser descrita por sentenças FO na lógica de gráficos como

1. Cada nó tem uma borda para outro nó: ${\ displaystyle \ forall _ {x} \ exists _ {y} G (x, y).}$
2. Nenhum nó tem uma vantagem para si: ${\ displaystyle \ forall _ {x, y} (G (x, y) \ Rightarrow x \ neq y).}$
3. Há pelo menos um nó conectado a todos os outros: ${\ displaystyle \ exists _ {x} \ forall _ {y} (x \ neq y \ Rightarrow G (x, y)).}$

No entanto, essas propriedades não axiomatizam a estrutura, uma vez que para a estrutura (1 ') as propriedades acima também são válidas, embora as estruturas (1) e (1') não sejam isomórficas.

Informalmente, a questão é se, ao adicionar propriedades suficientes, essas propriedades juntas descrevem exatamente (1) e são válidas (todas juntas) para nenhuma outra estrutura (até isomorfismo).

Abordagem

Para uma única estrutura finita, é sempre possível descrever com precisão a estrutura por uma única sentença FO. O princípio é ilustrado aqui para uma estrutura com uma relação binária e sem constantes: ${\ displaystyle R}$

1. diga que há pelo menos elementos:${\ displaystyle n}$${\ displaystyle \ varphi _ {1} = \ bigwedge _ {i \ neq j} \ neg (x_ {i} = x_ {j})}$
2. diga que há no máximo elementos:${\ displaystyle n}$${\ displaystyle \ varphi _ {2} = \ forall _ {y} \ bigvee _ {i} (x_ {i} = y)}$
3. indique cada elemento da relação :${\ displaystyle R}$${\ displaystyle \ varphi _ {3} = \ bigwedge _ {(a_ {i}, a_ {j}) \ in R} R (x_ {i}, x_ {j})}$
4. indique todos os não-elementos da relação :${\ displaystyle R}$${\ displaystyle \ varphi _ {4} = \ bigwedge _ {(a_ {i}, a_ {j}) \ notin R} \ neg R (x_ {i}, x_ {j})}$

tudo para a mesma tupla , produzindo a sentença 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})}$

Extensão para um número fixo de estruturas

O método de descrever uma única estrutura por meio de uma frase de primeira ordem pode ser facilmente estendido para qualquer número fixo de estruturas. Uma descrição única pode ser obtida pela disjunção das descrições para cada estrutura. Por exemplo, para duas estruturas e com sentenças de definição e isso seria ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle \ varphi _ {A}}$${\ displaystyle \ varphi _ {B}}$

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

Extensão para uma estrutura infinita

Por definição, um conjunto contendo uma estrutura infinita fica fora da área de que trata o FMT. Observe que estruturas infinitas nunca podem ser discriminadas em FO, por causa do teorema de Löwenheim – Skolem , que implica que nenhuma teoria de primeira ordem com um modelo infinito pode ter um modelo único até isomorfismo.

O exemplo mais famoso é provavelmente o teorema de Skolem , de que existe um modelo não padrão contável de aritmética.

Caracterização de uma classe de estruturas

Uma linguagem L é expressiva o suficiente para descrever exatamente (até o isomorfismo) aquelas estruturas finitas que possuem certa propriedade P ?

Problema

Todas as descrições fornecidas até agora especificam o número de elementos do universo. Infelizmente, a maioria dos conjuntos interessantes de estruturas não se restringe a um determinado tamanho, como todos os gráficos que são árvores, são conectados ou acíclicos. Assim, discriminar um número finito de estruturas é de especial importância.

Abordagem

Em vez de uma declaração geral, o que se segue é um esboço de uma metodologia para diferenciar as estruturas que podem e não podem ser discriminadas.

1. A ideia central é que sempre que se quer ver se uma propriedade P pode ser expressa em FO, escolhe-se as estruturas A e B , onde A tem P e B não. Se para A e B as mesmas sentenças FO forem válidas, então P não pode ser expresso em FO. Resumidamente:

${\ displaystyle A \ in P, B \ não \ in P}$ e ${\ displaystyle A \ equiv B,}$

onde é uma abreviação para para todas as frases FO-ct, e P representa a classe de estruturas com propriedade P . ${\ displaystyle A \ equiv B}$${\ displaystyle A \ models \ alpha \ Leftrightarrow B \ models \ alpha}$

2. A metodologia considera contáveis ​​muitos subconjuntos da linguagem, a união dos quais forma a própria linguagem. Por exemplo, para FO considere as classes FO [ m ] para cada m . Para cada m, a ideia central acima deve ser mostrada. Isso é:

${\ displaystyle A \ in P, B \ não \ in P}$ e ${\ displaystyle A \ equiv _ {m} B}$

com um par para cada um e α (em ≡) de FO [ m ]. Pode ser apropriado escolher as classes FO [ m ] para formar uma partição do idioma. ${\ displaystyle A, B}$${\ displaystyle m}$

3. Uma maneira comum de definir FO [ m ] é por meio do quantificador rank qr (α) de uma fórmula FO α, que expressa a profundidade do aninhamento do quantificador . Por exemplo, para uma fórmula na forma normal prenex , qr é simplesmente o número total de seus quantificadores. Então FO [ m ] pode ser definido como todas as fórmulas FO α com qr (α) ≤ m (ou, se uma partição for desejada, como aquelas fórmulas FO com classificação de quantificador igual am ).

4. Assim, tudo se resume a mostrar nos subconjuntos FO [ m ]. A abordagem principal aqui é usar a caracterização algébrica fornecida pelos jogos Ehrenfeucht – Fraïssé . Informalmente, eles pegam um único isomorfismo parcial em A e B e o estendem m vezes, a fim de provar ou refutar , dependendo de quem ganha o jogo. ${\ displaystyle A \ models \ alpha \ Leftrightarrow B \ models \ alpha}$${\ displaystyle A \ equiv _ {m} B}$

Exemplo

Queremos mostrar que a propriedade de que o tamanho de uma estrutura ordenada A = (A, ≤) é par, não pode ser expressa em FO.

1. A ideia é escolher A ∈ EVEN e B ∉ EVEN, onde EVEN é a classe de todas as estruturas de tamanho par.

2. Começamos com duas estruturas ordenadas A ₂ e B ₂ com universos A ₂ = {1, 2, 3, 4} e B ₂ = {1, 2, 3}. Obviamente, A ₂ ∈ MESMO e B ₂ ∉ MESMO.

3. Para m = 2, podemos agora mostrar * que em um jogo Ehrenfeucht – Fraïssé de 2 movimentos em A ₂ e B ₂ o duplicador sempre vence e, portanto, A ₂ e B ₂ não podem ser discriminados em FO [2], ou seja, A ₂ α ⇔ B ₂ α para todo α ∈ FO [2]. ${\ displaystyle \ models}$ ${\ displaystyle \ models}$

4. Em seguida, temos que dimensionar as estruturas aumentando m . Por exemplo, para m = 3, devemos encontrar A ₃ e B _{3 de} forma que o duplicador sempre ganhe o jogo de 3 movimentos. Isso pode ser alcançado por A ₃ = {1, ..., 8} e ​​B ₃ = {1, ..., 7}. De forma mais geral, podemos escolher A _m = {1, ..., 2 ^m } e B _m = {1, ..., 2 ^m -1}; para qualquer m, o duplicador sempre ganha o jogo de m- movimento para este par de estruturas *.

5. Assim, MESMO em estruturas ordenadas finitas não pode ser expresso em FO.

(*) Note que a prova do resultado do jogo Ehrenfeucht – Fraïssé foi omitida, pois não é o foco principal aqui.

Formulários

Teoria do banco de dados

Um fragmento substancial de SQL (ou seja, aquele que é efetivamente álgebra relacional ) é baseado na lógica de primeira ordem (mais precisamente pode ser traduzido em cálculo relacional de domínio por meio do teorema de Codd ), como o exemplo a seguir ilustra: Pense em uma tabela de banco de dados " GIRLS "com as colunas" FIRST_NAME "e" LAST_NAME ". Isso corresponde a uma relação binária, digamos G (f, l) em FIRST_NAME X LAST_NAME. A consulta FO {l: G ('Judy', l)} , que retorna todos os sobrenomes onde o primeiro nome é 'Judy', ficaria em SQL assim:

select LAST_NAME 
from GIRLS
where FIRST_NAME = 'Judy'

Observe, presumimos aqui, que todos os sobrenomes aparecem apenas uma vez (ou devemos usar SELECT DISTINCT, pois pressupomos que as relações e as respostas são conjuntos, não bolsas).

Em seguida, queremos fazer uma declaração mais complexa. Portanto, além da tabela "GIRLS" temos uma tabela "BOYS" também com as colunas "FIRST_NAME" e "LAST_NAME". Agora queremos consultar os sobrenomes de todas as meninas que têm o mesmo sobrenome de pelo menos um dos meninos. A consulta FO é {(f, l): ∃h (G (f, l) ∧ B (h, l))} , e a instrução SQL correspondente é:

select FIRST_NAME, LAST_NAME 
from GIRLS
where LAST_NAME IN ( select LAST_NAME from BOYS );

Observe que, para expressar o "∧", introduzimos o novo elemento de linguagem "IN" com uma instrução select subsequente. Isso torna a linguagem mais expressiva pelo preço de maior dificuldade de aprender e implementar. Este é um compromisso comum no design de linguagem formal. A maneira mostrada acima ("IN") não é, de longe, a única a estender a linguagem. Uma forma alternativa é, por exemplo, introduzir um operador "JOIN", que é:

select distinct g.FIRST_NAME, g.LAST_NAME 
from GIRLS g, BOYS b
where g.LAST_NAME=b.LAST_NAME;

A lógica de primeira ordem é muito restritiva para alguns aplicativos de banco de dados, por exemplo, devido à sua incapacidade de expressar fechamento transitivo . Isso levou a construções mais poderosas sendo adicionadas a linguagens de consulta de banco de dados, como o WITH recursivo em SQL: 1999 . Lógicas mais expressivas, como a lógica de pontos fixos , foram, portanto, estudadas na teoria de modelos finitos por causa de sua relevância para a teoria e aplicações de banco de dados.

Consultando e pesquisando

Os dados narrativos não contêm relações definidas. Assim, a estrutura lógica das consultas de pesquisa de texto pode ser expressa em lógica proposicional , como em:

("Java" AND NOT "island") OR ("C#" AND NOT "music")

Observe que os desafios na pesquisa de texto completo são diferentes da consulta de banco de dados, como classificação de resultados.

História

• Trakhtenbrot 1950 : falha do teorema da completude na lógica de primeira ordem
• Scholz 1952: caracterização de espectros em lógica de primeira ordem
• Fagin 1974 : o conjunto de todas as propriedades expressáveis ​​na lógica existencial de segunda ordem é precisamente a classe de complexidade NP
• Chandra, Harel 1979/80: extensão lógica de primeira ordem de ponto fixo para linguagens de consulta de banco de dados capazes de expressar fechamento transitivo -> consultas como objetos centrais de FMT
• Immerman , Vardi 1982: a lógica de ponto fixo sobre estruturas ordenadas captura PTIME -> complexidade descritiva ( teorema de Immerman-Szelepcsényi )
• Ebbinghaus , Flum 1995: primeiro livro abrangente "Teoria do Modelo Finito"
• Abiteboul , Hull, Vianu 1995: livro "Foundations of Databases"
• Immerman 1999: livro " Descriptive Complexity "
• Kuper, Libkin, Paredaens 2000: livro "Constraint Databases"
• Darmstadt 2005 / Aachen 2006: primeiros workshops internacionais sobre "Teoria do Modelo Algorítmico"

Citações

Referências

• Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995). Teoria dos Modelos Finitos . Springer . ISBN 978-3-540-60149-4.

• Libkin, Leonid (2004). Elementos da Teoria dos Modelos Finitos . Springer . ISBN 3-540-21202-7.

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

• Immerman, Neil (1999). Complexidade descritiva . Nova York: Springer . ISBN 0-387-98600-6.

Leitura adicional

• Grädel, Erich; Kolaitis, Phokion G .; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007). Teoria dos modelos finitos e suas aplicações . Textos em Ciência da Computação Teórica. Uma série EATCS. Berlim: Springer-Verlag . ISBN 978-3-540-00428-8. Zbl  1133.03001 .

links externos

• Libkin, Leonid (2009). "A caixa de ferramentas da teoria do modelo finito de um teórico de banco de dados". PODS 2009: Anais do vigésimo oitavo simpósio ACM SIGACT – SIGMOD sobre Princípios de sistemas de banco de dados . pp. 65–76. doi : 10.1145 / 1559795.1559807 . Também adequado como introdução geral e visão geral.
• Leonid Libkin. Capítulo introdutório de "Elementos da teoria dos modelos finitos" . Motiva três áreas de aplicação principais: bancos de dados, complexidade e linguagens formais.
• Jouko Väänänen. Um Curso Curto em Teoria dos Modelos Finitos . Departamento de Matemática da Universidade de Helsinque. Baseado em palestras de 1993-1994.
• Anuj Dawar. Teoria dos modelos infinitos e finitos , slides, Universidade de Cambridge, 2002.
• "Teoria do Modelo Algorítmico" . RWTH Aachen. Arquivado do original em 17 de julho de 2012 . Retirado em 7 de novembro de 2013 . Inclui uma lista de problemas FMT abertos.