Lambda MicroEgg — 스코프와 알파 동치를 이해하는 바인더 지원 e-graph

AI 요약

Philip Zucker가 공개한 Lambda MicroEgg는 잘 정의된 스코프를 가진 알파 인식 바인더를 지원하는 e-graph 도구입니다. 기존의 lifting 기반 e-graph 아이디어를 S-expression 프론트엔드에 연결한 구현이며, Max의 microegg에서 큰 영향을 받았습니다. 저장소와 WebAssembly 데모를 함께 제공하고, 일반적인 일차식 재작성뿐 아니라 람다식, 고차 애플리케이션, Miller 패턴, 캡처 회피 치환을 하나의 작은 시스템 안에서 다루는 것을 목표로 합니다.

■ 바인더를 포함한 재작성

첫 번째 예제는 합 기호를 단항 바인더로 표현합니다. `@sum`이 변수 하나를 바인딩하고, `{?a x}`는 바인딩된 변수 `x`를 인자로 받는 Miller 패턴입니다. 입력에는 `x`와 `y`를 차례로 바인딩한 중첩 합이 들어가며, 재작성 규칙은 합 안의 상수 인자를 밖으로 인수분해하고, 상수만 남은 합을 `N`으로 치환하며, 곱셈의 교환법칙을 적용합니다. 실행 결과는 5라운드, 17 unions, 9 classes, 22 e-nodes였고, 매칭에 21.72마이크로초, 적용에 14.991마이크로초, rebuild에 19.347마이크로초가 걸렸습니다. 마지막 `guard` 조건도 통과해 원래 식이 `2 * (N * (sum x x))`와 같다는 사실을 확인합니다.

기본적인 성능 비교를 위해 1부터 10까지 중첩된 덧셈에 교환법칙과 결합법칙을 적용하는 AC-10 포화도 실험도 제시합니다. 100라운드를 실행했지만 실제로는 9라운드에서 262,291 unions, 1,023 classes, 57,012 e-nodes에 도달했습니다. 매칭은 350.089112밀리초, 적용은 999.980826밀리초, rebuild는 152.433662밀리초였습니다. 저자는 비슷한 실험에서 `egg`가 약 0.6초였다고 설명하며, Lambda MicroEgg가 더 느리지만 극단적으로 느린 수준은 아니라고 평가합니다. lifting 정보를 `u32 Id`에서 가져온 1바이트에 저장하므로, 해당 기능을 사용하지 않는 일차식 코드에서는 오버헤드가 크지 않기를 기대한다고 덧붙입니다.

■ 일차식과 고차 애플리케이션

일반적인 일차식 표현은 `FOApp(Symbol, Vec<Id>)`처럼 함수와 인자 목록을 분리합니다. 반면 고차식에서는 `HOApp(Id, Id)` 형태의 이항 애플리케이션이 자연스럽습니다. Lambda MicroEgg는 후자를 지원하면서도, 사용자가 매번 `app (app f x) y`처럼 작성하지 않도록 대괄호 표기 `[]`를 추가했습니다. 이 표기는 애플리케이션을 자동으로 커링합니다.

예제에서는 `[map [comp f g] [cons 3 nil]]`에 대해 함수 합성의 정의, `map`과 `cons`의 전개, 빈 리스트 처리 규칙을 적용합니다. `[ [comp f g] 3 ]`이 `[f [g 3]]`과 같다는 `guard`가 통과하며, 2라운드에서 4 unions, 16 classes, 19 e-nodes를 만들었습니다. 다만 같은 AC 포화 예제를 `()` 기반 일차식 대신 `[]` 기반 고차식으로 표현하면 비용이 증가합니다. 고차 버전에서는 9라운드 동안 262,143 unions, 2,046 classes, 58,035 e-nodes가 만들어졌고, 매칭 685.163722밀리초, 적용 1.287551403초, rebuild 150.952363밀리초가 기록됐습니다. 저자는 패턴 안의 ground id를 미리 계산하는 최적화로 이 비용을 줄일 수 있을지 검토하고 있습니다.

■ Miller 패턴과 베타 치환

Miller 패턴은 스코프가 있는 구문에서 메타변수가 어떤 변수를 사용할 수 있는지 제한하는 고차 패턴입니다. 예를 들어 `{?a x y}`에서 `?a`는 현재 스코프의 자유변수를 사용할 수 있고, 패턴 안에서 허용된 바인딩 변수 `x`, `y`도 사용할 수 있지만, 스코프에 존재하더라도 허용 목록에 없는 `z`는 사용할 수 없습니다. 메타변수는 임의의 항이 아니라 서로 다른 바인딩 변수들에 적용되어야 하므로, 고차 매칭과 통일 가운데 결정 가능한 영역을 제공합니다.

이 기능으로 람다식의 베타 치환도 재작성 규칙으로 표현할 수 있습니다. `(@lam x {?body x})`가 어떤 본문을 나타내고, 여기에 인자 `?e`가 적용되면 `{?body ?e}`로 치환하는 규칙입니다. `(@lam x x)`에 `42`를 적용한 예제는 한 라운드, 1 union, 3 classes, 4 e-nodes를 거쳐 `42`를 추출합니다. 우변에서 수행되는 치환은 캡처 회피 방식으로 동작하며, 저자는 이 과정이 e-graph를 재귀적으로 복사하는 것과 비슷하거나, 여러 항을 추출하고 치환한 뒤 다시 삽입하는 것과 동등하다고 설명합니다.

■ 컨텍스트, lifting, 알파 동치

