🔢 mathematics

Categorical E-Graphs for Lambda Calculi

이 논문은 e-그래프의 범주론적 프레임워크를 폐쇄 대칭 단성 범주(closed symmetric monoidal categories)로 확장하여 $\lambda$ -calculus의 변수 바인딩을 네이티브로 지원하며, 표준 항 재작성(term rewriting)과 동등함이 증명된 이중 푸시아웃 재작성 메커니즘을 갖는 계층적 하이퍼그래프 표현을 도입한다.

원저자: Aleksei Tiurin, Dan R. Ghica, Nick Hu

게시일 2026-06-26

📖 4 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Aleksei Tiurin, Dan R. Ghica, Nick Hu

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 거대한 퍼즐을 풀려고 노력하고 있다고 상상해 보세요. 하지만 퍼즐 조각을 하나 움직일 때마다, 당신은 이미 배치해 두었던 다른 조각들을 실수로 파괴하게 됩니다. 이것이 컴퓨터 과학자들이 복잡한 컴퓨터 프로그램을 최적화할 때 직면하는 문제입니다. 그들은 e-그래프(equality graph, 등가 그래프)라는 도구를 사용하는데, 이는 마치 매우 효율적인 서류 보관함과 같습니다. 이 도구는 더 나은 버전을 발견했을 때 기존의 프로그램 버전을 버리는 대신, 모든 버전을 동일한 보관함 안에 유지하며 서로 같은 의미를 가진 조각들을 그룹화합니다. 이를 통해 컴퓨터는 길을 잃지 않고 수백만 개의 가능성을 동시에 탐색할 수 있습니다.

하지만 문제가 하나 있습니다. e-그래프는 역사적으로 변수(수식에서의 "x"와 같은 것)를 다루는 데 어려움을 겪어 왔습니다. 프로그램에서 변수는 옮겨 다닐 수 있는 이름표와 같습니다. 만약 이름표를 옮기면 프로그램의 의미가 변할 수도 있고, 이름표가 놓인 위치가 다르다는 이유만으로 두 개의 동일한 프로그램이 서로 다르게 보일 수도 있습니다. 이 때문에 e-그래프가 그것들이 실제로 동일하다는 것을 인식하기가 매우 어렵습니다.

핵심 아이디어: 텍스트에서 그림으로

이 논문의 저자들은 이러한 변수 이름표를 처리하는 새로운 방법을 제안합니다. 그들은 프로그램을 (우리가 읽는 문장 같은) 텍스트로 취급하는 대신, 스트링 다이어그램(string diagrams, 도식)처럼 취급합니다.

기존 방식 (텍스트): 레시피를 쓰는 것을 상상해 보세요. 만약 1단계에 "소금을 넣는다"라고 쓰고 5단계에도 "소금을 넣는다"라고 쓴다면, 컴퓨터는 이를 두 개의 별개 문장으로 인식합니다. 설령 그 의미가 같더라도, 컴퓨터는 그것들이 동일하다는 것을 알아내기 위해 추가적인 작업을 수행해야 합니다.
새로운 방식 (스트링 다이어그램): 레시피를 재료와 동작을 연결하는 전선이 있는 물리적인 순서도라고 상상해 보세요. 만약 "소금을 넣는다"라는 단계가 두 개 있다면, 그것들은 말 그대로 동일한 물리적 전선이 두 개의 다른 지점에 연결되어 있는 것입니다. 텍스트를 비교할 필요가 없습니다. 그림 자체가 그것들이 동일함을 보여줍니다.

"마법 상자" 솔루션

변수(프로그램의 특정 부분 안에 묶이거나 잠길 수 있는 로컬 변수 등)를 처리하기 위해, 저자들은 범주론(Category Theory)이라는 고급 수학 개념을 사용합니다.

프로그램을 입력과 출력이 있는 기계라고 생각해 보세요.

상자 (The Box): 그들은 함수(람다 추상화, λx와 같은 것)를 둥근 상자로 표현합니다. 변수 x는 상자 안으로 들어가는 전선입니다.
공유 (The Sharing): 그들은 동일한 것들의 집합을 나타내기 위해 점선 상자를 사용합니다. 만약 두 부분이 수학적으로 같다면, 그들은 동일한 점선 상자 안에 놓이게 됩니다.
결과: 이 상자들을 결합함으로써, 그들은 Closed E-Hypergraph(폐쇄형 e-하이퍼그래프)라는 구조를 만들어냅니다. 이것은 서로 다른 상자 안에 있거나 서로 다른 변수 이름을 가지고 있더라도, 두 조각이 동일하다는 것을 자동으로 인식하는 "퍼즐 지도"의 세련된 이름입니다.

