How to prove equations using diagrams, part 1

図を用いた方程式の証明方法、パート1

この記事はTopos Institute blogにも転載されています。

e-graph、すなわち「等価性グラフ」は、式木（expression tree）上の合同関係を維持するデータ構造です。これは、新しい式を形成する際に安定した同値関係です。1980年にNelsonとOppenによって最初に考案されました（Nelson 1980; Nelson and Oppen 1980）。e-graphは、Willseyらによって、e-graphと等価性飽和を組み合わせることで、方程式推論のための高速で強力かつ適応性の高いツールとなりうることをソフトウェアパッケージeggで実証して以来、新たな注目を集めています（Willsey et al. 2021）。私のCatColabでの仕事では、eggの後継であるegglog（Zhang et al. 2023）を使用して、有限表示された圏について推論し始めています。

Nelsonの博士論文（Nelson 1980）に始まる標準的な説明は、union-findデータ構造のような、e-graphを実装するために必要なデータ構造とアルゴリズムを強調しています。コンピュータ代数の研究が最終的にこのように地に足のついたものになることは重要です。それでも、実装の詳細から抽象化すると、e-graphで本当に何が起こっているのか、私は不思議に思わずにはいられません。e-graphの図式的で視覚的な性質は、インタラクティブなegglogデモで明らかであり、圏論者であれば、圏論的なアイデアが暗黙のうちに働いている可能性を示唆するでしょう。

最近、2つのグループがe-graphの圏論的意味論を提案しました（Biondo, Castelnovo, and Gadducci 2025; Tiurin et al. 2025）。具体的には触れませんが、どちらも「e-ハイパーグラフ」を、直接的または間接的に同値関係を指定する追加構造を備えたラベル付きハイパーグラフとして定義しています。彼らの出発点は、e-graphが何であるかを述べることです。最終的には私自身の「e-図」の定義を提案しますが、e-graphがどのように操作されるかを考慮することから始めます。最終的な目標は、e-graph計算の圏論的かつ操作的な意味論を与えることです。中心となる概念は初期ファンクターになります。

この記事では、追加構造のない圏で主要なアイデアを紹介します。e-graphと比較すると、この設定は非常に制限的になります（単項関数記号のみを許可することに対応します）が、最小限のセットアップでポイントに到達するという利点があります。将来の記事では、有限積を備えた圏に一般化し、e-graphの標準設定を回復します。

図を用いた方程式の表現

抽象代数に触れたことがあるなら、圏論者が可換図を描いて射間の等式をどのように表現するかを見たことがあるでしょう。例えば、ある圏における射の正方形が

［画像］

可換であるということは、(g \circ f = k \circ h) という等式が成り立つことを意味します。

形式的な定義を思い出しましょう。これらは標準的ですが、微妙な違いがないわけではありません。

定義1 圏(\mathsf{C})における図とは、関手 (D: \mathsf{J} \to \mathsf{C}) のことです。その定義域(\mathsf{J})（図のインデックス圏または形状）は、小さな圏です。追加の用語：

• 図が自由であるとは、その形状が自由圏であること、つまり、(\mathsf{J} = \mathrm{Path}(G)) が（無限である可能性もある）グラフ (G) によって自由に生成されること。
• 図が有限表示であるとは、その形状が有限表示された圏であること。
• 図が可換であるとは、(\mathsf{J}) における同じ始域と終域を持つ任意の2つの射について、ターゲット圏 (\mathsf{C}) におけるそれらの像が等しいこと。

図が自由かつ可換である可能性もあることに注意してください。自由であることは図の形状の性質であり、可換であることはターゲット圏における図の像も決定的に関わります。

実際には、自由かつ有限表示された図を扱います。これは、図の形状が有限グラフによって自由に生成されることを意味し、これはコンピュータ科学者が容易に実装できるデータ構造です。コンピュータ代数を行う場合、ターゲット圏自体は生成元と関係によって有限表示されます。当初、私たちが「知っている」唯一の等式は、関係として明示的に与えられたものです。私たちの目標は、ターゲット圏におけるさらなる等式を、ターゲット圏内の図を操作することによって導き出すことです。

しかし待ってください：有限表示された圏における図は、コンピュータ科学者が理解できるグラフ理論的概念のみを使用して記述できる場合、圏と関数の導入のポイントは何でしょうか？圏論が、図の有効な操作を簡潔に記述するために不可欠であることがわかります。これらの操作は、追加のプロパティを満たす関手である図の間の射の形式を取ります。

初期ファンクター

図による推論、または「図追跡」1は、与えられた図、例えば (D: \mathsf{J} \to \mathsf{C}) を、特定の推論規則に従って別の図 (D': \mathsf{J}' \to \mathsf{C}) に変換する技術です。通常の数学的実践では、これらの規則が何であるかを述べることに誰も手間をかけません。私たちはより体系的になることを目指します。

