Teoria de modelos finitos – Wikipédia, a enciclopédia livre

Esta página cita fontes, mas que não cobrem todo o conteúdo. Ajude a inserir referências. Conteúdo não verificável pode ser removido.—Encontre fontes: ABW  • CAPES  • Google (N • L • A) (Junho de 2015)

Teoria dos modelos finitos (TMF) é uma subárea da Teoria dos modelos (TM). A TM é um ramo da Lógica matemática que lida com a relação entre a linguagem formal (sintaxe) e suas interpretações (semântica). A TMF é uma restrição da TM para a interpretação de estruturas que tem um universo finito.

• Como muitos teoremas centrais da TM são inconsistentes quando restritos a estruturas finitas, a TMF é bem diferente da TM em seus métodos de prova. Os resultados desses teoremas centras da Teoria dos Modelos clássica que falham para estruturas finitas incluem o Teorema da compacidade, Teorema da completude de Gödel, e o método do ultraproduto para a Lógica de primeira ordem (LPO).
• Como a TM está muito relacionada à álgebra, a TMF se tornou um "efetivo mas não usual"^[1] instrumento na Ciência da computação. Em outras palavras: "Na história da Lógica matemática, sempre houve mais interesse nas estruturas infinitas... No entanto, os objetos que os computadores tratam são sempre finitos. Para estudar computação, nós precisamos de uma teoria de estruturas finitas."^[2] Assim, as principais áreas de aplicação da TMF são: Teoria da complexidade descritiva, Teoria do banco de dados (Banco de dados relacional) e teoria da linguagem formal.
• A TMF trata da separação de estruturas. A pergunta de motivação usual é se uma dada classe de estruturas pode ser descrita em uma linguagem dada. Por exemplo, todos os grafos cíclicos podem ser separados (dos não cíclicos) através de uma sentença da LPO? Isso também pode ser escrito como: A propriedade "cíclico" de um grafo é expressável na LPO?

Desafios Básicos[editar | editar código-fonte]

Uma única estrutura sempre pode ser descrita de forma única na LPO. Alguns conjuntos finitos de estruturas também pode ser descritos em LPO. Contudo, essa lógica não é suficiente para descrever qualquer conjunto que contém estruturas infinitas.

Caracterização de uma Estrutura Simples[editar | editar código-fonte]

Uma linguagem (assinatura) L é expressiva o suficiente para descrever uma estrutura finita S de uma única forma (ignorando isomorfismo)?

Problema[editar | editar código-fonte]

Uma estrutura como (1) na figura pode ser descrita na lógica de primeira ordem assim:

1. Todo vértice tem uma aresta para outro vértice: ${\displaystyle \forall _{x}\exists _{y}G(x,y).}$
2. Nenhum vértice tem uma aresta para ele mesmo: ${\displaystyle \forall _{x,y}(G(x,y)\Rightarrow x\neq y).}$
3. Existe pelo menos um vértice que está conectado a todos os outros: ${\displaystyle \exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).}$

No entanto, essas propriedades não descrevem a estrutura unicamente (ignorando isomorfismo), uma vez que para a estrutura (1'), as propriedades acima também são satisfeitas, mas as estruturas (1) e (1') não são isomorfas.

Informalmente, a questão é se, adicionando algumas propriedades, essas propriedades descrevem exatamente (1) e não são válidas para nenhuma outra estrutura (exceto as isomorfas).

Abordagem[editar | editar código-fonte]

É sempre possível descrever uma estrutura finita precisamente por uma sentença da LPO. Esse princípio é ilustrado aqui para uma estrutura com uma relação binária ${\displaystyle R(-,-)}$ e sem constantes:

1. Digamos que existem pelo menos ${\displaystyle n}$ elementos: ${\displaystyle \varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})}$
2. Digamos que existem no máximo ${\displaystyle n}$ elementos: ${\displaystyle \varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)}$
3. Verificar todos os elementos que pertencem a ${\displaystyle R}$: ${\displaystyle \varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})}$
4. Verificar todos os elementos que não pertencem a ${\displaystyle R}$: ${\displaystyle \varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})}$