작동 원리: "재배선" 기술

전통적인 e-그래프에서는 프로그램을 변경하려면 기존 조각을 삭제하고 새 조각을 붙여넣어야 합니다. 이는 위험하고 느린 작업입니다.

이 새로운 시스템에서 프로그램을 변경하는 것은 회로 기판의 배선을 다시 하는 것과 같습니다.

베타 축약(Beta-reduction, 함수에 값을 대입하는 프로그래밍의 기본 규칙)을 단순히 텍스트를 삭제하는 것이 아니라, 전선을 한 소켓에서 뽑아 다른 소켓에 꽂는 것으로 생각합니다.
구조가 이러한 다이어그램을 기반으로 구축되었기 때문에, 컴퓨터는 변수를 이름을 바꾸거나(renaming) 변수가 잘못된 범위에 포착(captured)되었는지 확인할 필요가 없습니다. 전선은 자연스럽게 흐릅니다.

이것이 왜 중요한가 (논문에 따르면)

저자들은 이 아이디어를 선형 치환 계산법(linear substitution calculus, 코드의 "let" 문과 공유를 다루는 방식)이라는 특정 유형의 프로그래밍 로직을 사용하여 테스트했습니다.

기존 방식의 문제점: "let" 문(예: let x = 1 in...)을 처리하기 위해, 기존의 e-그래프는 이름을 관리하기 위한 특수한 "관료적(bureaucratic)" 노드와 규칙들을 추가해야 했습니다. 이는 시스템을 복잡하게 만들고 속도를 늦췄습니다.
새로운 방식: 그들의 다이어그램 시스템에서 "let" 문은 자연스러운 연결일 뿐입니다. 시스템은 let x = 1 in (x + x)가 let y = 1 in (y + y)와 같다는 것을 추가적인 규칙 없이도 자동으로 이해합니다. "공유"는 다이어그램의 기하학적 구조 안에 내장되어 있습니다.

결론

이 논문은 프로그램을 텍스트가 아닌 위상적 지도(topological maps)로 취급하는 e-그래프를 위한 새로운 수학적 토대를 구축했다고 주장합니다. 변수를 숨기기 위한 "상자"와 그들을 연결하는 "전선"을 사용함으로써, 그들은 다음과 같은 시스템을 만들었습니다:

동등성이 자동화됨: 두 다이어그램이 위상적으로 같다면, 그것들은 동일한 프로그램입니다.
재작성이 안전함: 프로그램의 일부를 변경해도 나머지 부분을 파괴하지 않습니다.
변수가 자연스럽게 처리됨: 더 이상 번거로운 이름 변경이나 특수한 "관료적" 노드가 필요하지 않습니다.

저자들은 이 접근 방식이 (변수를 명시적인 데이터 슬롯으로 취 treating하는) "슬롯형(slotted)" e-그래프에 의존했던 이전 방식들에 비해, 함수형 프로그래밍 언어(람다 계산법에 기반한 언어들)에 특히 강력하다고 주장합니다. 그들은 자신들의 다이어그램 기반 재작성이 전통적인 텍스트 기반 재작성만큼 정확하면서도, 프로그램의 "형태"를 직접 다룰 수 있다는 이점을 제공한다는 수학적 증명을 제시합니다.

기술 요약: 람다 계산식을 위한 범주론적 E-그래프 (Categorical E-Graphs for Lambda Calculi)

문제 정의

등가 포화(Equality saturation)는 프로그램 최적화 및 추론을 위한 강력한 기법으로, 치환되지 않는 방식으로 변환 규칙의 집합을 탐색하기 위해 동치 클래스의 항(equivalence classes of terms, e-graphs)을 활용한다. 그러나 전통적인 e-graph는 함수형 프로그래밍 언의 핵심 기능인 변수 바인딩(variable binding)을 네이티브하게 지원하지 못한다.

바인딩을 통합하려는 기존 방식들은 다음과 같은 중대한 문제에 직면해 있다:

텍스트 표현식: 표준적인 텍stual 구문에서 $\alpha$ -동치(alpha-equivalent)인 항들은 서로 별개의 것으로 취급되며 공유될 수 없다. De Bruijn 인덱스는 $\alpha$ -동치를 구문론적으로 식별하지만, 이 인덱스들은 변수의 스코프(scope)에 의존하기 때문에 인덱스 할당만 다른 항들(예: $\lambda f. f((\lambda x. fx)2)$ )을 공유하는 것을 방해한다.
명시적 치환 (Explicit Substitution): 바인딩을 처리하기 위해 명시적 치환 노드(예: $t[x/u]$ )를 추가하면 "관료주의(bureaucracy)"가 발생한다. 이는 상호작용하지 않는 치환들의 순열(graphical equivalence)을 관리하기 위한 추가적인 노드와 변환 규칙을 요구하며, 도메인 특화된 변환보다는 행정적인 오버헤드에 의한 상태 공간의 비대화를 초래한다.
슬롯형 E-그래프 (Slotted E-Graphs): 최근 연구(Schneider 등)는 변수를 일급 데이터로 다루는 "슬롯형 e-graph"를 도입했다. 이 방식은 임의의 언어(예: $\pi$ -calculus)에 적용 가능한 nominal 기법에 의존하지만, 람다 계산의 특정 구조적 특성을 전용 의미론 모델만큼 효율적으로 활용하지는 못할 수 있다.

핵심 문제는, 명시적 치환 노드나 복잡한 이름 변경 규칙 없이도 람다 계산식에서 효율적인 등가 포화를 지원할 수 있는, 변수 바인딩을 위한 네이티브한 범주론적 데이터 구조의 부재이다.

방법론

저자들은 e-graph를 스트링 다이어그램(string diagrams)의 해석으로 확장하는 **범주론적 의미론(categorical semantics)**에 기반한 솔루션을 제안한다.

1. 범주론적 프레임워크

본 논문은 e-graph(바인딩이 없는 경우)를 **대칭 단사 반격자-풍부 범주(symmetric monoidal semilattice-enriched categories, SLat-categories)**의 사상(morphism)으로 모델링한 Tiurin 등의 연구를 바탕으로 한다.

SLat-풍부성 (SLat-Enrichment): Hom-set은 반격자(semilattice)이며, 여기서 조인(join) 연산( $+$ )은 부분항의 동치(equivalence of subterms, 즉 e-class)를 나타낸다.
단사 폐쇄 구조 (Monoidal Closed Structure): 변수 바인딩을 처리하기 위해 저자들은 범주를 단사 폐쇄(monoidal closed) 구조로 확장한다. 이는 내부 호(internal hom object) $A \multimap B$ 와 인접 관계(adjunction) $- \otimes B \dashv B \multimap -$ 를 도입한다.
스트링 다이어그램 (String Diagrams): 항들은 스트링 다이어그램으로 표현된다. 바인딩은 "둥근 상자"( $\lambda$ -추상화 표현)로 모델링되며, 동치 클래스는 "점선 상자"(반격자 조인 표현)로 모델링된다.

2. 조합적 표현: 폐쇄형 e-하이퍼그래프 (Closed E-Hypergraphs)

구체적인 데이터 구조를 제공하기 위해, 저자들은 폐쇄형 e-하이퍼그래프를 정의한다. 이는 다음을 인코딩하는 계층적 하이퍼그래프이다:

하이퍼엣지 (Hyperedges): 연산(generators)을 나타낸다.
계층적 엣지 (Hierarchical Edges): 두 종류의 중첩된 구조:
- E-클래스 (점선 상자): 부분항의 동치 클래스를 나타낸다.
- 추상화 상자 (둥근 상자): $\lambda$ -추상화를 나타낸다.
인터페이스 (Interfaces): 구조는 확장된 코스팬(extended cospans)을 사용하여 입출력을 관리하며, 외부 인터페이스(최상위)와 엄격히 내부적인 인터페이스(상자 내부에 중첩됨)를 구분한다.

3. 변환 시스템 (Rewriting System)

저자들은 폐쇄형 e-하이퍼그래프를 위한 인터페이스를 포함한 이중 푸시아웃(Double-Pushout with Interfaces, DPOI) 변환 시스템을 정의한다.

변환 규칙: 코스팬의 스팬(span)으로 정의된다.
경계 보충 (Boundary Complements): 계층적 구조를 처리하기 위해 매칭된 부분을 제거한 후 남는 "구멍(hole)"에 대한 특수한 정의가 도입된다. 이는 하위 그래프가 제거될 때 내부 인터페이스가 올바르게 조정되도록 보장한다(예: 중첩된 항을 제거하면 부모의 엄격한 내부 인터페이스가 업데이트됨).
건전성 및 완전성: 본 논문은 이러한 폐쇄형 e-하이퍼그래프에 대한 DPO 변환이 대칭 단사 SLat-범주의 방정식 및 폐쇄 구조의 분배 법칙을 따르는 폐쇄형 $\Sigma^+$ -항의 변환에 대해 건전하고 완전함을 입증한다.

