Unificação, confluência e tipos com interseção para sistemas de reescrita nominal

Abstract

Sistemas nominais são uma abordagem alternativa para o tratamento de variáveis em sistemas computacionais, onde a reescrita de primeira ordem é generalizada através do suporte para especificação de ligação de variáveis e de _-equivalência, fazendo uso do conceito de freshness e da troca bijetiva de nomes (swapping). Teoremas bem conhecidos em reescrita de primeira ordem podem ser adaptados a fim de serem adicionalmente válidos em reescrita nominal. Nesta tese, nós analisamos sob que condições a confluência de sistemas de reescrita e o Critério dos Pares Críticos são válidos para a reescrita nominal, assim como para a reescrita nominal fechada (que é uma noção de reescrita mais eficiente nesse contexto). As condições definidas aqui são de fácil checagem através de um algoritmo de unificação nominal. A unificação nominal foi inicialmente estudada por Urban, Pitts e Gabbay e formalizada por Urban no assistente de prova Isabelle/HOL. Neste trabalho, são também apresentadas uma especificação nova de unificação nominal na linguagem do PVS e uma formalização da sua terminação, correção e completude. Em nossa especificação, ao invés de aplicar regras de simplificação a condições restritivas de unificação e freshness, soluções para um problema de unificação são construídas recursivamente através de uma especificação funcional direta, obtendo uma formalização que é mais próxima a implementações algorítmicas. Esta formalização é o passo inicial com vistas a ter mais resultados formalizados sobre reescrita nominal em PVS, onde um forte arcabouço de sistemas de reescrita de termos já é disponibilizado. Ademais, um sistema de tipos com interseção para termos nominais é apresentado. O sistema de tipos presente possui a importante propriedade de redução do sujeito para uma noção especializada de reescrita nominal tipada, o que significa que a tipabilidade no sistema é coerente com execuções computacionais.