todos para a mesma tupla ${\displaystyle x_{1}..x_{n}}$, produzindo a sentença ${\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[editar | editar código-fonte]

O método de descrever uma única estrutura através de uma sentença de lógica de primeira ordem pode ser facilmente estendido para um número fixo de estruturas. Uma única descrição pode ser obtida das disjunções das descrições de cada estrutura. Por exemplo, para duas estruturas, seria:

${\displaystyle \exists _{x_{1}}...\exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})\lor \exists _{x_{1}}...\exists _{x_{n}}(\varrho _{1}\land \varrho _{2}\land \varrho _{3}\land \varrho _{4}).}$

Extensão para uma estrutura infinita[editar | editar código-fonte]

Por definição, um conjunto contendo uma estrutura infinita sai da área de atuação da TMF. Note que estruturas infinitas nunca podem ser separadas das outras em lógica de primeira ordem por causa do Teorema da compacidade da Teoria dos Modelos clássica: Para todo modelo infinito, um modelo não-isomórfos pode ser descoberto, o qual tem exatamente as mesmas propriedades da descrição do anterior.

O exemplo mais famoso é o Teorema de Löwenheim–Skolem , que tem um modelo contável e não-padrão da aritmética.

Caracterização de uma Classe de Estruturas[editar | editar código-fonte]

Uma linguagem (assinatura) L é expressiva o suficiente para descrever exatamente as estruturas finitas que tem possuem uma propriedade P em comum (ignorando isomorfismo)?

Problema[editar | editar código-fonte]

As descrições dadas até agora especificam o número de elementos do universo. Infelizmente a maioria dos conjuntos de estruturas não são restritos a um certo tamanho, como todos os grafos que são árvores, sejam eles conexos ou acíclicos. Contudo, para separar um número finito de estruturas, essa restrição é de grande importância.

Abordagem[editar | editar código-fonte]

Em vez de um método geral, a seguir está um esboço de uma metodologia para diferenciar as estruturas que podem e que não podem ser separadas.

1. A ideia central é que sempre que se quer ver se uma propriedade P pode ser expressa na lógica de primeira ordem, escolhem-se estruturas A e B, onde A tem P e B não. Se as sentenças são válidas para A e também para B, então P não pode ser expresso em lógica de primeira ordem (caso contrário, pode). Resumindo:

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

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

2. A metodologia considera contáveis muitos subconjuntos da linguagem, linguagens estas cuja união forma a própria linguagem. Por exemplo, para a lógica de primeira ordem, considere as classes [m] para cada m. Para cada m, a ideia central acima tem que ser mostrada. Isto é:

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

com um par ${\displaystyle A,B}$ para cada ${\displaystyle m}$ e α; (in ≡) de [m]. Isso pode ser apropriado para escolher as classes [m] que formam uma partição da linguagem.

3. Um jeito comum de definir [m] é pelo número de quantificadores qr(α) de uma fórmula ALFA. Por exemplo, para uma formula na Forma normal prenex, qr é simplesmente o total de quantificadores (se atentando ao fato de que uma fórmula pode ter um número diferente de quantificadores antes e depois de estar na forma Prenex). Visto isso, [m] pode ser definido com todas as fórmulas α da LPO com qr(α) ≤ m (ou, se é desejada uma partição, todas as fórmulas da LPO com qr(α) = m).

4. Assim, tudo se resume a mostrar que ${\displaystyle A\models \alpha \Leftrightarrow B\models \alpha }$ nos subconjuntos [m]. A principal abordagem aqui é usar a caracterização algébrica fornecida pelo Jogo de Ehrenfeucht–Fraïssé. Informalmente, são pegos isomorfismos parciais em A e B e depois, estendidos m vezes, para provar (ou não) ${\displaystyle A\equiv _{m}B}$, dependendo de quem ganhar o jogo.

