Resumo Técnico: E-Graphs Categóricos para Cálculo Lambda

Declaração do Problema

A saturação de igualdade é uma técnica poderosa para otimização de programas e raciocínio, utilizando classes de equivalência de termos (e-graphs) para explorar um espaço de regras de reescrita de forma não destrutiva. No entanto, as e-graphs tradicionais carecem de suporte nativo para ligação de variáveis (variable binding), uma característica fundamental de linguagens de programação funcional baseadas no $\lambda$-cálculo.

As abordagens existentes para incorporar ligações enfrentam desafios significativos:

1. Representações Textuais: Na sintaxe textual padrão, termos $\alpha$-equivalentes são distintos e não podem ser compartilhados. Embora os índices de De Bruijn identifiquem a $\alpha$-equivalência sintaticamente, os índices dependem do escopo da variável, impedindo o compartilhamento de termos que diferem apenas na atribuição de índices (ex: $\lambda f. f((\lambda x. fx)2)$).
2. Substituição Explícita: Adicionar nós de substituição explícita (ex: $t[x/u]$) para lidar com ligações introduz "burocracia". Isso requer nós adicionais e regras de reescrita para gerenciar permutações de substituições não interativas (equivalência gráfica), sobrecarregando o espaço de estados com overhead administrativo em vez de reescrita específica do domínio.
3. E-Graphs com Slots (Slotted E-Graphs): Trabalhos recentes (Schneider et al.) introduzem "e-graphs com slots" onde variáveis são dados de primeira classe. Embora eficaz, esta abordagem depende de técnicas nominais aplicáveis a linguagens arbitrárias (como o $\pi$-cálculo), mas pode não aproveitar as propriedades estruturais específicas do $\lambda$-cálculo tão eficientemente quanto um modelo semântico dedicado.

O problema central é a falta de uma estrutura de dados categórica nativa para e-graphs que suporte ligação de variáveis, permitindo a saturação de igualdade eficiente em $\lambda$-cálculos sem o overhead de nós de substituição explícita ou regras de renomeação complexas.

Metodologia

Os autores propõem uma solução fundamentada em semântica categórica, estendendo a interpretação de e-graphs como diagramas de cordas (string diagrams).

1. Estrutura Categórica

O artigo baseia-se no trabalho de Tiurin et al., que modelou e-graphs (sem ligação) como morfismos em categorias SLat-enriched simétricas monoidais (categorias SLat-enriched).

• Enriquecimento SLat: Os conjuntos Hom são semilattices, onde a operação de junção ($+$) representa a equivalência de subtermos (classes de e-graph).
• Estrutura Monoidal Fechada: Para lidar com a ligação de variáveis, os autores estendem a categoria para ser monoidal fechada. Isso introduz o objeto de hom interno ($A \multimap B$) e a adjunção $- \otimes B \dashv B \multimap -$.
• Diagramas de Cordas: Os termos são representados como diagramas de cordas. A ligação é modelada via "caixas arredondadas" (representando abstração $\lambda$), e as classes de equivalência são modeladas via "caixas tracejadas" (representando a junção do semilattice).

2. Representação Combinatória: E-Hipergrafos Fechados

Para fornecer uma estrutura de dados concreta, os autores definem e-hipergrafos fechados. Estes são hipergrafos hierárquicos que codificam:

• Hiperarestas: Representando operações (geradores).
• Arestas Hierárquicas: Dois tipos de estruturas aninhadas:
  • E-classes (Caixas tracejadas): Representando classes de equivalência de subtermos.
  • Caixas de Abstração (Caixas arredondadas): Representando abstrações $\lambda$.
• Interfaces: A estrutura utiliza cospans estendidos para gerenciar entradas e saídas, distinguindo entre interfaces externas (topo) e interfaces estritamente internas (aninhadas dentro de caixas).

3. Sistema de Reescrita

Os autores definem um sistema de reescrita Double-Pushout with Interfaces (DPOI) para e-hipergrafos fechados.

