lambda-microegg: un egraph que entiende binders y patrones de Miller

Philip Zucker ha publicado lambda-microegg, un egraph que sabe con qué variables está trabajando. En lugar de tratar los enlaces de un término como texto plano, arrastra binders con alcance definido y reescribe sin romper la correspondencia entre una variable ligada y sus usos. El frontend es a base de expresiones S y hay una demo compilada a wasm para probarlo sin montar nada.

El punto de partida es microegg, del que hereda la estructura general. Encima, Zucker ha metido binders nativos, patrones de Miller de orden superior y sustitución que evita capturas en el lado derecho de las reglas. En la sintaxis, @ marca una forma de ligadura unaria: (@ sum x (...)) es el sumatorio sobre x. La aplicación de orden superior se escribe con corchetes, [f x], que currifican solos y se codifican internamente con un constructor propio, distinto del de primer orden. Escribir (app (app f x) y) era engorroso, así que el atajo viene integrado.

Miller patterns

Un patrón de Miller {?a x y} dice que el metavariable solo puede aplicarse a variables ligadas distintas entre sí, nunca a términos arbitrarios. Dentro del patrón, ?a puede contener las ligadas x e y, no una z que ande por ahí, y sí las variables libres que estén en el ámbito de la parte alta. Es la zona decidible del matching de orden superior, y es justo lo que hace falta para modelar la sustitución beta sobre un término con @lam: la regla que reescribe [( @ lam x { ? body x }) ? e] a { ? body ? e }, aplicada a [( @ lam x x ) 42], devuelve 42. No es magia, pero convierte el egraph en algo usable con sintaxis con alcance real.

Rendimiento

En una saturación AC-10 de manual, el egraph acabó con 262.291 uniones, 1.023 clases y 57.012 e-nodos: 350 ms de matching, cerca de un segundo de aplicación y 152 ms de reconstrucción. Si se cambia la notación de primer orden por los corchetes de orden superior, el mismo problema sube a 262.143 uniones, 2.046 clases y 58.035 e-nodos, con 685 ms de matching y 1,29 s de aplicación. Zucker compara con egg, que para algo parecido tarda unos 0,6 s en su equipo: reconoce que esto va más lento, aunque no por un orden de magnitud.

El detalle que más pesa de cara a operarlo es que las liftings se guardan en un byte robado al u32 del Id, así que si no se usan apenas cuestan. El fragmento lambda-free de orden superior ya tiene tratamiento específico en probadores como E y Zipperposition; aquí la gracia es tenerlo dentro de un egraph con binders de verdad. Queda por ver si los patrones de orden superior se optimizan, algo que el propio autor apunta como posible vía precalculando los ids ground dentro del patrón. Por ahora es una herramienta de investigación, sin más banco de pruebas que los ejemplos de la entrada.