Unification of Deterministic Higher-Order Patterns (Full Version)

Resumo Técnico: Unificação de Padrões de Ordem Superior Determinísticos

Declaração do Problema
Este artigo aborda o problema de unificação para uma classe específica de termos $\lambda$ simplesmente tipados conhecida como Padrões de Ordem Superior Determinísticos (DHPs). Enquanto a unificação de ordem superior padrão é indecidível e infinitária (potencialmente produzindo infinitos unificadores incomparáveis), e a unificação de primeira ordem é decidível e unitária, os DHPs ocupam uma posição intermediária única. Os DHPs, introduzidos por Yokoyama et al., são definidos de modo que seu problema de correspondência (matching) seja determinístico (existe no máximo uma substituição). No entanto, ao contrário dos padrões de ordem superior de Miller ou da Unificação de Funções como Construtores (FCU) de Libal e Miller, o problema de unificação para DHPs não é unitário; conjuntos completos mínimos de unificadores (MCSUs) podem ser infinitos. O desafio central é desenvolver um procedimento de unificação correto e completo para esta classe que lide com a natureza potencialmente infinitária do espaço de soluções, mantendo as propriedades estruturais que tornam a correspondência determinística.

Metodologia
Os autores propõem um sistema de inferência correto e completo para calcular conjuntos completos de unificadores (CSUs) para DHPs. A metodologia baseia-se nos seguintes fundamentos técnicos:

1. Representação de Termos: O procedimento opera sobre termos $\lambda$ simplesmente tipados na forma normal longa $\beta\eta$, utilizando uma formulação livre de $\beta\eta$ para simplificar a aplicação de substituições e evitar a redução $\beta$ explícita durante as provas.
2. Definição de DHPs: Um termo é um DHP se, para cada subtermo da forma $x_n.y(t_m)$ onde $y$ é uma variável livre:
   • Cada argumento $t_i$ contém pelo menos uma variável ligada de $x_n$ (garantindo correspondência determinística).
   • Os argumentos são "expandidos" (suas formas normais $\eta$ não são abstrações).
   • Os argumentos são distintos sob a relação de "subtermo expandido" (restrição local), impedindo que um argumento seja um subtermo de ordem superior de outro.
3. Sistema de Inferência: O procedimento de unificação é um sistema de inferência não determinístico operando sobre pares de DHPs. Ele estende o quadro da unificação completa de ordem superior (Huet), mas introduz otimizações específicas para DHPs:
   • Resolução Flex-Flex: Ao contrário da unificação completa de ordem superior, que exige ligações parciais para pares flex-flex (pares onde ambas as cabeças são variáveis livres), o sistema DHP resolve estes de uma maneira "mais geral". As regras (ff=) e (ff̸=) constroem unificadores mantendo apenas argumentos iguais ou combinando argumentos sem introduzir variáveis livres, respectivamente.
   • Projeção e Imitação: O sistema utiliza regras de imitação e projeção, mas restringe-as para garantir que os termos resultantes permaneçam dentro da classe DHP. Notavelmente, projeções em DHPs devem resultar em cabeças que sejam símbolos de função ou variáveis ligadas, e não variáveis livres.
   • Estratégia para Minimalidade: Para garantir que o conjunto calculado de unificadores seja mínimo (ortogonal), os autores definem estratégias que priorizam as regras (rem) e (var) e calculam nomes de variáveis frescas de forma determinística.

Principais Contribuições e Resultados

• Correção e Completude: O artigo prova que o sistema de inferência é correto (derivações bem-sucedidas produzem unificadores válidos) e completo (para qualquer unificador $\delta$, existe uma derivação produzindo um unificador $\theta$ tal que $\theta$ é mais geral que $\delta$).
• Minimalidade: Os autores demonstram que, sob estratégias específicas (localmente ótimas e determinísticas para variáveis frescas), o sistema de inferência produz um Conjunto Completo Mínimo de Unificadores (MCSU). Isso é significativo porque, na unificação de ordem superior geral, conjuntos mínimos não são garantidos de serem ortogonais ou finitos.
• Espaços de Solução Infinitos: O artigo fornece exemplos (por exemplo, Exemplos 10 e 13) mostrando que os MCSUs para DHPs podem ser infinitos. Consequentemente, o sistema de inferência não é garantido de terminar, e a decidibilidade do problema de unificação DHP permanece uma questão em aberto.
• Generalização da FCU: O método generaliza a FCU de Libal e Miller ao remover a "restrição global" (que impede que um argumento de variável livre seja um subtermo de qualquer argumento de variável em todo o problema). Ao eliminar isso, o sistema lida com um conjunto estritamente maior de termos, mas perde a propriedade unitária da FCU.

Significado e Alegações
Os autores posicionam este trabalho como uma investigação necessária sobre uma classe de termos onde a correspondência permanece determinística, mas a unificação perde a propriedade unitária, saltando imediatamente para problemas infinitários. O significado reside em:

1. Sub-rotinas Práticas: Os DHPs são definidos como uma classe de termos, e não como uma restrição dependente do problema (como a restrição global da FCU). Isso torna os DHPs mais fáceis de usar como sub-rotina em prova automática de teoremas ou programação lógica, pois não é necessário verificar restrições globais para determinar se um termo está no escopo.
2. Insight Teórico: O trabalho esclarece a fronteira entre correspondência determinística e unificação unitária, mostrando que a transição da unificação unitária para a infinitária pode ocorrer sem passar por uma etapa finitária.
3. Simulação da FCU: Os autores alegam que sua abordagem pode simular a FCU; se um problema FCU tiver um unificador mais geral, o sistema de inferência o encontrará através de uma derivação finita e determinística.

O artigo conclui observando que, embora o sistema de inferência seja finitamente ramificado, sua não-terminação impede uma prova de decidibilidade. Trabalhos futuros exigiriam representações engenhosas de conjuntos infinitos de unificadores (por exemplo, usando gramáticas regulares) para lidar efetivamente com os cenários de ramificação infinita.