Aplicações da Lógica na Computação

Prévia do material em texto

1 
Abril de 2008 INF05508 – Lógica para Computação 
 
Das aplicações da lógica na Computação 
 
Bruno Silva Guedes 
1
 
Leonardo Roveda Faganello 
2
 
Matheus de Carvalho Proença
3
 
Thiago Caberlon Santini 
4
 
(artigo escrito para trabalho da disciplina INF05508 – Lógica para Computação) 
 
Resumo 
A lógica possui aplicações inesperadas em diversas áreas da Ciência da 
Computação. São sobre essas aplicações que o artigo On the Unusual Effectiveness of 
Logic in Computer Science versa. A lógica, que teoricamente é considerada derivada da 
Matemática, encontra muito mais aplicações práticas na Ciência da Computação, e 
baseado nos exemplos citados pelo artigo em inglês, resumimos aqui a idéia básica 
destas aplicações. 
 
 
 
 
 
1
 Graduando em Engenharia de Computação 
Universidade Federal do Rio Grande do Sul 
E-mail: bsguedes@inf.ufrgs.br 
 
2
 Graduando em Engenharia de Computação 
Universidade Federal do Rio Grande do Sul 
E-mail: lrfaganello@inf.ufrgs.br 
 
3
 Graduando em Engenharia de Computação 
Universidade Federal do Rio Grande do Sul 
E-mail: mcproenca@inf.ufrgs.br 
 
4
 Graduando em Engenharia de Computação 
Universidade Federal do Rio Grande do Sul 
E-mail: tcsantini@inf.ufrgs.br 
 
2 
 
INTRODUÇÃO 
 
Considerada “o Cálculo da Ciência da Computação”, a lógica desempenhou 
um papel fundamental no desenvolvimento dessa área do conhecimento. 
Desenvolvida fortemente no início do século XX, com o objetivo de formalizar e reunir 
todo o conhecimento matemático até então desenvolvido, a lógica acabou perdendo 
espaço entre os matemáticos, após Gödel demonstrar que a lógica de primeira ordem 
não era suficiente para demonstrar a completude da Matemática. 
Após a metade do século XX, a lógica se desvinculou da matemática 
tradicional e seu desenvolvimento está concentrado na sua potencialidade de 
aplicações. Do mesmo modo que a matemática encontrou aplicações em áreas 
“inesperadas” nas Ciências Naturais, como Física, Biologia, Química, a Lógica 
encontrou amparo na Ciência da Computação, em aplicações como Complexidade de 
Algoritmos e Banco de Dados, bases da Teoria da Computação, Teoria dos Tipos, 
Circuitos Digitais e Lógica Epistêmica, outros tópicos fundamentais na Computação. 
Os tópicos a seguir são baseados no artigo On the Unusual Effectiveness of 
Logic in Computer Science, escrito por Joseph Halpern, Robert Harper, Neil Immerman, 
Phokion Kolaitis, Moshe Vardo e Victor Vianu. O artigo foi publicado no The Bulletin of 
Symbolic Logic, Volume sete, Número 2, em junho de 2001. 
3 
 
APLICAÇÕES NA TEORIA DE COMPLEXIDADE 
A computação nos auxilia na resolução de milhares de tipos de problemas. A 
forma como um computador resolve problemas se baseia na execução de um 
algoritmo previamente pensado por algum ser humano. Como o computador é 
limitado fisicamente, faz sentido prever que um computador leva mais tempo para 
resolver problemas mais difíceis. A medida de “dificuldade” de um problema está 
diretamente relacionada com a complexidade do algoritmo que o resolve. Encontrar 
melhores algoritmos para resolução de certos problemas sempre foi uma tarefa 
primordial para o desenvolvimento da Teoria da Computação. 
A lógica está intimamente ligada à criação e desenvolvimento destes 
algoritmos mais robustos. A aplicação que o artigo cita são os problemas P e NP. Em 
complexidade, problemas do tipo P são aqueles que podem ser resolvidos em tempo 
polinomial O(f(n)), onde f(n) é uma função do tipo anx
n
 + an-1x
