On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS

Abstract

Embora indecidível, terminação é uma propriedade muito importante relacionada à cor- reção de objetos computacionais. Ela garante que para cada entrada, não haverá execução infinita, ou seja, a execução deve parar e fornecer algum resultado. Esta propriedade per- mite, por exemplo, raciocinar sobre a correção de programas, uma vez que garantir que

alguma propriedade seja válida para cada saída depende da obtenção de uma saída a ser verificada sempre que uma entrada for fornecida. Ao longo dos anos, várias estratégias de semidecisão foram usadas para abordar esse problema e raciocinar sobre ele. No contexto

de Programas Funcionais (FPs), por exemplo, a análise pode ser feita por meio dos Gráfi- cos de Contexto de Chamada, e no contexto de Sistemas de Reescrita de Termos (TRSs),

podem ser usados Pares Dependentes.

Este trabalho formaliza o Critério de Terminação por Pares Dependentes (Mais Inter- nos), um critério muito conhecido para análise de terminação de TRSs, no assistente de

prova PVS. PVS é um assistente de prova com uma linguagem de especificação funcional que permite lógica de ordem superior e realiza provas seguindo o Cálculo de Sequentes de Gentzen. Também são apresentados vários Critérios de terminação formalizados para FPs em uma linguagem simplificada que modela especificações em PVS (chamada PVS0) e a formalização da equivalência entre eles, permitindo automação de provas de terminação de especificações de funções recursivas de primeira ordem em PVS. O trabalho também discute a possibilidade de navegar entre os critérios de terminação para TRSs e FPs com o objetivo de aprimorar a automação para verificar terminação.