초기 함자로 도식 변형의 등식 추론을 설명한다

2025년 5월 27일 Topos Institute 블로그에 실린 글에서 Evan Patterson은 범주론의 초기 함자를 이용해 도식 변형이 등식 추론에 어떻게 쓰이는지 설명합니다. Patterson은 CatColab 작업에서 egg의 후속 프로젝트인 egglog를 사용해 유한 제시 범주를 다루기 시작했습니다. 이 글은 그 개인 작업을 바탕으로, e-graph의 구현 자료구조보다 계산 과정에서 어떤 도식 변형이 유효한지를 설명하는 데 초점을 둡니다.

e-graph는 식 트리에 동치 관계를 함께 관리하는 자료구조입니다. 동치 관계가 합동성을 만족하면, 동치인 식에 같은 연산을 적용한 결과도 동치로 다룰 수 있습니다. Patterson은 이런 계산을 범주론으로 설명하려면 e-graph의 모양 자체보다 그 모양을 바꾸는 규칙을 살펴야 한다고 제안합니다.

범주론에서 도식은 대상과 사상으로 이루어진 모양을 다른 범주에 대응시킨 것입니다. 예를 들어 사각형이 가환한다는 말은 한쪽 경로를 따라 합성한 사상과 다른 쪽 경로를 따라 합성한 사상이 같다는 뜻입니다. 도식의 모양은 대상 범주와 구별되며, 도식의 사상은 그 모양 안의 경로를 대상 범주의 사상으로 보냅니다. 대상 범주에 처음 주어진 관계를 바탕으로, 도식을 변형해 새로운 등식을 이끌어내는 것이 글의 문제입니다.

집합으로 해석한 도식의 극한은 각 대상에 값을 하나씩 배정하되 모든 화살표가 요구하는 등식을 만족하는 값 배정의 집합입니다. 따라서 도식 모양을 바꾸는 추론 규칙이 해를 보존하려면, 변형 전후의 극한이 동형이어야 합니다. 집합으로 해석하면 두 해 집합 사이에 정준적인 일대일 대응이 생깁니다.

Patterson이 말하는 초기 함자는 도식의 모양 사이를 잇는 함자 가운데, 도식을 그 함자에 따라 당겨도 극한을 보존하는 함자입니다. 초기성은 집합을 대상으로 극한을 취했을 때 정준 함수가 전단사인지로 판정할 수 있습니다. 동등한 판정법으로는 대상 범주의 각 대상 k에 대해 R/k라는 범주가 비어 있지 않고 연결되는지 확인하는 방법이 있습니다. 이 범주의 객체는 도식의 대상에서 k로 가는 사상이며, 사상은 관련 삼각형을 가환하게 만드는 연결입니다. 도식의 범주들이 자유롭고 유한하게 생성된 전형적인 경우, 이 조건을 확인하는 일은 조합적 검사로 다룰 수 있습니다.

이 원리에서 도식 변형의 규칙이 나옵니다. 사상이나 경로를 도식에 도입하는 조작, 같은 사상에 대응하는 중복 부분을 합치는 합동 축약은 초기 함자로 나타낼 수 있습니다. 대상 범주에 이미 성립하는 등식을 도식에 도입할 때는 두 도식 사이에 span을 이루는 두 함자가 초기성을 만족합니다. 이 단계는 임의의 관계를 새로 가정하는 것이 아니라, 대상 범주에 주어진 관계를 사용하는 방식입니다.

두 가환 사각형이 변 하나를 공유할 때 바깥 경로도 가환한다는 사실은 이 규칙을 적용하는 예입니다. Patterson은 대상 X 하나만 있는 도식에서 시작해 증명할 두 경로를 도입합니다. 첫 번째 사각형의 등식을 적용한 뒤 반복된 사상 f를 합동 축약으로 정리하고, 두 번째 사각형의 등식도 같은 방식으로 도입합니다. 이어 반복된 g와 ℓ을 축약합니다. 각 변형이 극한을 보존하므로 마지막 도식의 극한도 처음처럼 X입니다. 이로부터 바깥 경로를 이루는 두 사상이 같다는 결론을 얻습니다.

모노이드 예에서는 생성자 f에 f³=id과 f⁵=id이라는 관계를 둡니다. 두 관계를 도식의 고리로 나타낸 뒤 합동 축약을 반복하면 f를 나타내는 자기 사상만 남습니다. 이 도식의 극한이 처음의 단일 객체로 보존되므로 f=id이라는 등식을 얻습니다. 따라서 이 관계를 만족하는 모노이드는 자명한 모노이드입니다.

Patterson은 유효한 변형을 작은 단계마다 따로 정의하기보다 초기 함자의 성질로 묶고, 그 조건에서 구체적인 규칙을 도출하는 방식으로 e-graph 계산의 작동 의미를 설명하려 합니다. 실용 시스템에서 효율을 위해 여러 축약을 묶어 처리하는 경우도 초기 함자들의 합성으로 나타낼 수 있다고 설명합니다. 이번 편은 추가 구조가 없는 범주를 다루므로 단항 함수 기호만 허용하는 제한된 경우에 해당합니다. Patterson은 후속 글에서 유한곱을 포함하는 범주로 확장해 표준적인 e-graph 설정에 다가가고, e-graph와의 직접 연결을 다루겠다고 밝혔습니다.