asc-community / asc-community/AngouriMath
SoundUnderAssumptions names no assumption: 177 rules declare it and the condition exists only in comments
- Dominant language
- C#
- Stars
- 831
- Forks
- 79
- Avg merge
- 3h 23m
- Merged PRs (30d)
- 309
Description
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`:
```csharp
MatchPattern.Node(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.
Contributor guide
Research direction
Start by reading RewriteRule, RewriteStep, DerivationPath, and the metadata path through RuleRegistryGenerator, then inspect MatchedRules.cs and the existing RuleConfluenceTest and RuleSetTerminationTest. The first step is to resolve whether conditions belong on rules or are derived at rewrite steps; done requires an agreed design before auditing the 177 declarations.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- csharp
- Domain
- backend
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Active
- Clarity
- Needs clarification
- Newbie friendliness
- 30/100