Repository navigation
The saturation runaway is one inverse pair across two sets, not a tier (#746) - #1193
Merged
Merged
Conversation
#746 tier 2's remaining item was phrased as "a scheduling policy for Expands/Unknown rules", on the observation that sin(2x) + cos(2x) reaches 254 e-nodes at the widest ceiling without saturating -- and extracts the input unchanged, so the blow-up finds nothing. Ablating every set in turn says the unjudged rules are not the cause as a class: remove any one of Common, ExpandMultipleAngle or Trigonometric and it saturates at about twenty nodes; remove CollapseMultipleFractions and it gets worse, 618, because that set was a brake. Ablating the rules of those three sets one at a time names four. ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle sin(2x) -> 2 sin x cos x Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-... sin x cos x -> sin(2x) / 2 Common / a-numeric-factor-floats-out-of-a-product-of-functions the 2 goes out Common / a-reciprocal-rational-factor-is-a-division the 1/2 becomes / 2 The first two are an exact inverse pair. An e-graph is supposed to absorb one -- both directions land in a class and it stops -- and this one is not absorbed because its two forms differ by a coefficient the two Common rules rearrange non-confluently, so every pass makes a fresh spelling rather than a merge. That is a precise thing, and it is the first cross-set inverse pair anything here has measured. InversePairTable.md says the single-set observation "never meets" a pair split across two sets, and saturation meets it because it runs every set at once; the document records the pair now, and says so. Pinned in both directions by SaturationAblationTest: the runaway is a known non-saturation, each of the four rules is asserted load-bearing for it, and no other rule of the three sets is -- so fixing the pair deletes entries rather than leaving names that mean nothing, and a fifth rule joining the cycle fails. The load-bearing list checks each name still exists in the registry, so a rename cannot leave it asserting about nothing. What this does not do is fix the pair. Which direction to withhold from saturation -- or whether to make the coefficient rules confluent so the graph can absorb it -- is the decision the table is for, and it is a smaller one than the item it replaces. Part of #746. Full suite 9574 passed, 0 failed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 6, 2026
…ed to trig (#1194) #1193 named the four rules behind sin(2x) + cos(2x) running away at the widest ceiling and left the decision open: withhold one direction of the inverse pair, or make the two Common coefficient rules confluent so the graph could absorb it. Measuring how broad the runaway is settles both, and the facts are pinned so neither branch can be re-proposed from the symptom. The coefficient rules are confluent on plain arithmetic. 2 * x * y, (1/2) * x and 2 * (x * y) / 3 saturate at the widest ceiling in a handful of nodes, with every trigonometric set present and with all five removed, and extract 2 * x * y, x / 2 and 2/3 * x * y. They were load-bearing in the runaway only because they supplied the respellings the trigonometric pair fed on; making them confluent is not a branch. The runaway is a family and it is bounded to the trigonometric sets. sin(2x), sin(x) cos(x), sin(3x) and sin(2x) cos(2x) all run away at the widest ceiling, cos(2x) does not, and with Trigonometric, ExpandMultipleAngle, ExpandTrigonometric, CollapseTrigonometricFunctions and NormalTrigonometricForm removed the exemplar saturates at seven nodes. And the safe ceiling already withholds the expanding direction. ExpandMultipleAngle's rules are declared Expands, so RulesUpTo(Rearranges) fires only the collecting one and every member of the family saturates there. That was inferred from the declarations when #1193 went in; RunawayBreadthTest asserts it now. Growth is the direction marker and the ceiling is the scheduling policy, mechanically, for every pair whose two directions are declared -- a pair whose expanding direction is unjudged is the one case it cannot protect, which is what declaring a growth for a rule is for. The RulesUpTo remark and InversePairTable.md say so. Four tests, 300 ms between them, bounded by the same 3,000-step ceiling as the ablation. Each failure message says which way the fact moved and what to do about it. Part of #746. Full suite 9578 passed, 0 failed. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 7, 2026
…s measured (#1203) EMatching.md deferred whether Expands rules ever join SafeRules to "a separate document's question, once one exists", and Transformations.md's list of what is left said the graph had no production caller. Both were true when written and are not now: #1193 and #1194 measured that the growth ceiling is the scheduling policy and that Expands rules do not join the safe set; #1198 and #1202 found what the graph did need -- a rational folded on insertion and an extraction that is a fixed point from the leaves up -- by running the safe ceiling over the corpus; and #1201 gave the graph its first production caller. The documents point at those rather than at a question nobody is going to open. Part of #746. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <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.
#746 tier 2's remaining item was phrased as "a scheduling policy for
Expands/Unknownrules", onthe observation that
sin(2x) + cos(2x)reaches 254 e-nodes at the widest ceiling withoutsaturating — and extracts the input unchanged, so the blow-up finds nothing.
Ablation says the unjudged rules are not the cause as a class. Remove any one of
Common,ExpandMultipleAngleorTrigonometricand it saturates at about twenty nodes. RemoveCollapseMultipleFractionsand it gets worse — 618 — because that set was a brake. Ablating therules of the three sets one at a time names four:
ExpandMultipleAngle/sine-of-a-whole-multiple-of-an-anglesin(2x)→2 sin x cos xTrigonometric/a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sinesin x cos x→sin(2x) / 2— the exact inverseCommon/a-numeric-factor-floats-out-of-a-product-of-functions2outCommon/a-reciprocal-rational-factor-is-a-division1/2into/ 2Why an e-graph doesn't just absorb it
It is supposed to: both directions of an inverse pair land in one class and the graph stops. This
pair is not absorbed because its two forms differ by a coefficient, and the two
Commonrulesrearrange that coefficient non-confluently — so every pass produces a fresh spelling rather than
a merge.
That is a precise thing, and it is the first cross-set inverse pair anything here has measured.
InversePairTable.mdsays the single-set observation "never meets" a pair split across two sets;saturation meets it because it runs every set at once. The document records the pair now.
Pinned in both directions
SaturationAblationTest: the runaway is a known non-saturation; each of the four rules is assertedload-bearing for it; and no other rule of the three sets is — so fixing the pair deletes entries
rather than leaving names that mean nothing, and a fifth rule joining the cycle fails. The
load-bearing list checks each name still exists in the registry, so a rename cannot leave it
asserting about nothing.
Cost to the suite: one second. The first version cost five minutes, because a non-culprit
ablation leaves the runaway intact and burned a three-second wall, a hundred times over. The runaway
is past 250 nodes by 30k steps and a saturating run needs a few hundred, so a 3,000-step ceiling
separates them cleanly and the wall is a backstop.
What this does not do
It does not fix the pair. Which direction to withhold from saturation — or whether to make the
coefficient rules confluent so the graph can absorb it — is the decision the inverse-pair table is
for. It is a much smaller decision than "a scheduling policy for two tiers of rules", which is the
point of having measured it.
Part of #746.
Checks
Full suite 9574 passed, 0 failed, 14 skipped. The three new tests take one second between them.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura