Repository navigation
Seven rules say how much they expand (#825) - #1159
Merged
Merged
Conversation
Growth is `Unknown` for a code replacement unless it is declared, and 262 rules sat there. Seven of them can say what they do, each argued from the shape of the replacement rather than from the corpus, and each measured against the corpus as well. Two mechanisms, the same arithmetic. Six are negation rules -- (-a) + (-b), (-a) - x, and the four that bring a negative factor out of a product, a numerator or a denominator -- where the operators map one for one, the literal is replaced by its magnitude, and the negation the replacement puts round the whole of it is two nodes. The seventh is a ^ n = 1 / a ^ (-n), where the power stays a power with its exponent replaced one for one and the quotient and its numerator are the two. Expands rather than the other two on purpose, and not only because it is what they do. Saturation.RulesUpTo builds its set as the rules up to Rearranges, so Collects and Rearranges are declarations that change which rules equality saturation fires while Expands is one that does not. These seven record what was already true without moving anything, which is the right first batch; the ones that would change the saturation want it measured before and after, and that is a separate change. An eighth was measured at +2 on all 18 of its firings and is left alone. `a-negated-reciprocal-rational-factor-is-a-negated-division` counts five nodes to five when I work through its pattern, so the measurement and the reading disagree and I cannot argue the claim. WritingARule.md says to leave such a rule Unknown, and that applies to the person who wrote the sentence. Full suite 9552 passed, 0 failed. Part of #825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
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
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.
Growth is
Unknownfor a code replacement unless it is declared, and 262 rules sat there. Seven cansay what they do. 255 now do not.
Argued from the code, measured against the corpus
Two mechanisms, the same arithmetic.
Six negation rules —
(-a) + (-b),(-a) - x, and the four that bring a negative factor out ofa product, a numerator or a denominator. The operators map one for one, the literal is replaced by
its magnitude, and the negation the replacement puts round the whole of it is two nodes:
One power rule —
a ^ n = 1 / a ^ (-n). The power stays a power with its exponent replaced onefor one; the quotient and its numerator
1are the two.Each was also run against the generated corpus by
RuleGrowthAgreesWithTheCorpusTest, between 9 and84 firings apiece, none contradicting. That is corroboration and not the argument — the corpus can
only refute.
Why
Expandsis the right first batchNot only because it is what they do.
Saturation.RulesUpTobuilds its set as the rules up toRearranges, so:CollectsorRearrangesadds a rule to what equality saturation fires;Expandschanges nothing about what runs.These seven record something that was already true without moving anything. The
CollectsandRearrangescandidates in the measurement are real too, but each of those is a behavioural changeand wants the saturation measured before and after — a separate PR, not a line in this one.
The eighth, left alone
a-negated-reciprocal-rational-factor-is-a-negated-divisionmeasures +2 on all 18 of itsfirings, which is exactly the evidence the other seven have. It stays
Unknown.Working through its pattern I count five nodes to five, so the measurement and my reading of the
code disagree, and I cannot argue the claim.
WritingARule.mdsays that where you cannot argue itfrom the code you leave it
Unknown— and that sentence was written in the previous PR, by me, soit applies here first.
Declaring it on corpus agreement alone would be the same mistake #1158 caught: a growth asserted
from what it looked like rather than from what it does.
Verification
Full suite 9552 passed, 0 failed, 14 skipped. The census moves 262 → 255 in
WritingARule.mdandRuleAuthoringGuideTest.Part of #825.