始関手と e グラフ：圏論的操作論的意味論への一歩

はじめに

**e グラフ（equality graph）**とは、表現ツリー上の同値関係（congruence relation）を維持するデータ構造です。この概念は 1980 年にネルソンとオッペンによって提唱され、その後「等式飽和（equality saturation）」技術と組み合わせることで、等式推論において高速かつ強力なツールへと進化しました。著者の研究では、egg の後継である egglogを用いて有限次提示圏（finitely presented categories）の推論を開始しています。

しかし、実装の詳細を抽象化し、「e グラフの本質的な仕組み」を探究する際、圏論家の直観が暗黙的に働いていることに気づかされます。最近、2 つの研究グループが e グラフの圏論的意味論を提案しており（「e ハイパグラフ」として定義）、本稿ではそれらの議論を補完すべく、**始関手（initial functor）**という鍵となる概念を導入し、e グラフ計算への圏論的および操作論的な意味論を与えることを目指します。

まず追加構造を持たない**裸の圏（bare categories）**における主要なアイデアを紹介します。

図式を用いた等式の表現

圏論家は、圏の射間の等式を**可換図式（commutative diagram）**によって表すことが多いです。例えば、四角形が可換であれば (g \circ f = k \circ h) が成り立つことを意味します。

定義：図式の形式化

カテゴリ (\mathsf{C}) 内の**図式（diagram）**とは、領域 (\mathsf{J})（形状または索引圏）が小さい圏である関手 (D: \mathsf{J} \to \mathsf{C}) です。

• 自由（free）な図式: 形状が自由圏（無限グラフ (G) によって自由に生成される (\mathsf{J} = \mathrm{Path}(G))）であるもの。
• 有限次提示（finitely presented）な図式: 形状が有限次提示圏であるもの。
• 可換（commutative）な図式: (\mathsf{J}) 内の同じ定義域と余域を持つ任意の射について、それらの (\mathsf{C}) への像が等しいもの。

実用的な視点 コンピュータ代数において我々は主に自由かつ有限次提示な図式を扱います。これらは有限グラフで記述可能であり、コンピュータ上で簡単に実装できます。ターゲット圏も発生記号と関係式によって定義されており、我々の目標は図式の操作を通じて新たな等式を導き出すことです。

なぜ圏論と関手を導入すべきでしょうか？それは、有効な図式操作を簡潔に記述するためです。これらの操作は、図式間の特別な種類の関手（追加の性質を満たす）によって表現されます。

始関手（Initial functors）

