Lambda MicroEgg : e-graphe d'ordre supérieur avec motifs de Miller et substitution évitant la capture

Les e-graphes excellent en raisonnement équationnel mais opèrent traditionnellement sur des termes du premier ordre, ce qui rend la réécriture consciente des lieurs malaisée. Lambda MicroEgg de Philip Zucker étend microegg de Max Willsey avec des lieurs natifs, des motifs de Miller et une substitution évitant la capture.

L'idée d'ingénierie clé consiste à stocker les annotations de levage (profondeur de portée) dans un seul octet pris sur l'ID u32 de l'e-classe. Cela permet aux termes lambda alpha-équivalents de se hash-consolider en e-classes identiques — (@lam x (@lam y (+ x y))) et (@lam a (@lam b (+ a b))) deviennent le même e-nœud — tandis que les termes non alpha-équivalents mais liés par amincissement partagent une sous-structure plus profonde.

Les motifs de Miller {?a x y} restreignent les métavariables à ne s'appliquer qu'à des variables liées distinctes dans la portée, fournissant un fragment décidable de l'appariement d'ordre supérieur. Le système prend également en charge l'application d'ordre supérieur sans lambda via la notation [] qui auto-currifie en HOApp(Id,Id), évitant l'encodage verbeux (app (app f x) y). La substitution bêta devient une simple règle de réécriture.

Les performances se situent dans un facteur 2 à 3 de la bibliothèque egg de base sur les benchmarks de saturation AC (262k unions en ~1,5 s contre ~0,6 s pour egg), l'octet de levage ajoutant une surcharge négligeable lorsqu'il n'est pas utilisé.

Prendre un octet sur les ID u32 des e-classes pour stocker les annotations de levage, permettant le hash-consing alpha-équivalent et la substitution évitant la capture sans surcoût mémoire supplémentaire

Les e-graphes du premier ordre nécessitent des encodages De Bruijn verbeux ou une machinerie de substitution explicite pour les lieurs

Les motifs de Miller donnent un fragment décidable et bien comporté de l'appariement d'ordre supérieur

Prendre un octet sur les ID existants évite la surcharge d'allocation pour les annotations de levage

Le hash-consing alpha-équivalent émerge naturellement de la représentation par levage

Un seul octet pris sur les ID existants peut encoder la discipline de portée, transformant un e-graphe du premier ordre en un e-graphe d'ordre supérieur avec une surcharge minimale.

L'implémentation est open-source à github.com/philzook58/lambda-microegg avec une démo WASM. L'auteur prévoit d'ajouter la journalisation des preuves, des e-nœuds éphémères pour davantage de variables, et une intégration avec la complétion de Buchberger/multiensemble/chaîne/semi-anneau.