Take the sign back the right way when both operands are negative (#936) - #937
Merged
Conversation
RewriteRules.NumericNeat.ApplyOnce("-1 + -1") 2 -> -(1 + 1)
RewriteRules.NumericNeat.ApplyOnce("-2 + -3") 5 -> -(2 + 3)
RewriteRules.NumericNeat.ApplyOnce("-1 - (-1)") 2 -> 1 - 1
A wrong answer through public API. `RewriteRules` and `RewriteRuleSet.ApplyOnce` are both public,
and `Transformation.Rewriting(RewriteRules.NumericNeat)` is the documented way to run one rule set.
Two branches, and the arithmetic in each. `(-a) + (-b)` is `-(a + b)`, and the operands are already
negative where the rule matches, so what is added is their magnitudes: written `-(left + right)` it
negated a sum that was negative already. And `(-a) - (-b)` is `b - a`, not `a + b`. Every
neighbouring branch is right -- the four mixed-sign sum and difference cases and the both-negative
product and quotient -- so this is two lines rather than a design problem, and there is a test on the
neighbours so that a later correction cannot fix one sign by breaking another.
**Why nothing caught it, which is the part worth keeping.** `Simplify` and `Evaled` were correct
throughout: the rule only ever fires on numerals, and on numerals evaluation has already produced the
answer before this is consulted. Every harness in `work/` exercises `Simplify`, so none of them could
see it, and the corpora were green on both sides. **A rule that only fires where something else
covers for it can be arbitrarily wrong and never show** -- until a caller applies it alone, which the
transformation layer now lets them do. The test asserts the rule set applied on its own for exactly
that reason, and asserts the value rather than the shape, since writing `-1 + -1` as `-(1 + 1)` is
what the rule is for.
Found by `rulecheck`, a new harness for #746 tier 2, which asks for confluence and termination
"checked by tooling rather than asserted by authors". It applies each rule set to generated
expressions and, for a set declaring Equivalence, compares the value at sample points on and off the
real line. This was two of its findings on the first run; the other eight are non-termination and
want their own issue.
Measured: suite 7024 passed / 0 failed, 13 of them new; casbench 116/119 with 0 wrong, 0 error,
0 timeout; simpsweep 10463/10463 agree; propcheck 1340 checks / 0 failures.
No BREAKING-CHANGES entry for `Simplify`, whose answers do not move. The rule set's own output does,
and that is what the issue and this message record.
#936
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #936. A wrong answer through public API.
RewriteRulesandRewriteRuleSet.ApplyOnceare both public, andTransformation.Rewriting(RewriteRules.NumericNeat)is the documented way to run a single rule set.The arithmetic
(-a) + (-b)is-(a + b), and the operands are already negative where the rule matches, so what is added is their magnitudes. Written-(left + right)it negated a sum that was negative already. And(-a) - (-b)isb - a, nota + b.Every neighbouring branch is right — the four mixed-sign sum and difference cases, and the both-negative product and quotient — so this is two lines rather than a design problem. There is a test on the neighbours so a later correction cannot fix one sign by breaking another.
Why nothing caught it, which is the part worth keeping
SimplifyandEvaledwere correct throughout: the rule only ever fires on numerals, and on numerals evaluation has already produced the answer before this is consulted. Every harness inwork/exercisesSimplify, so none of them could see it — the corpora were green on both sides.A rule that only fires where something else covers for it can be arbitrarily wrong and never show, until a caller applies it alone — which the transformation layer now lets them do. The test therefore asserts the rule set applied on its own, and asserts the value rather than the shape, since writing
-1 + -1as-(1 + 1)is what the rule is for.How it was found
rulecheck, a new harness for #746 tier 2, which asks for confluence and termination "checked by tooling rather than asserted by authors". EveryRewriteRuleSetdeclares aTransformationRelationand aSoundnessand nothing had ever checked either. It applies each set to generated expressions and, for a set declaringEquivalence, compares the value at sample points on and off the real line.These were two of its findings on the first run. The other eight are non-termination —
NumericNeaton--xproduces-1 * 1 * 1 * 1 * ...without settling — and want their own issue.Measured
Suite 7024 passed / 0 failed, 13 new; casbench 116/119 with 0 wrong, 0 error, 0 timeout; simpsweep 10463/10463 agree; propcheck 1340/0.
No
BREAKING-CHANGES.mdentry forSimplify, whose answers do not move; the rule set's own output does, and the issue records that.🤖 Generated with Claude Code