Exemplo[editar | editar código-fonte]

Nós queremos mostrar que a propriedade do tamanho de uma estrutura (com Relação de ordem) A = (A, ≤) ser par não pode ser expressa em LPO.

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

2. Nós começamos com 2 estruturas em ordem parcial A₂ e B₂ com universos A₂ = {1, 2, 3, 4} e B₂ = {1, 2, 3, 4, 5}. Obviamente A₂ ∈ PAR e B₂ ∉ PAR.

3. Para m = 2, nos podemos mostrar* que, em um Jogo de Ehrenfeucht–Fraïssé de 2-movimentos entre A₂ e B₂, o Duplicador (membro do jogo) sempre ganha, e assim A₂ e B₂ não podem ser separadas na PO[2], ou seja, A₂ ${\displaystyle \models }$ α; ⇔ B₂ ${\displaystyle \models }$ α; para todo α; ∈ FO[2].

4. Agora nós temos que escalar as estruturas com o aumento de m. Por exemplo, para m = 3 nós precisamos encontrar um A₃ e um B₃ onde o Duplicador sempre ganhe um jogo de 3-movimentos. Isso pode ser conseguido em A₃ = {1, ..., 8} e B₃ = {1, ..., 9}. Generalizando, nós podemos escolher A_m = {1, ..., 2^m} e B_m = {1, ..., 2^m+1}; para qualquer m, o Duplicador sempre ganha um jogo de m-movimentos entre essas duas estruturas*.

5. Assim, a classe PAR nas estruturas finitas e ordenadas não pode ser expressa na LPO.

(*) Os resultados do Jogo de Ehrenfeucht–Fraïssé foram omitidos, uma vez que não são a questão principal tratada aqui.

Aplicações[editar | editar código-fonte]

Teoria de Bancos de Dados[editar | editar código-fonte]

Um fragmento substancial do SQL (aplicado na Álgebra relacional) é baseado em LPO (mais precisamente, pode ser traduzido, em termos do teorema de Edgar Frank Codd, para cálculo do domínio relacional), como o exemplo a seguir ilustra: Imagine uma tabela de banco de dados "MULHERES" com as colunas "PRIMEIRO_NOME" e "ULTIMO_NOME". Isso corresponde a uma relação binária, digamos, G(p,u) com PRIMEIRO_NOME x ULTIMO_NOME. A busca (em LPO) {u : G('Renata', u)}, que retorna todos os últimos nomes de quem tem 'Renata' como primeiro nome, em SQL, seria assim:

select ULTIMO_NOME from MULHERES where PRIMEIRO_NOME = 'Renata' 

Perceba que nós assumimos aqui que todos os últimos nomes aparecem apenas uma vez.

A seguir, queremos fazer uma coisa mais complexa. Além da tabela "MULHERES", temos agora a tabela "HOMENS" com as mesmas colunas. A busca (em LPO) é {(p,u) : ∃h ( G(p, u) ∧ B(h, l) )}, que em SQL é:

select PRIMEIRO_NOME, ULTIMO_NOME from MULHERES where ULTIMO_NOME IN ( select ULTIMO_NOME from HOMENS ); 

Perceba que para expressar o "∧", nós introduzimos o novo elemento de linguagem "IN", seguido de uma seleção. Isso torna a linguagem mais difícil de se aprender e de implementar. Essa é uma relação comum na criação de linguagens. Essa extensão da linguagem mostrada acima não é (nem de longe) a única. Por exemplo, outra maneira de escrever a mesma busca é:

select distinct g.PRIMEIRO_NOME, g.ULTIMO_NOME from MULHERES g, HOMENS b where g.ULTIMO_NOME=b.ULTIMO_NOME; 