• Regras de Reescrita: Definidas como spans de cospans estendidos.
• Complementos de Fronteira: Uma definição especializada do "buraco" deixado após a remoção de um match é introduzida para lidar com a natureza hierárquica dos grafos. Isso garante que, quando um subgrafo é removido, as interfaces internas sejam ajustadas corretamente (ex: remover um termo aninhado atualiza a interface estritamente interna do pai).
• Correção e Completude: O artigo estabelece que a reescrita DPO nesses e-hipergrafos fechados é correta e completa em relação à reescrita de termos $\Sigma^+$-fechados modulo as equações da categoria monoidal simétrica SLat e a lei de distributividade da estrutura fechada.

Contribuições Principais

1. Extensão Categórica: A construção de uma forma de e-graphs que suporta ligação ao estender o domínio categórico de categorias simétricas monoidais SLat livres para categorias simétricas monoidais SLat fechadas livres.
2. E-Hipergrafos Fechados: A definição de uma representação combinatória concreta (e-hipergrafos fechados) que naturalmente absorve as equações da estrutura monoidal simétrica e da estrutura fechada (ligação).
3. Reescrita DPOI para Ligação: A formulação de um sistema de reescrita DPOI para estas estruturas, provando sua correção e completude em relação à reescrita de termos na correspondente teoria categórica.
4. Comparação com Slotted E-Graphs: Uma comparação teórica demonstrando que, enquanto slotted e-graphs oferecem ligação genérica via técnicas nominais, a abordagem categórica incorpora a ligação no próprio sistema de linguagem interna do modelo, potencialmente oferecendo vantagens para otimizações específicas do $\lambda$-cálculo.

Resultados

• Equivalência de Reescrita: O artigo prova que a reescrita de termos $\Sigma^+$-fechados é equivalente à reescrita DPO de e-hipergrafos fechados.
• Tratamento de Equivalência Gráfica: A abordagem lida naturalmente com "equivalência gráfica" (permutações de substituições não interativas) sem exigir nós de substituição explícitos. No modelo categórico, a substituição explícita é modelada como composição, e as leis estruturais da categoria absorvem as equivalências necessárias.
• Estudo de Caso ($\lambda_{lsub}$): Os autores aplicam a teoria ao cálculo de substituição linear ($\lambda_{lsub}$). Eles demonstram que termos com substituições explícitas (ex: let-bindings) podem ser representados diretamente como diagramas de cordas.
  • Ao contrário das e-graphs convencionais que exigem nós explícitos para substituição e regras de reescrita para lidar com sua permutação, o modelo categórico trata estes como propriedades estruturais do diagrama.
  • O artigo mostra que programas semanticamente equivalentes (ex: reordenar let-bindings) mapeiam para o mesmo diagrama de cordas, permitindo que a saturação de igualdade opere em uma representação normalizada.

Significância e Alegações

O artigo afirma fornecer uma semântica categórica fundamental para e-graphs com ligação, uma área anteriormente subdesenvolvida.

• Justificativa Teórica: Oferece uma justificativa rigorosa para as congruências mantidas pelas e-graphs com ligação, fundamentando-as nas propriedades das categorias simétricas monoidais fechadas SLat.
• Potencial de Eficiência: Ao absorver equações estruturais (como associatividade, comutatividade e permutações de substituição) na sintaxe gráfica e na categoria subjacente, a abordagem visa reduzir a "burocracia" no espaço de estado da saturação de igualdade. Isso contrasta com abordagens que tratam estas como regras de reescrita explícitas.
• Escopo: Os autores declaram explicitamente que sua abordagem é especializada para o $\lambda$-cálculo e variações do mesmo, aproveitando a linguagem interna metateórica do modelo categórico. Eles reconhecem que slotted e-graphs podem ser mais flexíveis para linguagens arbitrárias com ligadores (como o $\pi$-cálculo), mas argumentam que seu método é superior para otimizações específicas do $\lambda$-cálculo.

O trabalho não apresenta uma implementação de software completa ou benchmarks empíricos neste artigo, mas posiciona a representação de e-hipergrafos fechados como uma base viável para construir "e-graphs para reescrita de diagramas de cordas" em trabalhos futuros.