Lambda MicroEgg: Miller 패턴과 캡처 회피 치환을 갖춘 HO e-graph

E-graph는 등식 추론에 탁월하지만 전통적으로 일차항 위에서 동작하므로 바인더를 인식하는 재작성이 어색하다. Philip Zucker의 Lambda MicroEgg는 Max Willsey의 microegg를 네이티브 바인더, Miller 패턴, 캡처 회피 치환으로 확장한다.

핵심 엔지니어링 통찰은 리프팅 주석(스코프 깊이)을 u32 e-class ID에서 빌려온 단일 바이트에 저장하는 것이다. 이로써 알파 동등한 람다 항이 동일한 e-class로 해시-콘스될 수 있다 — (@lam x (@lam y (+ x y)))와 (@lam a (@lam b (+ a b)))는 같은 e-node가 된다 — 반면 알파 동등하지 않지만 thinning 관련된 항들은 더 깊은 하위 구조를 공유한다.

Miller 패턴 {?a x y}는 메타변수가 스코프 내의 서로 다른 바인딩된 변수에만 적용되도록 제한하여, 고차 매칭의 결정 가능한 단편을 제공한다. 이 시스템은 또한 [] 표기를 통한 람다 없는 고차 적용을 지원하며, 이는 자동으로 HOApp(Id,Id)로 커리되어 장황한 (app (app f x) y) 인코딩을 피한다. 베타 치환은 단순한 재작성 규칙이 된다.

성능은 AC 포화 벤치마크에서 기본 egg 라이브러리의 2-3배 이내이다(약 1.5초에 262k 유니온 vs egg의 약 0.6초). 리프팅 바이트는 사용되지 않을 때 무시할 수 있는 오버헤드만 추가한다.

u32 e-class ID에서 한 바이트를 빌려 리프팅 주석을 저장하여, 추가 메모리 오버헤드 없이 알파 동등 해시-콘싱과 캡처 회피 치환을 가능하게 했다

일차 e-graph는 바인더를 위해 장황한 De Bruijn 인코딩이나 명시적 치환 기계를 필요로 한다

Miller 패턴은 고차 매칭의 결정 가능하고 잘 동작하는 단편을 제공한다

기존 ID에서 바이트를 빌려오면 리프팅 주석을 위한 할당 오버헤드를 피할 수 있다

알파 동등 해시-콘싱은 리프팅 표현에서 자연스럽게 나타난다

기존 ID에서 빌려온 단일 바이트가 스코프 규율을 인코딩하여, 일차 e-graph를 최소한의 오버헤드로 고차 e-graph로 바꿀 수 있다.

구현은 github.com/philzook58/lambda-microegg에서 WASM 데모와 함께 오픈소스로 공개되어 있다. 저자는 증명 로깅, 더 많은 변수를 위한 임시 enode, 그리고 Buchberger/멀티셋/문자열/세미링 완성과의 통합을 추가할 계획이다.