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

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

未关闭
#1,252 2 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看

维护者通常 1 天内回复

还没有人认领这个 Issue。

评估

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

调研方向

先阅读 RewriteRule、RewriteStep、DerivationPath 以及通过 RuleRegistryGenerator 的元数据路径,然后检查 MatchedRules.cs 和现有的 RuleConfluenceTest 与 RuleSetTerminationTest。第一步是确定条件属于规则,还是在重写步骤中推导出来;只有在审查 177 个声明之前形成一致认可的设计后,这一步才算完成。

由索引模型根据 Issue 内容生成。

描述

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.

主要语言
C#
星标
831
派生
79
平均合并
2 小时 17 分钟
30 天内合并 PR
443

环境准备

  • 没有 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 摘要。