A LPO é muito restritiva para algumas aplicações de banco de dados, por causa da falta de habilidade de expressar o Fecho transitivo. Esse fato propiciou a criação construções poderosas em termos de "linguagem de busca", como o recursive WITH (buscas recursivas em SQL) em SQL:1999. Lógicas mais expressivas têm então sido estudadas na Teoria dos Modelos Finitos por causa de sua relevância para a teoria dos bancos de dados e suas aplicações.

Consultando e Buscando[editar | editar código-fonte]

Dados na forma de palavra não têm relações definidas. Dessa maneira, as estruturas lógicas de busca e consulta de texto podem ser expressas na Lógica proposicional, como em:

("Java" AND NOT "ilha") OR ("C#" AND NOT "peixe") 

Perceba que os desafios na busca de texto são diferentes das de consulta num banco de dados, como por exemplo uma ordenação de resultados.

História[editar | editar código-fonte]

1. Trakhtenbrot 1950: falha no teorema da completude em LPO,
2. Scholz 1952: caracterização de espectros em LPO,
3. Fagin 1974: o conjunto de todas as propriedades expressáveis em lógica de segunda ordem existencial é precisamente a classe de complexidade NP,
4. Chandra, Harel 1979/ 80: Extensão com ponto-fixo (fixed-point) da LPO para linguagem de consulta em bancos de dados capaz de expressar o fecho transitivo -> consultas como objetos centrais da TMF.
5. Immerman, Vardi 1982: lógica de ponto-fixo (fixed point logic) em estruturas ordenadas captura PTIME -> complexidade descritiva (... Teorema de Immerman–Szelepcsényi)
6. Ebbinghaus, Flum 1995: Primeiro livro de compreensão da "Teoria dos Modelos Finitos" (Finite Model Theory)
7. Abiteboul, Hull, Vianu 1995: Livro "Fundamentos de Bancos de Dados" (Foundations of Databases)
8. Immerman 1999: Livro "Complexidade Descritiva" (Descriptive Complexity)
9. Kuper, Libkin, Paredaens 2000: Livro "Bancos de Dados baseados em Restrições" (Constraint Databases)
10. Darmstadt 2005/ Aachen 2006: primeiro workshop internacional abordando "Teoria de Modelos Algorítmica" (Algorithmic Model Theory)

Citações[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]

O Wikilivros tem um livro chamado Finite Model Theory

• Libkin, Leonid (2009). «The finite model theory toolbox of a database theoretician» (PDF). PODS 2009: Proceedings of the twenty-eighth ACM SIGACT–SIGMOD symposium on Principles of database systems. pp. 65–76. doi:10.1145/1559795.1559807  Também indicado como uma introdução e uma visão geral.
• Leonid Libkin. Introductory chapter of "Elements of Finite Model Theory". Motivação para três das principais aplicações: banco de dados, complexidade e linguagens formais.
• Jouko Väänänen. A Short Course on Finite Model Theory. Departamento de Matemática, Universidade de Helsinki. Baseado em palestras entre 1993-1994.
• Anuj Dawar. Infinite and Finite Model Theory, slides, Universidade de Cambridge, 2002.
• «Algorithmic Model Theory». RWTH Aachen. Consultado em 7 de novembro de 2013. Arquivado do original em 17 de julho de 2012  Inclui uma lista de problemas abertos da TMF.

Referências[editar | editar código-fonte]

• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995). Finite Model Theory. [S.l.]: Springer. ISBN 978-3-540-60149-4 

• Libkin, Leonid (2004). Elements of Finite Model Theory. [S.l.]: Springer. ISBN 3-540-21202-7 

• Abiteboul, Serge; Hull, Richard; Vianu, Victor (1995). Foundations of Databases. [S.l.]: Addison-Wesley. ISBN 0-201-53771-0 

• Immerman, Neil (1999). Descriptive Complexity. New York: Springer. ISBN 0-387-98600-6