Verificação das propriedades computacionais de um modelo funcional de primeira-ordem

Abstract

Este trabalho descreve a mecanização de propriedades computacionais de um modelo funcional que tem sido aplicado para automatizar o raciocínio sobre a terminação de programas. A formalização foi desenvolvida no assistente de provas de lógica de ordem superior, chamado Prototype Verification System (PVS). O modelo de linguagem foi projetado para imitar o fragmento de primeira ordem de especificações funcionais e é chamado PVS0. Foram considerados dois modelos computacionais: o primeiro modelo especifica um programa funcional por meio de uma única função (modelo single-function PVS0, ou SF-PVS0), e o segundo modelo permite a especificação simultânea de múltiplas funções (modelo multiple-function PVS0, ou MF-PVS0). A semântica operacional da recursão na especificação do modelo SF-PVS0suporta a recursão sobre o programa completo. Por outro lado, em programas MF-PVS0, as chamadas funcionais são permitidas para todas as funções especificadas no programa. Este trabalho tem como objetivo certificar matematicamente a robustez dos modelos PVS0 como modelos computacionais universais. Para isso, propriedades cruciais e teoremas foram formalizados, incluindo Turing Completude, a indecidibilidade do Problema da Parada, o teorema da recursão, o teorema de Rice e o teorema do Ponto Fixo. Além disso, o trabalho discute avanços na indecidibilidade do Problema da Palavra e do Problema da Correspondência de Post. A indecidibilidade do Problema da Parada foi formalizada considerando a avaliação semântica de programas PVS0 que foram aplicados na verificação da terminação de especificações em PVS. A equivalência entre a avaliação funcional e predicativa de operadores foi fundamental para esse objetivo. Além disso, a composicionalidade de programas MF-PVS0, habilitada diretamente pela possibilidade de chamar diferentes funções, torna fácil a formalização da Turing Completude. Portanto, enriquecer o modelo foi uma decisão de design importante para simplificar a mecanização dessa propriedade e dos teoremas mencionados acima.