Refinement E-Graph — 등식 대신 정제 관계를 내장한 E-Graph

AI 요약

E-Graph는 서로 등가인 표현을 한 구조에 모아 재작성과 최적 표현 추출을 돕습니다. 하지만 컴파일러 재작성 규칙이 늘 양방향 등식인 것은 아닙니다. 정수 오버플로나 0으로 나누기, 식의 자식 평가 순서처럼 원본 언어가 결과를 정하지 않는 경우가 있습니다. 이런 추상적인 표현을 구체적인 실행 표현으로 좁히는 방향성 있는 규칙을 다루려면 등식과 별도로 정제 관계가 필요합니다. 저자는 <=를 E-Graph에 내장한 Refinement E-Graph 프로토타입을 microegg 기반으로 구현하고, 웹어셈블리 데모도 제공합니다.

Don’t Care 회로 예제

디지털 회로의 don’t-care 입력은 결과를 정하지 않아도 되는 입력입니다. 최적화기는 그 입력에서 참이나 거짓 중 어느 쪽을 출력해도 되므로, 더 단순한 회로를 선택할 여지가 생깁니다. 글의 예제에서는 dontcare <= true, dontcare <= false를 모두 기록합니다. 조건식 ite(x, true, dontcare)에서 dontcare를 true로 좁히면 전체 식을 x로 추출할 수 있습니다.

여기서 dontcare를 true 또는 false와 등치시키지는 않습니다. 등치시키면 해당 상수를 쓰는 모든 위치가 한쪽 값으로 고정되지만, 정제 관계에서는 각 사용 위치에서 독립적으로 선택할 여지를 남깁니다. 의미론은 Bool -> Set Bool로 설명합니다. true는 항상 {True}, false는 {False}, dontcare는 {True, False}를 나타내며, t <= s는 모든 입력에서 t가 나타내는 집합이 s의 집합에 포함된다는 뜻입니다.

부등식 Union-Find와 함수 분산성

저자는 일반적인 E-Graph를 Union-Find와 hash cons의 조합으로 보고, Refinement E-Graph에는 등식 대신 부등식을 추적하는 Union-Find가 필요하다고 설명합니다. 제안한 인터페이스는 기존 union, is_eq, find에 add_le, is_le, all_le, all_ge를 더합니다. 각 항목의 상한과 하한을 저장하고, 전체 상·하한 집합은 필요할 때 깊이 우선 탐색으로 계산합니다. 부등식 관계는 반사적·추이적으로 다루며, 양방향 관계가 생기면 등식으로 합칩니다.

함수 기호마다 인자별 분산성(variance)을 지정합니다. 단조(monotone) 인자에서는 a <= b가 f(a) <= f(b)로 이어집니다. 반단조(antitone) 인자에서는 방향을 뒤집습니다. 저자가 든 diff(A, B)는 첫 인자에서 단조이고 둘째 인자에서 반단조입니다. 분산성을 모르는 인자는 등식으로만 처리합니다. 이 정보는 정제 폐쇄뿐 아니라 패턴 탐색과 추출 과정에서도 관계의 방향을 결정합니다.

정제 폐쇄와 E-matching

일반적인 합동 폐쇄(congruence closure)는 자식 인자들이 등치되면 해당 함수 항도 등치시킵니다. 정제 폐쇄(refinement closure)는 함수의 분산성을 따라 인자 사이의 부등식을 함수 항 사이의 부등식으로 전파합니다. 예를 들어 diff(a,c) <= diff(b,d)는 a <= b와 c >= d에서 도출됩니다.

정제 폐쇄는 새 enode를 만들어 관계를 확장하는 방식과, 이미 존재하는 enode 사이에만 부등식을 기록하는 방식으로 나뉩니다. 전자는 유용하지만 항을 계속 만들며 커질 수 있습니다. 저자는 새 항을 만들지 않는 약한 폐쇄도 구현에 포함합니다. 새 enode를 만드는 폐쇄는 종료를 보장하기 어렵고, 재작성 규칙처럼 주의해서 다뤄야 한다고 짚습니다.

정제 E-matching은 패턴과 대상 사이의 제약을 패턴 <= 대상 또는 대상 <= 패턴 형태로 추적합니다. 함수 인자를 따라 내려갈 때 분산성이 단조면 방향을 유지하고, 반단조면 뒤집으며, 불변이면 등식 모드로 전환합니다. 예를 들어 diff(?a, ?b) <= diff(x, y)는 ?a <= x, ?b >= y로 나뉩니다. 탐색 중에는 등식으로 연결된 항뿐 아니라 부등식 간선도 따라갈 수 있습니다.

추출과 한계

기존 추출은 등식 클래스 안에서 비용이 가장 낮은 항을 고릅니다. 정제 추출은 추출 결과 <= 대상 또는 추출 결과 >= 대상 같은 방향 조건을 둡니다. 가장 구체적이고 결정적인 표현을 우선한 뒤 항 크기로 동률을 깨는 방법, 또는 반대 순서를 쓰는 방법을 생각할 수 있다고 설명합니다. 코드에서는 추출과 패턴 탐색 모두 EQ, LE, GE 모드를 사용합니다.

저자는 일반적인 부분순서에서 부등식을 완전히 일반화하면 등식만큼 간단하거나 빠르게 처리하기 어렵다고 봅니다. 희소한 관계를 저장하고 조회 때 폐쇄를 계산하는 방식이 작은 마이크로벤치마크에서는 관계를 미리 모두 펼치는 방식보다 메모리와 시간 면에서 유리했다고 적습니다. 다만 Egglog처럼 최적화된 구현과의 성능 비교는 확인하지 못했다고 덧붙입니다. 적용 후보로 논리, 관계 대수, 부분형(subtyping), 질의 포함 관계, 격자 분석을 들며, 전체 작업이 정제 규칙만으로 이뤄진다면 정제 E-Graph가 부등식 테이블을 둔 hash cons보다 나은 점이 크지 않을 수도 있다고 선을 긋습니다.

원문: Lobsters / 번역·요약: Trawling