| |
| Acadêmico(a): André Ramaciotti da Silva |
| Título: Provador interativo de teoremas com tipos dependentes |
| |
| Introdução: |
Embora ainda seja um assunto relativamente polêmico dentro da Matemática, matemáticos estão aos poucos aceitando o uso de ferramentas computacionais para auxílio na validação e no desenvolvimento de provas formais (AVIGAD; HARRISON, 2014). Provavelmente, um dos casos mais importantes nessa área foi o teorema das quatro cores1, comprovado por Appel e Haken (1977), primeiro teorema a ser provado com a ajuda de um computador.
Na computação, Hudak e Jones (1994) afirmam que programadores vêm percebendo as vantagens de se usar linguagens de programação funcionais com sistemas de tipos mais expressivos. Esses sistemas podem ser estendidos com diferentes abstrações e uma que tem recebido destaque recentemente é a teoria de tipos dependentes (MCBRIDE; MCKINNA, 2004), em que o tipo de um termo pode depender do valor de outro termo.
Os avanços das duas áreas se encontram nos provadores interativos de teoremas. Essas ferramentas, entre as quais a mais conhecida possivelmente seja Coq (THE COQ DEVELOPMENT TEAM, 2014), cumprem o papel duplo de verificar definições e teoremas matemáticos, além de certificarem que programas estão corretos com regras de validação mais restritas que a maioria das linguagens de programação utiliza.
Dentre as possíveis fundamentações teóricas para o desenvolvimento de provadores interativos de teoremas, a teoria dos tipos dependentes ainda é relativamente pouco explorada. Porém, começa-se a perceber seu potencial e linguagens de programação de cunho mais acadêmico, tais como Agda (NORELL, 2007) e Epigram (MCBRIDE, 2005), têm começado a utilizá-la. Entre as linguagens de programação de cunho mais comercial, o progresso é mais lento, mas extensões permitem simular algumas características de tipos dependentes na linguagem Haskell (MCBRIDE, 2002).
Diante desse contexto, percebe-se a importância de um provador interativo de teoremas. Sendo assim, propõe-se o desenvolvimento de um sistema em que programas e teoremas sejam validados e executados de acordo com as regras da teoria de tipos dependentes.
Para programadores, este trabalho se mostra relevante por permitir um contato inicial com a teoria de tipos dependentes em um contexto simplificado, fazendo com que seja mais fácil aprender suas peculiaridades. Além disso, um programador pode utilizar-se do sistema
1 O teorema das quatro cores é um teorema dentro da teoria de grafos que afirma que um mapa plano pode ser colorido com apenas quatro cores sem que regiões vizinhas compartilhem a mesma cor. Foi demonstrado pela primeira vez por Appel e Haken (1977) com o auxílio de um computador.
15
de tipos desenvolvido neste trabalho para verificar seu programa com regras de validação mais restritas que as encontradas na maioria das linguagens atuais, reduzindo o número de erros em tempo de execução.
Já para matemáticos, este trabalho é relevante, pois permite que escrevam seus teoremas de lógica de primeira ordem e os tenham validados pelo sistema de tipos da linguagem. No entanto, é importante ressaltar que o trabalho desenvolvido não objetiva chegar à prova de teoremas automaticamente, apenas checar se estão corretos de acordo com os teoremas previamente definidos. Ainda que em alguns casos seja possível inferir as definições intermediárias necessárias para que um teorema seja provado automaticamente, isso está além dos objetivos do trabalho. |
| |
|