이 구현에서 중요한 개념은 패턴 변수의 치환이 단순한 항 하나가 아니라 특정 컨텍스트 안의 항이라는 점입니다. `(@lam x (@lam y (+ 3 y)))`에서 `(+ ?a ?b)`를 매칭하면 바깥 컨텍스트 크기 1에서 `?a = 3`, `?b = $0`을 얻습니다. 반면 `(@lam y (+ ?a {?b y}))`를 매칭하면 전체 치환은 빈 컨텍스트에 놓이고, `?b` 자체가 추가 바인딩 변수를 받는 `ctx1`의 항이 됩니다. 따라서 컨텍스트가 없는 항은 별도의 본질적 종류가 아니라 `ctx0`의 축약 표현으로 볼 수 있으며, 상수 역시 0-arity 함수의 축약으로 이해할 수 있다고 설명합니다.

알파 동치인 두 람다식은 같은 해시 컨싱된 구조를 공유합니다. 예를 들어 변수 이름만 다른 `(@lam x (@lam y (+ x y)))`와 `(@lam a (@lam b (+ a b)))`는 같은 e-node 구조로 합쳐집니다. 내부적으로는 변수의 위치와 lifting 정보를 표시하는 `l_10`, `l_01` 같은 주석이 사용됩니다. 더 흥미로운 사례로, 깊은 스코프에 있는 변수를 가리키는 두 항은 단순한 de Bruijn 인덱스라면 서로 다른 인덱스를 갖지만, 실제로 사용되지 않는 중간 바인딩을 건너뛰는 thinning 구조를 통해 상당한 메모리 공유를 얻을 수 있습니다. 즉, 현재 스코프 전체를 인덱스에 포함하기보다 실제로 사용되는 변수에 필요한 해시 컨싱만 지불하는 방식입니다.

lifting 또는 thinning 정보는 현재 `u32 Id`에서 1바이트를 떼어 저장합니다. sentinel `1`로 thinning 비트벡터의 시작점을 표시하는 인코딩을 사용하며, 이 방식으로 컨텍스트 안의 최대 7개 변수를 표현할 수 있습니다. 저자는 더 넓은 thinning을 위해 전체 별도 `u32`를 사용해 64비트 fat id를 만들거나, 큰 id만 별도 arena에 저장하는 ephemeral e-node 방식을 검토하고 있습니다.

■ 현재 제약과 다음 실험

현재 구현은 ordered Miller pattern만 지원합니다. 따라서 바인딩된 변수를 패턴에서 사용하려면 바인딩 순서와 같은 순서로 인자로 넘겨야 합니다. `(@lam x (@lam y (?a x y)))`는 허용되지만 `(@lam x (@lam y (?a y x)))`는 허용되지 않습니다. 순서를 바꾸고 싶다면 우변에서 인자를 뒤집어 사용해야 합니다. 이 제한은 구현 복잡도를 줄였지만, 같은 메타변수가 서로 다른 순서로 사용되는 비선형 패턴에서는 표현력이 손실될 수 있습니다. 저자는 패턴 안에서 항을 생성하거나, thinning에 교환을 추가하는 방식을 가능한 해결책으로 보고 있습니다.

향후 계획으로는 proof log를 순회해 Lean 방식의 proof term을 출력하는 기능, Buchberger·multiset·string·semiring completion을 주입하는 실험, 7개를 넘는 변수를 위한 표현 방식, 더 풍부한 패턴 전처리 등이 언급됩니다. 저자는 아직 대규모 마이크로 최적화를 진행한 것은 아니지만 의미 없는 마이크로벤치마크에서는 `egg`의 약 3배 수준을 관찰했고, 10배 미만이면 괜찮다고 보는 대략적인 기준을 제시합니다. 구현에는 AI를 많이 활용했으며, 인덱스 조작 수학의 세부 사항을 반복해서 검토했지만 철저히 검증하지는 않았고 테스트를 바탕으로 동작한다고 판단한다고 밝혔습니다. 이 프로젝트를 통해 바인더 자체보다 먼저 컨텍스트가 변수 포함 항의 의미를 구성하는 핵심이라는 점, 그리고 weakening과 exchange 같은 컨텍스트 조작이 중요하다는 점을 강조합니다.

■ Lobsters 반응

• @cole-k — 한동안 e-graph 세계를 떠나 있었기 때문에 이 블로그 글의 전체 맥락을 이해할 수 있다고 말하기는 어렵지만, 람다를 제대로 지원하는 방향으로 진전된 모습은 멋집니다. 제 연구실 동료가 물어본 문제와도 관련이 있어 보입니다. 그는 `f(g(h(2)))`와 `f(g(h(3)))`가 어떻게 표현되는지 알고 싶어 했고, 저는 둘이 완전히 서로 다른 e-node와 e-class가 될 것이라고 답했습니다. 제가 틀린 것은 아니라고 꽤 확신하지만, 이것은 분명 비효율적으로 보입니다. 다만 항을 기준으로 생각할 때만 분명한 비효율이고, e-graph 세계에서는 실제로 그렇게 동작하지 않는다는 점도 함께 설명했습니다. 적절한 애플리케이션 규칙이 있다면 표현을 `app (f . g . h) 2` 같은 형태로 만들어 공유를 적용할 수 있지 않을까요? 글의 주제와 실제로 관련이 없는 이야기일 수도 있지만, 이 글을 보며 그 질문이 떠올랐습니다.

원문: Philip Zucker 블로그 / 번역·요약: Trawling