aula09_2010

Prévia do material em texto

A´lgebra A - Aula 09
Lo´gica e cieˆncia da computac¸a˜o
Elaine Pimentel
Departamento de Matema´tica, UFMG, Brazil
2o Semestre - 2010
Motivac¸a˜o
Lo´gica em cieˆncia da computac¸a˜o:
I Primeira abordagem computac¸a˜o-como-modelo: computac¸o˜es:
estruturas matema´ticas contendo nodos, estados e transic¸o˜es
e a lo´gica constro´i afirmativas sobre essas estruturas.
I Segunda abordagem computac¸a˜o-como-deduc¸a˜o: estados:
descritos atrave´s de um conjunto de proposic¸o˜es; mudanc¸as
nos estados: modelados por mudanc¸as nas proposic¸o˜es dentro
de uma derivac¸a˜o.
Motivac¸a˜o
I Primeira abordagem: tem sido amplamente estudada e faz
uso de to´picos da matema´tica como teoria de conjuntos,
teoria das categorias, a´lgebras, etc. para modelar
computac¸o˜es (estruturas matema´ticas complexas).
I Segunda abordagem: lida com estruturas mais simples (que
raramente fazem refereˆncia ao infinito).
I Apo´s recentes pesquisas na a´rea de teoria de provas e
programac¸a˜o lo´gica (lo´gica linear) observou-se um
crescimento do estudo nessa a´rea de pesquisa.
Lo´gica Cla´ssica
I A verdade de uma afirmativa e´ absoluta e independe da
quaisquer pensamento, entendimento ou ac¸a˜o.
I Afirmativas sa˜o verdadeiras ou falsas, onde falso e´ a mesma
coisa que na˜o verdadeiro.
I Isso e´ conhecido com princ´ıpio do meio exclu´ıdo: p ∨ ¬p.
Lo´gica Intuicionista
I Em p ∨ ¬p nenhuma informac¸a˜o e´ dada sobre qual realmente
vale:
Existem dois nu´meros irracionais x e y tais que xy e´
racional.
Existem sete 7s consecutivos na representac¸a˜o
decimal do nu´mero pi.
I Afirmativas so´ sa˜o va´lidas perante a existeˆncia de uma prova
ou construc¸a˜o da afirmativa.
Lo´gica intuicionista
I Essa lo´gica e´ de especial interesse porque suas fo´rmulas esta˜o
em correspondeˆncia 1 a 1 com tipos em λ-calculus, base das
linguagens de programac¸a˜o funcionais: Lisp, ML, Haskell.
I Ainda, lo´gica intuicionista e´ uma lo´gica de recursos infinitos
(mas na˜o de concluso˜es infinitas).
Lo´gica linear
I Lo´gica linear e´ uma lo´gica de recursos conscientes.
I No caso de transic¸a˜o de estados:
maior tem valor 1 −◦ maior tem valor 2
I E´ claro que a proposic¸a˜o { maior tem valor 1} deve deixar de
ser va´lida no estado 2, enquanto que a proposic¸a˜o { maior
tem valor 2}, que na˜o era va´lida no estado 1, passa a valer no
estado 2.
I Esse tipo de comportamento na˜o pode ser descrito em lo´gicas
cla´ssica ou intuicionista, apenas em lo´gica linear.
Linguagens lo´gicas de programac¸a˜o - Prolog
I Cla´usulas de Horn:
G ::= A|G ∧ G
D ::= A|G ⊃ A|∀xD
I Ou seja, fo´rmulas gol sa˜o conjunc¸o˜es de fo´rmulas atoˆmicas e
cla´usulas de programas sa˜o da forma:
∀x1 . . . ∀xm[A1 ∧ . . . ∧ An ⊃ A0]
I Assinaturas e programas sa˜o globais.
I Ou seja, nada de mecanismos para modularizac¸a˜o ou
construtores de dados!
Linguagens lo´gicas de programac¸a˜o - λ-Prolog
I Fo´rmulas de primeira ordem de Harrop:
G ::= A|G ∧ G |P ⊃ G |∀xG
D ::= A|G ⊃ A|∀xD
I Deste modo, o programa pode crescer ao longo da prova
(modularizac¸a˜o) e novas constantes podem ser adicionadas ao
programa (abstract datatypes)
I Desvantagem: recursos ilimitados para construc¸a˜o de provas.
Linguagens lo´gicas de programac¸a˜o - Forum
I Lo´gica linear na˜o e´ uma linguagem abstrata de programac¸a˜o.
I Forum e´ uma linguagem lo´gica de programac¸a˜o baseada em
lo´gica linear.
I Ale´m de modularizac¸a˜o e abstrac¸a˜o de dados tambe´m permite
encapsulac¸a˜o de estado, concorreˆncia e primitivas de
comunicac¸a˜o e sincronizac¸a˜o.