| |
|
FERNANDO
FERREIRA, Departamento de Matemática, FCUL
PRINCÍPIOS DE ANÁLISE FRACA
RESUMO
A formalização da matemática em sistemas de
aritmética de segunda-ordem (sistemas de análise)
tem uma história longa e distinta. Pode dizer-se que remonta
a Richard Dedekind e que foi objecto de atenção por,
entre outros, Hermann Weyl, David Hilbert, Paul Bernays, Georg Kreisel,
Solomon Feferman, Harvey Friedman e Stephen Simpson. Tradicionalmente,
os sistemas de aritmética de segunda-ordem estudados pressupõem
a aritmética recursiva primitiva (finistismo) e, em geral,
assumem princípios fortes de formação de conjuntos
e/ou indução. A análise fraca investiga a formalizacão
da matemática em sistemas bastante mais fracos, i.e., relacionados
com classes notáveis da complexidade computacional.
Em sistemas
fracos há questões delicadas sobre a representação
dos objectos matemáticos. Nesta conferência, mostramos
como se podem representar os números reais e as funções
contínuas. Demonstramos o teorema do valor intermédio,
o que permite concluir que o nosso sistema interpreta a teoria dos
corpos ordenados realmente fechados. Uma consequência interessante
deste resultado é a seguinte: a álgebra e a análise
elementares (incluindo a geometria euclideana) é interpretável
numa teoria aritmética sem indução.
Nas últimas
duas décadas o programa da Matemática Recíprocatem
investigado a força lógica e matemática dos
teoremas da matemática usual. A cartografia destas relações
de força já está delineado nos seus traços
gerais, tendo-se obtido um mapa muito interessante. O programa tem-se
concentrado nos sistemas aritméticos tradicionais. Um dos
objectivos da análise fraca é esboçar um mapa
semelhante em que se pressupõem apenas teorias fracas. Mostraremos
alguns resultados nesta direcção. Na última
década, Ulrich Kohlenbach tem investigado o problema de extrair
informação computacional de demonstrações
>clássicas("proof mining"). No âmbito
dos sistemas fracos, esta investigação é potencialmente
interessante e, a nosso ver, poderá ser eficazmente conduzida
por um mapa do género descrito acima.
Enquanto que
o impacto dos computadores na Análise Numérica tem
sido tremendo, o impacto da Ciência da Computação
nesta disciplina é quase nulo. A razão é simples:
a complexidade computacional estuda o discreto, enquanto que a Análise
Numérica trabalha com o contínuo. É, noutras
roupagens, o antigo problema do contínuo versus discreto.
Há indícios de que a abordagem do último parágrafo
possa contribuir para fundamentar partes da Análise Numérica.
São matérias controversas e, antes de tudo, é
mister investigá-las!
Parte deste
trabalho foi efectuado em colaboração com: António
M. Fernandes (IST).
VOLTAR
ISABEL
OITAVEM, Departamento de Matemática, FCT,
Universidade Nova de Lisboa
CARACTERIZAÇÕES
IMPLÍCITAS: UMA ABORDAGEM COMUM A PTIME, LSPACE,
E NC
RESUMO
Todas as classes de complexidade computacional são, em primeira
instância, definidas com base em processos mecânicos
(máquinas de Turing, circuitos ou outros), sobre os quais
eventualmente recaem limitações quanto aos recursos
disponí veis durante a computação. Para muitas
das mais relevantes classes de complexidade têm vindo a ser
estabelecidas caracterizações onde quer o processo
mecânico em questão quer os recursos disponíveis
estão implícitos - caracterizações
implícitas. A obtenção de caracterizações
implícitas, para além do seu interesse intrínseco,
permite-nos transpor problemas do âmbito da complexidade computacional
para outros domí nios.
É nosso
objectivo descrever caracterizações implícitas
de três classes de complexidade: Ptime, Lspace
e NC. As caracterizações aqui apresentadas
são expressas num contexto de álgebras livres. Isto
permite-nos obter caracterizações implícitas
de classes tão diversas como Ptime, Lspace
e NC mudando apenas a álgebra de base. Deste modo,
damos uma abordadem comum a classes de complexidade computacional
que resultam de processos computacionais tão diferentes como
deterministas e alternados com restrições de tempo,
espaço ou tempo e espaço.
VOLTAR
MANUEL
LAMEIRAS CAMPAGNOLO, Departamento de Matemática,
Instituto Superior de Agronomia
FUNÇÕES REAIS
RECURSIVAS
RESUMO
Em teoria das funções recursivas definem-se classes
de funções que contém um conjunto de funções
iniciais e são fechadas relativamente a um conjunto de operações,
tais como, por exemplo, composição de funções,
iteração ou recursão primitiva. Analogamente,
definem-se classes de funções reais recursivas com
funções iniciais definidas em R e operadores que transformam
funções de variável real em funções
de variável real, tais como composição ou integração.
As classes de
funções recursivas, também designadas por álgebras
de funções, possuem propriedades algébricas.
Por exemplo, uma dada classe pode ser ou não fechada relativamente
a uma determinada operação. Possuem também
propriedades computacionais. Por exemplo, uma dada álgebra
de funções pode estar ou não contida numa determinada
classe de complexidade computacional.
Nesta comunicação
mostrar-se-á que o mesmo tipo de questões se colocam
para funções reais recursivas. Serão dados
exemplos de classes de funções reais recursivas e
de propriedades que essas classes possuem.
Adicionalmente,
as álgebras de funções definidas em teoria
das funções reais recursivas podem possuir propriedades
analíticas tais como continuidade ou analiticidade dos elementos
dessas álgebras. Consequentemente é possível
estabelecer relações entre as suas propriedades computacionais
e analíticas.
As principais
operações consideradas na definição
de classes de funções recursivas são operações
de integração de equações diferenciais,
i.e., operações que transformam um par de funções
na solução de um problema de Cauchy por elas definido.
Assim, diversos resultados que serão descritos estabelecem
conexões entre a teoria das equações diferenciais
e a teoria da complexidade computacional.
VOLTAR
JOSÉ
JÚLIO ALFERES, Departamento de Informática,
FCT, Universidade Nova de Lisboa
"UPDATES" DE PROGRAMA
EM LÓGICA
RESUMO
Até há bem pouco tempo, o uso da programação
em lógica para representação do conhecimento
centrava-se essencialmente na representação de conhecimento
sobre uma realidade estática, i.e. uma realidade que não
evolui ao longo do tempo. Note-se que isto não significava
que o conhecimento fosse ele próprio estático: vários
trabalhos trataram do problema de como fazer evoluir um programa
face à aquisição de mais informação
sobre uma dada realidade. Mas, desde 1988 com o trabalho de Winslett,
que sabemos que os formalismos lógicos para lidar com actualizações
de conhecimento por via de aquisição de nova informação
sobre uma realidade estática (i.e. para lidar com revisão
de crenças) não são adequados para lidar com
actualizações de conhecimento causadas por alterações
na realidade modelada (i.e. para lidar com "updates").
No contexto
da programação em lógica o problema de base
dos "updates" enuncia-se de forma simples: dada uma sequência
de programas P_1 + ... + P_n, onde cada programa P_i representa
informação que passou a estar em vigor no momento
i, o que é verdade em cada momento desde 1 até n?
Se assumirmos que em cada momento i esse significado pode ser expresso
por apenas um programa em lógica, todas as regras que fazem
parte de P_i terão necessariamente que ser verdadeiras dado
esse significado. Quanto às regras introduzidas em momentos
anteriores a i, umas deverão também ter que ser verdadeiras.
Mas outras poderão ser falsas, pois correspondem a regras
que entretanto foram "desactualizadas" face a informação
posterior. Um dos componentes fundamentais na definição
de uma semântica declarativa para "updates" de programas
é pois o determinar, em cada momento, quais as regras que
estão em vigor e quais as que (no todo ou em parte) deverão
ser preteridas face à nova realidade. Falar-vos-ei um pouco
sobre uma tal semântica declarativa para "updates",
bem como sobre procedimentos (e respectivas implementações)
para essa semântica.
No final da
comunicação dar-vos-ei ainda conta de alguns domínios
de aplicação de "updates" de programas em
lógica. E há várias aplicações
possiveis. Por exemplo: modelação de leis e regulamentos
que vão sendo especificadas e alteradas ao longo do tempo
(que leis continuam em vigor? quais foram preteridas face a novas
leis?); modelação de alterações a especificações
de software; modelação de agentes racionais que deverão
saber reagir a um ambiente em mudança (tanto de factos observáveis,
como das próprias regras pela qual o agente se deve reger).
VOLTAR
SABINE BABETTE BRODA, Departamento
de Ciência de Computadores, FCUP
GERAÇÃO
DE HABITANTES NORMAIS EM TA_LAMBDA
RESUMO
Versões tipadas de sistemas de lambda-calculus têm
sido estudadas desde o seu aparecimento no início deste século,
devido à sua importância para diversas áreas
da lógica matemática e ultimamente também para
a ciência de computadores. Uma das sub-áreas onde encontra
aplicação directa é a programação
funcional (e.g. as linguagens ML, Miranda ou Haskell), um exemplo
paradigmático duma área na ciência de computadores
onde a interligação estreita entre teoria e prática
levou a um crescimento frutuoso de ambas: os desenvolvimentos na
teoria levam a aplicações práticas directas
e as necessidades da implementação suscitam novas
abordagens teóricas. De facto, a programação
funcional baseia-se na representação de funções
computáveis/algoritmos por lambda-termos e a execução
de programas corresponde à redução de lambda-termos.
Uma atribuição de tipos a lambda-termos fornece então
uma especificação parcial dos algoritmos que são
representados, e serve para mostrar a correcção parcial
dos programas definidos. Por outro lado, usam-se os tipos também
para melhorar a eficiência da compilação de
programas funcionais (termos), identificando e implementando de
maneira adequada, por exemplo, partes
(sub-termos) com tipo especial (e.g. aritmético). Na base
de praticamente todos os sistemas utilizados encontra-se o sistema
TA_lambda o que justifica a atenção que tem recebido
no meio científico. Por outro lado, existe uma correspondência
directa, via isomorfismo de Curry-Howard, entre TA_lambda e o fragmento
implicacional P(->) do cálculo proposicional intuicionista.
De facto, um tipo tau pode ser inferido para algum lambda-termo
se e só se tau é um teorema de P(->). Para além
disso, cada termo (em forma normal) para o qual tau pode ser inferido,
i.e. cada habitante (normal) de tau representa uma prova (em forma
normal) da fórmula tau no sistema de dedução
natural.
Nesta apresentação
começamos por introduzir uma representação
alternativa para tipos em TA_lambda (ou equivalentemente para fórmulas
em P(->)). Esta representação evidencia a relação
existente entre a estrutura de um tipo e a estrutura dos seus habitantes
normais. Baseada nesta representação definimos ainda
o conceito de árvore de prova válida para um tipo
tau. Mostramos que cada uma destas árvores corresponde a
um conjunto finito de habitantes normais de tau e que todo o habitante
normal corresponde exactamente a uma árvore de prova válida
para tau. Apresentamos algoritmos precisos para estabelecer esta
relação. Characterizamos ainda as árvores de
prova que correspondem a habitantes principais normais de um tipo
tau.
Em 1996, Takahashi
et al. mostraram que o conjunto de habitantes normais de um tipo
tau pode ser descrito utilizando uma generalização
do conceito de gramática de contexto livre, em que se pode
utilizar um número infinito de símbolos não
terminais bem como regras de produção. O conjunto
de habitantes normais de tau obtém-se então a partir
do conjunto de termos gerado por essa gramática infinita,
por redução-eta. Utilizando a representação
introduzida para os tipos em TA_lambda, mostramos que o conjunto
de habitantes normais de um tipo tau pode de facto ser descrito
por uma gramática de contexto livre (finita) e os habitantes
normais de tipos com uma mesma estrutura são descritas por
gramáticas idênticas, a menos de renomeação
de símbolos.
VOLTAR
PAULO MATEUS, Departamento de
Matemática, IST
PROTOCOLOS
DE COMPUTAÇÃO SEGURA
RESUMO
O problema central da área de computação segura
consiste em avaliar uma função publicamente mantendo
os seus argumentos secretos. Um exemplo motivador e familiar é
o protocolo de eleição, que em termos vagos procede
da seguinte forma: depositam-se os votos secretos numa urna, estes
são contados por um agente de confiança que, por fim,
anuncia o resultado. Como este exemplo indica, na presença
de um agente de confiança o problema central é resolvido
trivialmente. O objectivo principal deste ramo da criptografia é
estabelecer protocolos onde este agente não esteja presente.
Os protocolos
propostos na literatura assentam na conjectura da existência
de permutações de sentido único, que por sua
vez implica NP diferente de P. Para além destas conjecturas
fundamentais e da questão essencial de desenhar protocolos,
o principal problema levantado nesta área consiste em demonstrar
que os protocolos são invioláveis, tendo em linha
de conta que uma certa percentagem de participantes é honesta.
Para este problema apresentam-se detalhadamente os dois resultados
centrais: uma função pode ser computada em segurança
usando canais privados caso a maioria dos participantes seja honesta;
uma função pode ser computada em segurança
usando canais públicos caso mais de dois terços dos
participantes sejam honestos. Salienta-se que estes resultados baseiam-se
numa séries de suposições, tais como os participantes
honestos nunca podem ser corrompidos, que quando adulteradas resultam
num novo problema, muitas vezes aberto. Este facto justifica uma
apresentação cuidada de todas estas suposições,
que, em geral, se edificam em seis parâmetros: número
de participantes; percentagem de participantes desonestos (chamados
de adversários); tipo de adversários; complexidade
computacional dos participantes; erro permitido; tipo de canais.
Após
percorrer rapidamente os resultados obtidos nas diversas variantes
do problema em mente, observa-se que todos eles são obtidos
de forma similar, i.e., mostrando que o protocolo proposto simula
o protocolo ideal com um agente de confiança. Para os casos
em aberto, nota-se que o conceito de segurança encontra-se
ainda por definir rigorosamente. Para um caso conhecido, a noção
de segurança é apresentada e discutida usando uma
álgebra de processos probabilísticos munida de uma
relação de simulação.
Finalmente,
tendo em linha de conta que todos os resultados na literatura são
obtidos caso a caso, apresenta-se a necessidade de criar métodos
formais, tais como os baseados em lógicas modais (já
existentes para protocolos de autenticação), para
provar que os protocolos de computação segura são
invioláveis, ou por outro lado, encontrar falhas nos mesmos.
VOLTAR
|
