Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

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

Đang mở
  • Có gì không ổn?
#1,251 1 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
25/100
Loại issue
Tính năng
Độ rõ ràng
Cần làm rõ
Mức độ hoạt động
Sôi nổi
Công nghệ
csharp
Lĩnh vực
backend-api-design

Hướng nghiên cứu

Bắt đầu bằng cách đọc EGraph, Saturation và BudgetOutcome, sau đó so sánh các hướng dẫn trong EqualitySaturationReviewFindings.md và issue #1036. Công việc được xem là hoàn tất khi xác định được truy vấn equality công khai nằm ở đâu, các kết quả về budget và soundness được biểu diễn như thế nào, đồng thời đo chi phí của nó riêng biệt với quá trình đơn giản hóa mặc định.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
C#
Star
831
Fork
79
Merge trung bình
2 giờ 22 phút
Pull request đã merge (30 ngày)
507

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của ASC-Community/AngouriMath

Tất cả issue của ASC-Community/AngouriMath

Issue tương tự

Thêm issue về C#

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.