Detalhes do Documento

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2017.

Terminação é uma propriedade crítica para formalização de correção de programas. Verificar automaticamente terminação de um programa é conhecido como Problema da Parada e Turing provou que é um problema indecidível. Apesar disso, é possível construir algoritmos de semi decisão para verificar terminação, que respondem ‘sim’ se pode provar que o algoritmo para e ‘não sei’ caso contrário. Para construir esses algoritmos de semi decisão é necessário considerar diferentes noções de terminação, provando que são equivalentes. Neste trabalho, noções de terminação são formalizadas equivalentes para uma linguagem funcional de primeira ordem chamada PVS0 usando o assistente de prova Prototype Verification System. Essas noções são: as funções produzem uma saída, a árvore de derivação de chamados recursivos de funções tem tamanho finito (ambas as noções são chamadas terminação semântica), e os argumentos das funções decrescem para cada chamado recursivo (essa noção é chamada ranking function). As contribuições desse trabalho incluem a formalização de alguns lemas necessários para demonstrar equivalência entre noções de terminação semântica e ranking function, e como resultado principal a formalizações de indecidibilidade do Problema da Parada e Turing-Completude de PVS0.

Termination is a critical property for the formalization of programs correctness. Verifing automatically termination of a program for an input is known as Halting Problem and Turing proved that this is undecidable. However, it is possible to build semi decision algorithms for the verification of termination, that answer ‘yes’ if it is possible to prove that the algorithm halts, and ‘do not know’ otherwise. To construct these semi decision algorithms it is necessary to consider different notions of termination, proving that they are equivalent. In this work, notions of termination were formalized equivalent for a minimal functional first order language called PVS0 using the proof assistant Prototype Verification System. These notions are: the functions produces an output, the derivation tree of recursive calls of functions has a finite size (both these notions are called semantic termination), and the arguments of functions decreases for each recursive call (this notion is called ranking function). The contributions of this work includes formalization of lemma related with the equivalence between notions of semantic and ranking function termination, and the main results are the formalization of indecidability of Halting Problem and Turing-Completeness of PVS0.