n-1 
+ ... + a0 (polinômio). 
Já os problemas NP são problemas cujos algoritmos trabalham em tempo superior ao 
polinomial, geralmente exponencial (algo como O(a
n
), a > 0 por exemplo). 
Dentro da classe de problemas NP, temos os chamados problemas NP-
Completos, que não podem ser reduzidos a problemas do tipo P. Porém, existem 
certos problemas em NP que podem ser reduzidos a P com alguma manipulação 
lógica-algébrica. Com o uso da Complexidade descritiva e as Lógicas de Primeira e 
Segunda Ordem, chega-se ao seguinte corolário: 
Corolário. (P = NP) ⇔ FO(LFP) = SO, onde LFP é um operador de mínimo ponto 
fixo e FO e SO se referem às lógicas de primeira e segunda ordem, respectivamente. 
Os problemas que podem ser manipulados dessa maneira podem ser 
transformados em tempo polinomial em problemas NP-completos. Caso se descubra 
uma maneira de resolver problemas NP completo em tempo polinomial, então 
finalmente teríamos uma maneira de resolver todos os problemas em NP em tempo 
polinomial. Esta questão ainda continua em aberto, e é um dos maiores problemas não 
resolvidos da Ciência da Computação. 
LÓGICA EM BANCO DE DADOS 
O impacto da lógica nos bancos de dados é um dos melhores exemplos da 
efetividade da mesma sobre a ciência da computação. A lógica de primeira ordem 
4 
 
reside no núcleo dos bancos de dados atuais, sendo utilizada desde as linguagens mais 
básicas como SQL até algumas mais complexas onde são utilizadas extensões da lógica 
de primeira ordem junto com a recursão. 
Há três motivos principais para sua utilização: 
1) - A lógica de primeira ordem possui variáveis sintáticas de fácil utilização. 
2) - Pode ser implementada usando relações algébricas, o que representa uma 
vantagem crucial quando tratamos de uma grande quantidade de dados. 
3) - Suas buscas podem demorar tempos constantes para qualquer tamanho 
do banco de dados se houver paralelismo suficiente. 
Uma busca que pode ser expressa em uma lógica de primeira ordem pode ser 
aberta em uma série de buscas menores, formando assim blocos fundamentais que 
podem ser usados na busca. Porém está abordagem não é satisfatória, pois pode ser 
muito lenta com o aumento do banco de dados. A abordagem utilizada na prática 
envolve relações algébricas. Em resumo, a lógica de primeira ordem e a relação 
algébrica expressam a mesma busca. 
O uso da álgebra de relações para realizar buscas pode ser implementada 
usando estruturas de dados chamadas de “indexes” que permitem acesso rápido aos 
dados, somando isso a algumas regras de reescrita, a mesma busca, após reescrita, 
pode levar apenas n log(n) em vez de n². 
Como citado antes, buscas usando a lógica de primeira ordem podem ser 
realizadas com tempo constante independente do tamanho do banco de dados, isto só 
pode ser realizado graças ao processamento em paralelo, onde mais uma vez a álgebra 
de relações nos permite tal feito. Porém é necessário o uso de muitos processadores 
tornando, por enquanto, inviável o uso de seu potencial máximo. Contudo há 
algoritmos que são capazes de tirar o máximo de proveito de um grupo de 
processadores e os processadores usados para realizar operações algébricas não 
precisam ser poderosos. 
Finalizando, a lógica é uma ferramenta muito efetiva na área de banco de 
dados. A lógica de primeira ordem é uma ótima base para as linguagens de busca 
padrão devido à sua implementação eficiente e seu fácil uso. 
5 
 
TEORIA DOS TIPOS NAS LINGUAGENS DE PROGRAMAÇÃO 
Nas décadas de 80 e 90, o estudo das linguagens de programação foi 
revolucionado por uma confluência de idéias da lógica matemática e filosófica e da 
teoria da computação: a Teoria dos Tipos. 
A Teoria dos Tipos, aplicada a um sistema de tipos, impõe restrições aos 
programas, prevenindo que ocorram vários erros, decorridos de falhas na 
interpretação dos valores, como, por exemplo, aplicar uma função a um número 
inteiro utilizando valores lógicos. 
Um sistema de tipo é definido da seguinte forma: Γ╟ e : τ, onde e é uma 
expressão, τ é seu tipo e Γ representa tipos das variáveisglobais que podem ocorrer 
em e. 
 Segundo o princípio das “proposições como tipos” há um isomorfismo entre 
