Lambda MicroEgg: e-graph de ordem superior com padrões de Miller e substituição que evita captura

Os e-graphs se destacam no raciocínio equacional, mas tradicionalmente operam sobre termos de primeira ordem, o que torna a reescrita sensível a binders complicada. O Lambda MicroEgg de Philip Zucker estende o microegg de Max Willsey com binders nativos, padrões de Miller e substituição que evita captura.

A principal percepção de engenharia é armazenar anotações de lifting (profundidade de escopo) em um único byte tomado emprestado do ID de e-class u32. Isso permite que termos lambda alfa-equivalentes sejam hash-consed em e-classes idênticas — (@lam x (@lam y (+ x y))) e (@lam a (@lam b (+ a b))) tornam-se o mesmo e-nó — enquanto termos não alfa-equivalentes, mas relacionados por thinning, compartilham subestrutura mais profunda.

Os padrões de Miller {?a x y} restringem as metavariáveis a se aplicarem apenas a variáveis ligadas distintas no escopo, fornecendo um fragmento decidível de casamento de ordem superior. O sistema também suporta aplicação de ordem superior sem lambda por meio da notação [], que faz auto-currying para HOApp(Id,Id), evitando a codificação verbosa (app (app f x) y). A substituição beta torna-se uma regra de reescrita simples.

O desempenho fica dentro de 2 a 3 vezes o da biblioteca egg base em benchmarks de saturação AC (262 mil uniões em ~1,5 s contra ~0,6 s do egg), com o byte de lifting adicionando sobrecarga desprezível quando não utilizado.

Tomar emprestado um byte dos IDs de e-class u32 para armazenar anotações de lifting, permitindo hash-consing alfa-equivalente e substituição que evita captura sem sobrecarga extra de memória

E-graphs de primeira ordem exigem codificações verbosas de De Bruijn ou maquinário explícito de substituição para binders

Os padrões de Miller fornecem um fragmento decidível e bem comportado de casamento de ordem superior

Tomar emprestado um byte dos IDs existentes evita sobrecarga de alocação para anotações de lifting

O hash-consing alfa-equivalente emerge naturalmente da representação de lifting

Um único byte tomado emprestado dos IDs existentes pode codificar a disciplina de escopo, transformando um e-graph de primeira ordem em um de ordem superior com sobrecarga mínima.

A implementação é de código aberto em github.com/philzook58/lambda-microegg, com uma demonstração em WASM. O autor planeja adicionar registro de provas, e-nós efêmeros para mais variáveis e integração com completação de Buchberger/multiconjunto/string/semianel.