| |
| Acadêmico(a): André Ramaciotti da Silva |
| Título: Provador interativo de teoremas com tipos dependentes |
| |
| Conclusão: |
No início do trabalho, elencou-se como objetivo criar um provador interativo de teoremas. De forma mais detalhada, objetivava-se especificar uma linguagem, seu sistema de tipos e implementar um interpretador capaz de validar e executar os programas escritos nessa linguagem. Ao término, pode-se verificar que todos os objetivos propostos foram alcançados.
Considerando como público-alvo os programadores, a possibilidade de escrever seus programas nessa linguagem e tê-los verificados por regras de validação mais restritas foi alcançada. No entanto, o uso da teoria de tipos também mostrou alguns inconvenientes. Em particular, devido à necessidade de codificar as provas nos próprios tipos e funções, muitas vezes eles se tornam mais complexos do que seriam em uma linguagem sem tipos dependentes. Um sistema de provas em que elas possam ser escritas à parte da função em si, como no caso de Coq, provavelmente seria mais vantajoso.
Para matemáticos, permitiu-se a escrita de teoremas de lógica de predicados construtiva. Para isso, o teorema que se deseja provar deve ser codificado como um tipo e a construção de um valor desse tipo cumpre o papel de uma prova. Porém, a lógica construtiva também possui suas limitações. Devido à necessidade de se construir um objeto lógico para que se considere uma prova como válida, outros tipos de prova, tal como a prova por contradição, não são considerados válidos dentro desse contexto.
A escolha de ferramentas para o desenvolvimento do trabalho foi bem acertada. A linguagem Haskell mostrou-se bastante expressiva, permitindo a escrita do interpretador em poucas linhas de código, e não houve problemas com a implementação escolhida (o compilador GHC). A escolha de linguagem também possibilitou a utilização da biblioteca Parsec, que permitiu a escrita do analisador sintático de maneira sucinta e muito próxima à notação utilizada na especificação da gramática. A ferramenta Cabal foi útil no gerenciamento do projeto, instalando as dependências necessárias e facilitando o processo de compilar, testar e executar o interpretador. A utilização do HUnit também foi um facilitador, automatizando o processo de testes, fazendo com que não fosse necessário executar diversos casos de testes para cada alteração feita no protótipo.
A única ferramenta que não teve grande impacto durante a elaboração do trabalho foi o Haddock, utilizada para a documentação. Embora os módulos e as funções tenham sido documentados segundo sua notação sem problemas, não houve utilidade prática para a documentação gerada a partir delas. No entanto, espera-se que seja útil no desenvolvimento de extensões para este trabalho. |
| |
|
