Nominal commutative narrowing

Abstract

Modelagem e raciocínio equacional são onipresentes na Matemática e na Ciência da Computação. Técnicas de reescrita têm sido aplicadas com sucesso para formalizar e implementar inferência automatizada em estruturas matemáticas dedutivas. Apresentar teorias equacionais por meio da reescrita dá origem a um mecanismo para decidir a redução equacional da teoria sempre que o sistema de reescrita for terminante e confluente, ou seja, sempre que for convergente. Resolver problemas equacionais é um passo adiante que requer mais esforço do que apenas usar reescrita. De fato, “estreitar” problemas equacionais é uma técnica bem conhecida que adiciona à reescrita o poder necessário para buscar soluções; em outras palavras, adiciona o poder de buscar instâncias das variáveis que ocorrem em um problema equacional que “unifica” as equações. Por sua vez, a lógica nominal foi desenvolvida para contornar as inconveniências apresentadas quando as variáveis são instanciadas. A abordagem nominal usa átomos nominais em vez de variáveis para evitar a necessidade de renomeação de variáveis ao lidar com equações na abordagem notacional padrão. A sintaxe nominal também inclui permutações de átomos para distinguir algebricamente os átomos evitando colisões e capturas destes. Neste trabalho, estudamos a reescrita nominal módulo comutatividade. Desenvolvemos o método estreitamento nominal comutativo (nominal commutative narrowing) para lidar com o problema de unificação nominal módulo teorias equacionais que incluem comutatividade, o qual não é finitário dependendo da representação das soluções.