Hacktoberfest 2026：维护者为十月标记出来的 issue，仍然开放、适合新手。 浏览 Hacktoberfest issue

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

未关闭
  • 哪里不对？
#1,251 1 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看

维护者通常 1 天内回复

还没有人认领这个 Issue。

评估

难度
5/5
预计耗时
一周以上
新手友好度
25/100
Issue 类型
功能
描述清晰度
需要澄清
活跃度
活跃
技术栈
csharp
领域
backend-api-design

调研方向

先阅读 EGraph、Saturation 和 BudgetOutcome，然后对比 EqualitySaturationReviewFindings.md 与 issue #1036 中的指导。完成的要求是明确公共等价性查询所在的位置、预算和 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 分钟
30 天内合并 PR
507

环境准备

  • 没有 Dockerfile 或 Docker Compose 文件
  • 没有 Pull Request 模板
  • 阅读贡献指南

从这里开始

  1. 先读完整个 Issue，再读项目的贡献指南。
  2. 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
  3. Fork 仓库，在一个分支上完成修改。
  4. 提交 Pull Request，并在描述里引用这个 Issue 编号。

ASC-Community/AngouriMath 的其他 Issue

查看 ASC-Community/AngouriMath 的全部 Issue

相似的 Issue

更多 C# Issue

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。