62ª Reunião Anual da SBPC

A. Ciências Exatas e da Terra - 2. Ciência da Computação - 16. Teoria da Computação

FORMALIZAÇÃO DO TEOREMA DE FERMAT GENERALIZADO

Lucas de Melo Guimarães ¹
Flávio Leonardo Cavalcanti de Moura ²

1. Depto.de Ciência da Computação - UnB
2. Prof. Dr. / Orientador - Depto.de Ciência da Computação - UnB

INTRODUÇÃO:

O trabalho em questão tem como objetivo verificar formalmente uma generalização do teorema de Fermat. A verificação formal e o uso de assistentes de provas são importantes para garantir a prova de algoritmos e teorias, como é o caso deste trabalho. Para este trabalho, utilizou-se o assistente de provas Coq, um sistema baseado em uma lógica de ordem superior utilizado na formalização de diversas teorias e sistemas computacionais.

Dada esta breve exposição sobre verificação formal, será apresentada a generalização do teorema de Fermat. A generalização proposta afirma que; se y e n são coprimos então, n é primo, se e somente se, (x+y) [n] = x[n] + y módulo n, onde a[b] denota "a" elevado a "b".

A verificação da generalização apresentada tem uma relevância significativa, uma vez que constitui um passo para o objetivo maior de provar formalmente a correção do algoritmo AKS(Agrawal-Kayal-Saxena).

METODOLOGIA:

Para se verificar a generalização proposta, optou-se por utilizar o provador de teoremas Coq, que provê uma linguagem formal que tem como intuito facilitar a escrita de definições matemáticas, algoritmos executáveis, bem como teoremas. Isto tudo está constituído em um ambiente semi-interativo para o desenvolvimento de provas checadas via software.

O Coq implementa uma linguagem denominada Gallina, que é baseada em um formalismo conhecido como Calculus of Inductive Constructions, possibilitando que o usuário seja capaz de definir funções e predicados, declarar teoremas matemáticos, desenvolver interativamente e formalmente estes teoremas, além de ter suas provas testadas por um número relativamente pequeno de regras.

Apesar de se ter utilizado um assistente de provas, foi necessário, primeiramente, fazer algumas demonstrações à mão com o intuito de se escolher a melhor abordagem, uma vez que as provas, em Coq, precisam ser construtivas.

RESULTADOS:

Acerca dos resultados do trabalho em questão, pode-se dizer que já foi verificada, em Coq, a parte da generalização que afirma; se y e n são coprimos e n é primo, então (x+y) [n] = x[n] + y módulo n.

Quanto à outra parte da demonstração, está em fase de conclusão. Nesta parte, já se verificaram diversos resultados matemáticos no que tange a números binomiais. Ainda sobre os binomiais, foram verificados resultados importantes, tais como o fato dos números binomiais serem necessariamente inteiros, bem como a definição mais usual de números binomiais, isto é, aquela em que o número binomial é relacionado ao quociente de fatoriais. Além disso, foram verificadas também duas decomposições não triviais de números binomiais. A primeira é a relação de Stifel, isto é, aquela que se baseia no triângulo de Pascal, decompondo o binomial na soma de outros dois. A segunda decompõe o binomial em um produto entre uma fração e um binomial onde os dois parâmetros são decrescidos de uma unidade em relação ao binomial original.

CONCLUSÃO:

Com base nos resultados apresentados, pode-se assegurar que a maior parte dos fatos matemáticos que servem como base para a demonstração da generalização do teorema de Fermat já foi verificada. A prova do teorema de Fermat generalizado é um passo importante na prova da correção do algoritmo AKS de forma mecânica, ou seja, via um assistente de provas. Tal procedimento exige um estudo detalhado do citado algoritmo o que pode permitir contribuições no que concerne a melhores cotas que permitam a construção de versões mais eficientes e extração de código correto efetivamente utilizáveis na prática. Como trabalho futuro, pretende-se terminar os poucos fatos que faltam para a verificação completa da generalização, bem como verificar o algoritmo AKS, com o fim de assegurar a sua correção.

Instituição de Fomento: Conselho Nacional de Desenvolvimento Científico e Tecnológico - CNPq

Palavras-chave: Teorema de Fermat, Verificação Formal, Primalidade.