考えられる明白な操作を検討してみましょう。図 (D: \mathsf{J} \to \mathsf{C}) が与えられた場合、ファンクター (R: \mathsf{J}' \to \mathsf{J}) に沿ってそれを引き戻すことにより、別の図 (D' \mathrel{\vcenter{:}}=D \circ R: \mathsf{J}' \to \mathsf{C}) を取得できます。逆に、ファンクター (R: \mathsf{J} \to \mathsf{J}') と図 (D': \mathsf{J}' \to \mathsf{C}) を見つけて (D = D' \circ R) となるように図 (D) を拡張できます。

［画像］

これ以上仮定しない限り、どちらの推論規則も、図によって提示される等式の解を正確に保存するという意味（正確には定義される）では有効ではありません。そのためには、(R) が特別な種類のファンクター、すなわち初期ファンクターである必要があります。これは、以下の同値な条件のいずれかによって特徴付けられます。

定義

定理1（初期ファンクター） ファンクター (R: \mathsf{J} \to \mathsf{K}) は初期である（ここでは (R: \mathsf{J} \twoheadrightarrow\mathsf{K}) と表記する）といい、以下の同値な条件のいずれかが成り立つ場合を指す。

• (R)に沿った引き戻しは極限を保存する：もし(\mathsf{C})が圏であり、(D: \mathsf{K} \to \mathsf{C})が(\mathsf{C})における図であるなら、極限が存在する限り、極限間の標準的な射 ([\lim riangleright_{\mathsf{K}} D \to \lim riangleright_{\mathsf{J}} (D \circ R))] は同型である。
• (R)に沿った引き戻しは集合の極限を保存する：もし(D: \mathsf{K} \to \mathsf{Set})が集合の図であるなら、極限間の標準的な関数 ([\lim riangleright_{\mathsf{K}} D \to \lim riangleright_{\mathsf{J}} (D \circ R))] は全単射である。
• (R)に関するスライスは連結である：任意の対象 (k \in \mathsf{K}) について、コンマ圏 (R/k) は空でなく連結である。2

この同値性の（双対の）証明については、(Riehl 2014, Lemma 8.3.4) を参照してください。

極限の直観があれば、極限の特性による初期性の判定は有用です。なぜなら、与えられたファンクターが初期であるかどうかを、集合の極限がどうなるかを想像するだけで、一目でわかることが多いからです。一方、スライスによる判定は、具体的かつ構文的であるため有用です。ファンクター (R: \mathsf{J} \to \mathsf{K}) と対象 (k \in \mathsf{K}) が与えられた場合、コンマ圏 (R/k) は以下を持つことを思い出してください。

• 対象：対象 (j \in \mathsf{J}) と射 (f: R(j) \to k) in (\mathsf{K}) のペア。
• 射：((j, f) \to (j', f')) は、三角形が可換になるような (h: j \to j') in (\mathsf{J}) の射：

［画像］

関係する圏が自由かつ有限生成である典型的な場合、初期性の証明（各コンマ圏 (R/k) が空でなく連結であることを確認すること）は、組み合わせ問題に帰着します。

解釈

なぜ初期ファンクターが等価性推論に関連するのでしょうか？一般に、図の極限は、図によって仮定される等式のすべての可能な解を表す対象と考えることができます。この解釈は、元の圏 (\mathsf{Set}) では明確です。そこでは、一般的な公式が、形状の射によってインデックス付けされた等式を満たす要素のタプルのサブセットとして、集合の図の極限を与えます。具体的には、図 (D: \mathsf{J} \to \mathsf{Set}) の極限は、すべての等式

([ D(f)(x_i) = x_j, \qquad \forall f: i \to j\ \text{in}\ \mathsf{J}, ]

を満たす (x_j \in D(j)) であるようなタプル ((x_j)_j \in \mathsf{J}) の集合です（Leinster 2014, Example 5.1.22）。したがって、初期ファンクターに沿った引き戻しは極限を保存するため、初期ファンクターは直観的には図によって提示される等式系の「解集合」を保存するものです。

しかし、私たちの関心は、ターゲットが有限表示された圏 (\mathsf{C}) である図 (D: \mathsf{J} \to \mathsf{C}) にあります。そのような圏は、通常、多くの非自明な積や等化器を持ちません。この問題は2つの方法で回避できます。

第一に、表示の集合論的な解釈、すなわちファンクター (F: \mathsf{C} \to \mathsf{Set}) を常に考慮できます。すると、合成 (F \circ D: \mathsf{J} \to \mathsf{Set}) は集合の図となり、標準的な設定に戻ります。この視点は、e-graphコミュニティが「解釈されない関数」または「関数記号」（私たちにとっては、(\mathsf{C}) の射を生成する）について語るときに取られます。解釈されない関数に関する任意の推論された等式は、実際の関数による解釈においても真のままです。したがって、関数を用いた等価性推論に対して完全な形式的な証明システムがある場合、初期ファンクターを使用して推論された等式には、そのシステム内に証明が存在します。3

もう少し注意を払うことで、任意の圏 (\mathsf{C}) で成り立つ等式をさらに導き出すことができます。単一の図から始めると仮定します。これは単一の対象 (X \in \mathsf{C}) をインデックス付けします。その図の極限は自明に (X) そのものであり、存在します。したがって、初期ファンクターに沿って引き戻したり拡張したりして得られる任意の図は、引き続き (X) を極限として持ちます。特に、そのような図における任意の2つの平行なパスは、(X) から始まる場合、可換でなければなりません。このテクニックは、後続の計算で使用します。有限積を持つ圏に一般化すると、任意の有限離散図から始めることができるため、より強力になります。そのインデックス付けされた対象は「自由変数」として機能します。

例と計算

記事の残りの部分では、一般的に見られる例と明示的な計算を通して、初期ファンクターの概念を説明します。目標は、初期ファンクターが図による機械的な推論の基礎としてどのように展開できるかを示唆することです。次の機会に、さらなる理論的発展を延期します。

初期ファンクター間のモチーフ

いくつかの最小限の初期ファンクターの例から始めます。これらはモチーフまたはパターンとして機能します。各例は、図による推論の推論規則を生み出します。

図のターゲット圏 (\mathsf{C}) は、ここでは固定されています。つまり、任意の初期ファンクターは、図の圏、すなわちスライス圏 (\mathsf{Cat}/\mathsf{C}) の射でもある必要があります。

• 操作導入：(\mathsf{C}) における任意の射 (f: X \to Y) について、図のマッピング

  ［画像］

  は初期です。

• より一般的に、(\mathsf{C}) における任意のパス (X_0 \xrightarrow{f_1} X_1 \xrightarrow{f_2} \cdots \xrightarrow{f_n} X_n) について、図のマッピング

  ［画像］

  は初期です。

• 合同削減：(\mathsf{C}) における任意の射 (f: X \to Y) について、図のマッピング4

  ［画像］

  （定義域の形状の (y) と (y') の両方を、値域の形状の (y) にマッピングする）は初期です。

• 操作導入と合同削減の両方を包含するものとして、任意の射 (f: X \to Y) in (\mathsf{C}) と整数 (n \geq 0) について、図のマッピング

  ［画像］

  （(y_1,\dots,y_n) のすべてを (y) にマッピングする）は初期です。

• 等式導入：等式 (g \circ f = k \circ h) が (\mathsf{C}) で成り立つと仮定します。これは前の図で示されています。すると、自由図のスパンの両方のマッピング

  ［画像］

  は初期です。より一般的には、これは (\mathsf{C}) における任意のパス等式に対して機能します。別の例として、恒等射 (\operatorname{id}_X = g \circ f) のようなナル関数パス等式を導入できます。

  ［画像］

後で、規則だけでなく、それらを適用する方法を形式化します。圏論的書き換えのアイデアを使用します。当面は、より大きな文脈で規則を適用する際に、結果のファンクターが依然として初期であると仮定します。または、各アプリケーションで初期性を検査することもできます。

可換な正方形の貼り合わせ

可換な正方形の貼り合わせ則を証明する最初の計算を行う準備ができました。これは、共通の辺を持つ2つの可換な正方形を並べて可換な長方形を生成することです。表記法により、これは明らかに真実のように見えますが、それでも証明が必要です。各図が初期ファンクターによって前の図に関連付けられる、または等式を導入する際には初期ファンクターのスパ​​ンによって関連付けられる、非常に機械的なスタイルで証明を提示します。

仮定：2つの可換な正方形が与えられているとします。

［画像］

これは、ターゲット圏 (\mathsf{C}) が (X,X',Y,Y',Z,Z') と呼ばれる6つの対象と、(f,f',g,g',h,k,\ell) と呼ばれる7つの射によって生成され、それらの2つの等式によって制約されることを意味します。

構築：(X) 上の単一図から始めます。その極限は自明に (X) です。証明したいパス等式の左辺と右辺を導入します。

［画像］

パス (X \xrightarrow{h} X' \xrightarrow{f'} Y') を最初の正方形の左辺として認識し、その等式を導入します。

［画像］

(f) の出現に対して合同削減を適用します。

［画像］

次に、パス (Y \xrightarrow{k} Y' \xrightarrow{g'} Z') を2番目の正方形の左辺として認識し、その等式を導入します。

［画像］

すでに完了していますが、(g) の出現、次に (\ell) の出現に対して合同削減を行うだけで、きれいにすることができます。

［画像］

結論：図の極限は依然として (X) であるため、外側の長方形は可換です。

モノイドの表示

要素 (f) が等式

([ f^3 = \operatorname{id}= f^5. ]

を満たすモノイドを考えます。つまり、ターゲット圏 (\mathsf{C}) は、単一の対象、例えば (\bullet) と、それらの2つの等式を満たす自己準同型射 (f: \bullet \to \bullet) によって生成されます。

単一図 ({\bullet}) から始め、両方の定義等式を導入します。各等式は片側に恒等射を持つため、サイクルとして現れることに注意してください。

［画像］

すべての射が生成射 (f) の上に横たわるため、矢印はラベルなしのままにします。次に、合同削減がそれ以上不可能になるまで、合同削減を繰り返し適用して合同閉包を計算します。合同削減の影響を受ける矢印は、上の2つの青い矢印から始まり、削減の両側で同じ色になります。最初の削減は次のとおりです。

［画像］

次：

［画像］

さらに3回の合同削減により、次の図が得られます。

［画像］

ここで止めることもできますが、さらに2回削減して、(f) 上の自己ループである図を生成することもできます。図の極限は、私たちが始めたもの、すなわち一意の対象 (\bullet) であるため、等式

([ f = \operatorname{id}, ]

を証明しました。言い換えれば、表示されたモノイドは実際には自明なモノイドです。これは、群論における、群の要素 (g) が (m) と (n) が互いに素な場合、(g^m = \operatorname{id}= g^n) を満たすならば (g = \operatorname{id}) であるという事実の特別なケースとして覚えているかもしれません。

議論

圏論はしばしば抽象的、さらには「抽象的なナンセンス」と言われますが、圏論の力を与えるのは抽象と具体の相互作用です。初期ファンクターは、その補完的な内在的および構文的な記述により、この相互作用を例示しています。

初期ファンクターがe-graphの操作的意味論の基礎を形成する方法を探求し始めました。通常の「小ステップ」操作的意味論のように、個々のステップを定義してからそれらを連鎖させるのではなく、初期ファンクターによって不変に有効な変換を定義し、有用な特殊化を探します。概念的な内容を超えて、この柔軟性は実用的なシステムが効率を向上させるために削減をバッチ処理する傾向があるため重要です。私たちにとって、それはしばしば初期ファンクターを合成するだけになります。

多くのヒントがありましたが、e-graphとの直接的な関連はまだ付けていません。別のヒントは、最後の例がNelsonとOppenの初期の仕事（Nelson 1980; Nelson and Oppen 1980）から直接取られていることです。そこでは、それは継続的な例となっています。今後の記事では、e-graphとの関連をさらに明確にします。また、形式主義が有限積を持つ圏にどのように一般化するかを説明します。これは代数理論の圏論的対応物です。

参考文献

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. arXiv:1612.09375.

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. DOI:10.1145/322186.322198.

Riehl, Emily. 2014. Categorical Homotopy Theory. Cambridge University Press. DOI:10.1017/CBO9781107261457. https://math.jhu.edu/~eriehl/cathtpy.pdf.

Tiurin, Aleksei, Barrett Chris, Dan R. Ghica, and Nick Hu. 2025. “Equivalence Hypergraphs: DPO Rewriting for Monoidal e-Graphs.” arXiv:2406.15882.

Willsey, Max, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. “Egg: Fast and Extensible Equality Saturation.” Proceedings of the ACM on Programming Languages 5 (POPL): 1–29. DOI:10.1145/3434304. arXiv:2004.03082.

Zhang, Yihong, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. “Better Together: Unifying Datalog and Equality Saturation.” Proceedings of the ACM on Programming Languages 7 (PLDI): 468–92. DOI:10.1145/3591239. arXiv:2304.04332.

注釈

1. このシリーズでは、まず生の圏を扱い、後でデカルト圏に一般化します。伝統的な形式の図追跡は、加法圏とアーベル圏で行われ、これは別の一般化の方向性です。私たちの方法を、可換モノイドまたはアーベル群における圏のエンリッチメントから始めて、加法設定に拡張してみるのは面白いでしょう。↩︎
2. 圏が連結であるとは、その任意の2つの対象が射のジグザグによって接続できること、つまり、それらの間に無向パスが存在することを意味します。↩︎
3. これは、完全性によって含意される証明を提示することが容易または便利であるという意味ではありません。私の理解では、証明抽出はe-graphコミュニティで活発に研究されているトピックです。↩︎
4. 圏 (\mathsf{C}) における図 (D: \mathsf{J} \to \mathsf{C}) を描画する際、「型理論的」表記 (x: X) は、ターゲット圏 (\mathsf{C}) の対象 (X) にマッピングされるインデックス圏 (\mathsf{J}) の対象 (x) に名前を付けます。図を項グラフと考えると、対象 (x) はまさに「型 (X) の項」です。↩︎