proposições e tipos, com a propriedade que a dedução natural prova que uma 
proposição corresponde aos elementos de seu tipo associado. Esse princípio se 
estende aos conetivos lógicos e quantificadores, incluindo os de segunda ordem ou de 
ordem maior. 
 Organizar linguagens de programação por estrutura de tipos possui vários 
benefícios, como evitar confusões de conceitos distintos, ocorrência de erros de 
interpretação, e aperfeiçoar a eficiência e a integridade do compilador. 
LÓGICA EPISTÊMICA 
Os estudos da lógica epistêmica se iniciaram nos anos 50, mas seu interesse 
só floresceu mais recentemente, para a implementação em vários campos da 
computação, como teoria dos jogos e IA. A chave dessa lógica é a conexão entre 
conhecimento e ação. O que um agente precisa saber sobre a operação de outro 
agente para realizar sua própria operação? 
Um modelo utilizado para isso é o seguinte: 
- Possuímos um conjunto Φ de proposições primitivas, onde uma proposição 
p pertencente a Φ, representa um fato básico, como por exemplo “Está chovendo na 
Espanha”, e um conjunto {1. . . . n} de agentes. 
- Utilizamos apenas conjunções e negações, como na lógica proposicional, e 
operadores modais K1,...Kn, E e C. Dessa forma, Kiφ é lido como “Agente i conhece 
6 
 
φ” , Eφ é lido como “Todos conhecem φ”, e Cφ é lido como “φ é de 
conhecimento comum.” 
A semântica dessa lógica, como a de outras lógicas modais, é baseada em 
mundos possíveis. 
VERIFICAÇÃO AUTOMATIZADA DE DESIGNS DE SEMICONDUTORES 
Os circuitos integrados construídos sobre semicondutores estão presentes 
praticamente na totalidade das interações tomadas em nosso dia-a-dia. Além disso, 
eles passaram a facilitar nossa vida cada vez mais, tornando-se capazes de executar 
tarefas cada vez mais complexas. Tal capacidade implica no aumento da complexidade 
do projeto de tais circuitos, que por sua vez acarreta numa cada vez maior dificuldade 
de desenhá-los, fazendo com que os projetistas não sejam capazes de usufruir o total 
potencial que a tecnologia é capaz de oferecer devido à grande possibilidade de erro. 
Para contornar esses problemas, os profissionais da área implementaram uma 
série de métodos de validação do circuito, que seriam capazes de verificar se o mesmo 
executa a função para qual foi projetado, concluindo assim se há erros no projeto ou 
não. Infelizmente, esse tipo de processo se tornou também complexo demais, 
atingindo o ponto em que a indústria passou a se referir ao problema como “crise da 
validação” quando o processo de validação atingiu metade dos recursos para a 
produção do circuito. 
Verificação formal é um processo matemático utilizado para verificar o 
comportamento de um modelo, dado uma especificação inicial. Recentemente, tal tipo 
de ferramenta era de interesse somente acadêmico, mas com a evolução do problema, 
passou a ser amplamente utilizado industrialmente. Um dos métodos mais utilizados a 
fim de tal prática é a lógica temporal linear (LTL – Linear Temporal Logic, em inglês), 
onde os momentos no tempo são tratados como se houvesse um único futuro 
possível. 
Em LTL as fórmulas são construídas com proposições atômicas, os operadores 
booleanos usuais e os operadores temporais unários X (próximo), F (eventualmente) e 
G (sempre), e o operador temporal binário U (enquanto). Esses operadores são 
capazes de modelar uma computação sobre a especificação dada, sendo possível 
verificar seu comportamento. 
7 
 
Ferramentas para modelagem e verificação do comportamento dos 
semicondutores não param em LTL. Há muitas outras abordagens lógicas possíveis 
para a resolução do problema, tendo, todas juntas, mostrado sua capacidade para 
auxiliar na continuidade da evolução da área, resolvendo problemas fundamentais 
para a computação. 
8 
 
CONCLUSÃO 
Os efeitos e aplicações da lógica sobre a computação se estendem sobre as 
mais diversas áreas da mesma, dos mais altos níveis, como inteligência artificial, aos 
mais baixos, como na produção dos circuitos integrados. Assim, fornece não somente 
uma base sólida para a fundamentação do ramo, mas também uma poderosa 
ferramenta para o desenvolvimento do mesmo.