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

SoundUnderAssumptions names no assumption: 177 rules declare it and the condition exists only in comments

Đang mở
  • Có gì không ổn?
#1,252 2 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
30/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

Hướng nghiên cứu

Bắt đầu bằng cách đọc RewriteRule, RewriteStep, DerivationPath và đường dẫn metadata thông qua RuleRegistryGenerator, sau đó kiểm tra MatchedRules.cs cùng RuleConfluenceTest và RuleSetTerminationTest hiện có. Bước đầu tiên là xác định liệu các điều kiện thuộc về các rule hay được suy ra ở các bước rewrite; bước này chỉ được xem là hoàn tất khi có một thiết kế được thống nhất trước khi audit 177 khai báo.

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

Mô tả

Measured on 2dbeedf7: 177 rule declarations carry Soundness.SoundUnderAssumptions, against 188 that carry Soundness.Sound. Nothing records what any of those 177 assumptions are.

The tier is machine-readable. The assumption is prose. From MatchedRules.cs:

MatchPattern.Node<Divf>(MatchPattern.Any("a"), MatchPattern.Any("b")),
// a * (1/b) and a/b are undefined at exactly the same points, but the quotient
// is a quotient either way, so this inherits division's own condition rather
// than adding one. Left at the conservative tier until the audit reaches it.
Soundness.SoundUnderAssumptions,

RewriteRule exposes Soundness, Growth, GuardSource, PatternSource, ReplacementSource, SourceLine — and GuardSource is a string of source text, not a condition that can be evaluated, conjoined or checked.

Why this is the blocking piece rather than a tidiness complaint

#746's tier 5 asks for derivations "a third party can replay step by step and independently check". A step can currently be replayed but not checked: RewriteStep says which rule fired and that it was conditional, and there is no way to ask what has to hold for the answer to be right. The difference matters most exactly where it is hardest to see — a rewrite that is fine on the reals and wrong across a branch cut is SoundUnderAssumptions today, and the answer carries no trace of which reading it assumed.

That comment above is also its own evidence: it says the tier was chosen conservatively pending an audit that never happened. With 177 of them, prose cannot say which are genuinely conditional and which are unlabelled Sound, so the tier is currently a lower bound with unknown slack, and the weakest-across-a-step rule in DerivationPath propagates that slack to every answer.

What already exists to build it out of
  • DomainConditionIn(Domain) (#1090) applies a reading throughout a tree and narrows without widening — so "what must hold of the operands" is computable for a great many of these rather than needing to be authored by hand.
  • Providedf is already the node for an expression carrying a condition, and already travels through simplification.
  • Rules are data now (all 30 sets run the matcher), so a per-rule field has one place to go and RuleRegistryGenerator already reads per-rule metadata.
  • RuleConfluenceTest / RuleSetTerminationTest are precedent for checking a declaration by tooling instead of trusting the author — a declared condition can be tested numerically, by sampling points where it fails and asserting the rewrite changes the value there. A rule whose stated assumption cannot be falsified anywhere is a rule that was probably Sound all along.
Suggested shape, for discussion

Give RewriteRule an optional condition alongside Soundness — an Entity over the pattern's bound names, so the rule a/b -> a * (1/b) states b != 0 rather than describing it. Then:

  • a rule declaring SoundUnderAssumptions and no condition is a build failure once the audit is done, which is what makes the audit finish;
  • RewriteStep can expose the instantiated condition, and DerivationPath can conjoin them, so a path ends with the assumptions its answer rests on;
  • the numeric check above becomes a test, so the declaration is evidence rather than a claim.

Not proposing to land this at once — the audit is 177 rules. The first question is whether the condition belongs on the rule at all, or whether it should be derived from DomainConditionIn at the step.

Part of #746, tier 5.

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.