주요 기여

범주론적 확장: e-graph의 범주적 영역을 자유 대칭 단사 SLat-범주에서 자유 폐쇄 대칭 단사 SLat-범주로 확장함으로써 바인딩을 지원하는 형태의 e-graph를 구축하였다.
폐쇄형 e-하이퍼그래프: 대칭 단사 구조와 폐쇄 구조(바인딩)의 방정식을 자연스럽게 흡수하는 구체적인 조합적 표현(폐쇄형 e-하이퍼그래프)을 정의하였다.
바인딩을 위한 DPOI 변환: 이 구조에 대한 DPOI 변환 시스템을 정식화하고, 해당 범주 이론에서의 항 변환에 대한 건전성과 완전성을 증명하였다.
슬롯형 e-그래프와의 비교: 슬롯형 e-graph가 nominal 기법을 통해 일반적인 바인딩을 제공하는 반면, 범주론적 접근 방식은 바인딩을 모델의 내부 언어에 내장함으로써 람다 계산 특화 최적화에 있어 잠재적 이점을 가질 수 있음을 이론적으로 비교하였다.

결과

변환의 동치성: 본 논문은 폐쇄형 $\Sigma^+$ -항의 항 변환이 폐쇄형 e-하이퍼그래프의 DPO 변환과 동치임을 증명한다.
그래피컬 동치 처리: 이 방식은 명시적 치환 노드나 이를 처리하기 위한 변환 규칙 없이도 "그래피컬 동치"(비상호작용 치환의 순열)를 자연스럽게 처리한다. 범주론적 모델에서 명시적 치환은 합성(composition)으로 모델링되며, 범주의 구조적 법칙이 필요한 동치 관계들을 흡수한다.
사례 연구 ( $\lambda_{lsub}$ ): 저자들은 이론을 **선형 치환 계산법( $\lambda_{lsub}$ $λ_{l s u b}$ )**에 적용한다. 명시적 치환(예: let-binding)을 포함하는 항들이 스트링 다이어그램으로 직접 표현될 수 있음을 보여준다.
- 전통적인 e-graph가 치환과 그 순열을 처리하기 위해 명시적 노드와 변환 규칙을 필요로 하는 것과 달리, 범주론적 모델은 이를 다이어그램의 구조적 특성으로 취급한다.
- 본 논문은 의미론적으로 동등한 프로그램들(예: let-binding의 순서 변경)이 동일한 스트링 다이어그램으로 매핑됨을 보여주며, 이를 통해 등가 포화가 정규화된 표현 위에서 작동할 수 있게 한다.

의의 및 주장

본 논문은 바인딩이 있는 e-graph를 위한 기초적인 범주론적 의미론을 제공한다고 주장한다.

이론적 정당성: e-graph가 유지하는 합동(congruence)에 대한 엄밀한 정당성을 제공하며, 이를 폐쇄 대칭 단사 SLat-범주의 속성에 근거하여 입증한다.
효율성 잠재력: 구조적 방정식(결합법칙, 교환법칙, 치환 순열 등)을 그래피컬 구문과 기저 범주로 흡수함으로써, 등가 포화의 상태 공간에서 발생하는 "관료주의"를 줄이는 것을 목표로 한다. 이는 이러한 현상을 명시적 변환 규칙으로 취급하는 방식과 대조된다.
범위: 저자들은 자신의 접근 방식이 람다 계산 및 그 변형에 특화되어 있으며, 범주 모델의 메타 이론적 내부 언어를 활용한다고 명시한다. 이들은 슬롯형 e-graph가 바인더가 있는 임의의 언어(예: $\pi$ -calculus)에 더 유연할 수 있음을 인정하면서도, 람다 계산 특화 최적화에는 자신들의 방법이 우월하다고 주장한다.

본 연구는 완전한 소프트웨어 구현이나 경험적 벤치마크를 제시하기보다는, 폐쇄형 e-하이퍼그래프 표현을 "스트링 다이어그램 변환을 위한 e-graph"를 구축하기 위한 실행 가능한 토대로 포지셔닝한다.