Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

The e-graph is a congruence closure and nothing can ask it whether two expressions are equal

オープン
  • 何か問題がありますか？
#1,251 コメント 1 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 1 日以内に返信

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
25/100
issue の種類
機能追加
明瞭さ
説明が足りない
活発さ
活発
技術スタック
csharp
領域
backend-api-design

調査の方向性

まず EGraph、Saturation、BudgetOutcome を読み、次に EqualitySaturationReviewFindings.md と issue #1036 の指針を比較します。公開されている等価性クエリがどこにあるのか、budget と soundness の結果がどのように表現されているのかを明らかにし、デフォルトの簡約とは別にそのコストを測定できれば完了です。

索引モデルが issue の本文から書いたものです。

説明

Measured on 2dbeedf7.

EGraph is internal sealed and is a congruence closure — Find, Merge, e-classes — with Saturation over it, a WorkBudget bounding it and pluggable extraction. It is reachable publicly only as a simplifier, Transformation.EqualitySaturation(budget, costModel), which saturates and then extracts one representative.

The question it could answer and is never asked is whether two expressions are equal: put a and b in one graph, saturate under a rule set, and report whether they landed in the same class.

That is not the same question as a.Simplify() == b.Simplify(). Two expressions can be equal under the rule set without either reaching a common normal form — simplification picks one representative per input by cost, and the two searches can settle in different places while the classes have already merged. The e-graph merges the classes whether or not extraction would agree.

What the public surface has today is neither:

  • MathS.UnsafeAndInternal.AreEqualNumerically(a, b) — sampling. Evidence, not a proof, and named accordingly.
  • Matrix.EntityTensorWrapperOperations.AreEqual(a, b) — structural, on the tensor wrapper.
Why it seems worth doing
  • It is a decision procedure over the rule set, which is a different capability from the whole Simplify pipeline rather than a convenience over it.
  • It is a verifier. #746's design principle 6 argues explicitly that "language models are strong proposers and weak verifiers; the platform must be the verifier", and that a design choice making verification cheap is worth more than one making generation slightly better. A cheap AreEqual is the smallest instance of that.
  • Tier 3 (the theorem graph) is recorded as "not started", and this is its cheapest entry point — an equality oracle over a rule set is the thing a fact database would be queried through.
  • The soundness metadata already lets the answer be qualified: Saturation knows which rules fired, and rules declare Sound vs SoundUnderAssumptions, so "equal, using only sound rules" and "equal, using conditional ones" are distinguishable rather than one boolean.
Questions rather than a design
  • Where should it live — MathS.AreEqual(a, b, budget), or on Entity?
  • What is the third answer? Saturation runs to a budget, so the honest result is three-valued: equal, not shown equal within the budget, budget exhausted — and #1036 is precedent for not spelling a resource limit the same as a mathematical negative. BudgetOutcome already exists to carry the third.
  • Should it report the weakest soundness used, the way DerivationPath takes the weakest across a step?
  • Is EGraph cheap enough to make this worth calling, given EqualitySaturationReviewFindings.md recommended against running Simplify on the graph by default? The recommendation was about the default simplification path; an explicitly-invoked equality query is a different cost question and should be measured on its own rather than inherited.

Part of #746, tier 3.

主要言語
C#
スター
831
フォーク
79
平均マージ
2時間 22分
マージ済み PR（30日）
507

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

ASC-Community/AngouriMath のほかの issue

ASC-Community/AngouriMath の issue をすべて見る

似ている issue

C# の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。