Rumo à unificação nominal AC

Abstract

O paradigma nominal estende a sintaxe de primeira ordem e representa adequadamente o conceito de variáveis ligadas. Para trabalhar com esse vantajoso paradigma faz-se necessário adaptar noções de primeira ordem a ele, como unificação e matching. Esta tese é sobre unificação e matching no paradigma nominal na presença de uma teoria equacional E e sobre nosso trabalho em progresso em AC-unificação nominal. Inicialmente, generalizamos e formalizamos um algoritmo de C-unificação nominal para realizar matching e equality-checking, através da adição de um parâmetro X para lidar com variáveis protegidas. A formalização foi usada para testar uma implementação manual em Python do algoritmo. Em seguida, fornecemos a primeira formalização de um algoritmo de ACunificação em primeira ordem. Escolhemos formalizar o algoritmo seminal de Stickel e na prova de terminação usamos uma intrincada (mas devidamente motivada) medida lexicográfica, baseada no trabalho de Fages. Depois disso, adaptamos este algoritmo para obter o primeiro algoritmo para AC-matching em nominal e verificamos que o algoritmo termina e é correto e completo. Assim como em C-unificação nominal, usamos um parâmetro X para as variáveis protegidas, o que nos permitiu obter um AC-equality-checker como corolário. As 3 formalizações descritas foram feitas no assistente de provas PVS e integram a NASALib, o principal repositório de formalizações do PVS. Para cada uma dessas formalizações descrevemos a estrutura e tamanho dos arquivos que compõem a formalização. Visando obter um algoritmo de AC-unificação nominal, mostramos que o problema tem duas questões interessantes associadas a ele: gerar as soluções para π · X ≈? X e demonstrar terminação. Para a primeira questão, propomos um procedimento não determinístico de enumeração e exemplificamos como este calcula soluções não triviais. Para a segunda questão demonstramos como o problema f(X, W) ≈? f(π · X, π · Y ) gera um loop e provamos que é suficiente “entrar no loop” uma quantidade limitada de vezes, onde esse limite depende da ordem da permutação π. Acreditamos que a teoria desenvolvida será útil para a formulação de um algoritmo de AC-unificação nominal.