Detalhes dos Anais Veja o resumo do trabalho

Publicado no Encontro de Saberes 2015

Evento: XXIII Seminário de Iniciação Científica

Área:

Subárea:

Título
PROVAS DE TERMINAÇÃO GENÉRICAS EM TEORIA DE TIPOS CONSTRUTIVA --- MÉTODOS, TÉCNICAS E FORMALIZAÇÃO
Autores
GUILHERME BAUMGRATZ FIGUEIROA (Autor)
RODRIGO GERALDO RIBEIRO (Orientador)
Resumo
A teoria de tipos construtiva pode ser interpretada como uma linguagem de programação expressiva na qual tanto algoritmos quanto provas de correção sobre estes podem ser representadas. Uma limitação da teoria de tipos vista como uma linguagem de programação é que podemos definir apenas programas cuja terminação pode ser demonstrada utilizando algum critério sintático sobre a estrutura dos parâmetros do algoritmo em questão. Portanto, algoritmos que não são estruturalmente recursivos sobre seus parâmetros não podem ser diretamente definidos, uma vez que suas chamadas recursivas contêm argumentos que não atendem a restrições sintáticas para garantia de terminação. Diversas abordagens visam resolver este inconveniente utilizando predicados que expressam relações de ordem bem formadas entre parâmetros. Porém, a construção de tais relações e das respectivas provas de que estas são bem formadas não são simples, o que pode desmotivar o desenvolvedor a utilizar linguagens baseadas em teoria de tipos como Coq e Agda para o desenvolvimento de programas que são corretos por construção. Neste sentido, o presente projeto propõe uma metodologia alternativa baseada em mônadas livremente geradas e morfismos, para representação e construção automática de certas provas de terminação de funções. Na abordagem proposta, implementa-se o algoritmo usando uma mônada que codifica, sintaticamente, a estrutura recursiva da função. A semântica desta mônada é dada por morfismo desta para outra mônada que efetivamente executa a função definida. Os resultados preliminares mostram que esta abordagem é promissora, pois permite que diferentes morfismos sejam construídos para uma mesma definição permitindo maior flexibilidade para criar funções que usam recursão geral em linguagens funcionais como Agda e Coq.
Voltar Visualizar PDF