図式推論（diagram chasing）とは、規則に従って図式 (D) を別の図式 (D') に変換するプロセスです。ここでは、始関手と呼ばれる特別な関手が等式の解を完全に保存することを示します。

始関手の定義

関手 (R: \mathsf{J} \to \mathsf{K}) が始関手であることは、以下の同値条件の一つを満たすことで特徴付けられます：

1. 極限の保存: 圏 (\mathsf{C}) 内の図式 (D) に対して、極限が存在すれば (\lim_{\mathsf{K}} D \to \lim_{\mathsf{J}} (D \circ R)) は同型写像です。
2. 集合の極限の保存: 集合の図式 (D: \mathsf{K} \to \mathsf{Set}) に対して、標準関数は全単射（双射）です。
3. スライスの連結性: 任意の (k \in \mathsf{K}) に対して、コマー圏（comma category）(R/k) は空でなくかつ連結です。

この条件は、関手が「解の集合」を保存する性質と深く結びついています。

解釈（Interpretation）

図式の極限は、図式が提起する等式系のすべての可能な解を表す対象として捉えることができます。始関手への引き戻しは、この「解の集合」を保存します。

• 有限次提示圏でのアプローチ: ターゲットが有限次提示圏の場合、自明でない極限は稀です。これを回避するには：
  1. 解釈（Interpretation）する: 関手 (F: \mathsf{C} \to \mathsf{Set}) を考慮し、複合 (F \circ D) として集合の図式とみなします。これにより始関手が等式の完全性を保つことが保証されます。
  2. 単一対象からの拡張: 任意の圏 (\mathsf{C}) で成り立つ等式を導出するには、singleton 図式から始め、始関手を介して図式を変換します。

例と計算

1. 操作の導入（Motifs for Initial Functors）

(\mathsf{C}) 内の図式の圏における射として、以下のパターンがあります：

• 操作の導入: 任意の射 (f: X \to Y) に対して、図式間の写像が始関手となります。一般化すると、経路全体についても同様です。
• 同値性の削減（Congruence reduction）: 領域側の二つの対象 (y, y') を、余域側のもとの (y) にマッピングする写像は始関手です。これは操作の導入を包含します。
  • 任意の数 (n \geq 0) について、(y_1, \dots, y_n) をすべて (y) に送る写像も始関手です。
• 等式の導入: (\mathsf{C}) で成り立つ等式 (g \circ f = k \circ h) がある場合、それに対応する自由図式間のスパン（span）の両方の写像は始関手となります。

これら規則を適用した後の関手が始関手であることを自明なものとして扱うか、または逐次検証するかによって実装戦略が異なります。

2. 可換四角形の貼り付け

共通の辺を持つ 2 つの可換四角形を並置し、可換長方形を作ることを機械的に証明します。

• 準備: 単一対象 (X) 上の singleton 図式から始め、極限は (X) です。
• ステップ:
  1. 左辺の四角形 (X \xrightarrow{h} X' \xrightarrow{f'} Y') を認識し、等式を導入（操作導入）。
  2. (f) の出現に対して同値性の削減を適用。
  3. 右辺の四角形 (Y \xrightarrow{k} Y' \xrightarrow{g'} Z') を認識し、等式を導入。
  4. さらに必要に応じて、(g) と (\ell) の出現に対して同値性の削減を適用して整理する。
• 結論: 図式の極限は依然として (X) であるため、外部の長方形は可換です。

3. 単体の提示（A monoid presentation）

元の (f) を持つ単体（monoid）を考え、等式 (f^3 = \operatorname{id}= f^5) が成り立つとします。

• 開始: singleton 図式 ({\bullet}) から始め、両方の等式を導入します。
• 同値性の削減の反復:
  • 最初の青色の矢印（(f^3 = \operatorname{id})）を処理し、同値性削減を適用。
  • 次に (f^5 = \operatorname{id}) を処理し、さらに削減を行う。
• 結果: 反復的に削減を進めると、最終的に (f) と (\operatorname{id}) が同一になることが示せます：

  f = id
  

  これは、提示された単体が実際には自明な単体であることを意味します（群論の結果：(g^m = \operatorname{id} = g^n) なら (g = \operatorname{id})）。

議論と展望

圏論は抽象的ですが、補足的な内在的記述と文法的記述の相互作用がその威力を生んでいます。本稿では、始関手が e グラフに対する操作論的意味論の基礎であることを示唆しました。

• 柔軟性: 個別のステップを定義して連鎖させるのではなく、有効な変換を始関手を介して不変に定義し、有用な特殊化を探します。
• 効率性: 実用的なシステムは削減操作を束ねて実行する傾向があり、これはしばしば始関手の合成として記述できます。
• 未来の研究:
  • e グラフとの直接的な接続をさらに強化する。
  • **有限積（finite products）**を備えた圏へ一般化し、より強力な推論（任意の有限離散図式を扱う）を実現する。
  • ネルソンとオッペンが初期から使用していた等式の例との対応関係を探る。

---

参考文献

• Biondo, Roberto, Davide Castelnovo, and Fabio Gadducci. 2025. "EGGs Are Adhesive!" arXiv:2503.13678.
• Leinster, Tom. 2014. Basic Category Theory. Cambridge University Press. DOI:10.1017/CBO9781107360068.
• Nelson, Greg. 1980. "Techniques for Program Verification." PhD thesis, Stanford University.
• Nelson, Greg, and Derek C. Oppen. 1980. "Fast Decision Procedures Based on Congruence Closure." Journal of the ACM 27 (2): 356–64.
• Riehl, Emily. 2014. Categorical Homotopy Theory. Cambridge University Press.
• Tiurin, Aleksei et al. 2025. "Equivalence Hypergraphs: DPO Rewriting for Monoidal e-Graphs." arXiv:2406.15882.
• Willsey, Max et al. 2021. "Egg: Fast and Extensible Equality Saturation." Proceedings of the ACM on Programming Languages 5 (POPL).
• Zhang, Yihong et al. 2023. "Better Together: Unifying Datalog and Equality Saturation." Proceedings of the ACM on Programming Languages 7 (PLDI).

フットノート

1. 図式追いの方向性: このシリーズでは、まず**裸の圏（bare categories）**と働き、後にデカルト圏へと一般化します。従来の加法圏や可換圏内での図式追いは別の方向への一般化です。
2. 圏の連結性: 圏は「任意の対象を射の折れ線（zig-zag）によって接続できる場合」に連結であると定義されます。
3. 完全性と証明抽出: 解釈を用いることで形式系の完全性が保たれます。証明抽出は e グラフコミュニティで活発に研究されています。
4. 項と型: 図式 (D: \mathsf{J} \to \mathsf{C}) を項グラフとみなす際、索引圏 (\mathsf{J}) の対象 (x) は「型 (X) の項」と解釈されます。