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

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

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

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

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

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
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時間 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 を短くまとめたダイジェスト。