Skip to content

The growth ceiling is the scheduling policy, and the runaway is bounded to trig - #1194

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
pin-runaway-breadth
Sep 6, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
pin-runaway-breadth

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

#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
this pins the facts so neither branch can be re-proposed from the symptom.

fact measured
The coefficient rules are confluent on plain arithmetic. 2 * x * y, (1/2) * x, 2 * (x * y) / 3 saturate at the widest ceiling in a handful of nodes, with every trigonometric set and with all five removed, extracting 2 * x * y, x / 2, 2/3 * x * y. Making them confluent is not a branch.
The runaway is a family, bounded to the trigonometric sets. sin(2x), sin(x) cos(x), sin(3x), sin(2x) cos(2x) all run away at the widest ceiling; cos(2x) does not; with the five trigonometric sets removed the exemplar saturates at seven nodes.
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.

The third 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, and point at the test.

Four tests, 300 ms between them, on the same 3,000-step ceiling as the ablation. Each failure
message says which way the fact moved and what to do about it — a family member that starts
saturating is to be deleted from the list, not left.

Part of #746.

Checks

Full suite 9578 passed, 0 failed, 14 skipped.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

…ed to trig

#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.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet
Rafael-SOWNet merged commit 72676b0 into master Sep 6, 2026
31 checks passed
Rafael-SOWNet added a commit that referenced this pull request Sep 7, 2026
…asured on the corpus (#1198)

* The e-graph folds a rational on insertion, and the safe ceiling is measured on the corpus

#746 tier 2's next item after declaring growth was to evaluate saturation on what
Simplify actually sees rather than on sixteen expressions. Run over the corpus gate's
forty problems and the two benchmark inputs at the safe ceiling, the graph is cheap --
every one saturates, none above 65 e-nodes, the 473-node SimplifyHard input in 12 ms --
and finds little: 6 of the 15 Simplify problems move and 3 match Simplify's answer,
because what Simplify does on the rest is either fold a number, which no rule does, or
fire a rule the ceiling withholds.

Run over the growth corpus's 3,630 generated shapes, 54 did not saturate within 20,000
steps, and every one of the 54 was constant-only arithmetic: 2 - 0 + 0 * 2,
1/2 * 2 * sin(y), 2 + -2 + (-2) / (-1). With nothing folding a number the rearranging
rules respell it for ever -- 2 * 1/2, 2 / 2 and 1/2 * 2 are three e-nodes -- so on pure
constants the safe ceiling did not terminate, and two inputs overshot a two-second wall
by fifteen and thirty-five times.

So EGraph.Add folds an arithmetic operator over two rational leaves into that number's
class, beside the neutral-element fold it already had: only where the value is itself a
rational (a quotient by zero and an irrational root stay as written), only for a whole
exponent of modest size (2 ^ 100000 is not computed), and never for a node carrying a
codomain of its own, which is the conflation ENodeIdentityTest exists to prevent. The
54 become 7 and the run goes from more than ten minutes to twenty-four seconds; on the
corpus, sqrt(2) * sqrt(3) reaches sqrt(6) and (x ^ 2) ^ 3 - x ^ 6 reaches 0, so the
ceiling moves 7 of 15 and matches Simplify on 5.

What is left is a stall, not a runaway, and it is pinned as one: 2 * x * 1/2,
x / x * -x, x ^ 2 / x and their relatives are a rational coefficient beside a variable
whose spellings -- 1/2 * x, x / 2, x * 2 ^ (-1) -- the Rearranges rules keep exchanging.
Fifteen times the budget still finds no fixed point, but the graph barely grows and
every one extracts the right answer. That corrects one sentence of #1194: the coefficient
rules settle on the three inputs it pinned and are not confluent as a family; the
breadth test, the inverse-pair table and this test now say so.

ConstantFoldTest holds all of it -- what folds, what does not, that the constant-only
inputs saturate, that the stall family stalls, and the corpus figures exactly, so a
declaration that widens or narrows the ceiling shows up as the count it changed.

Part of #746.

Full suite 9601 passed, 0 failed.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

* Record what the constant fold changes, which is almost nothing public

Measured on a build of master (d9b8b37) and of this branch with one throwaway probe
run on each. Transformation.CanonicalizationOverGraph runs the rule pass on either
side of the graph, and that pass already folds constants, so sqrt(2) * sqrt(3),
x + 3 / 3, 2 ^ 1000 and 1 / 0 answer exactly as before; the fold's effect is inside
saturation. The one public change on the inputs probed is (x ^ 2) ^ 3 - x ^ 6, which
was -x ^ 6 + x ^ 6 and is 0, because the graph now sees the two terms as one while
saturating rather than after. Entity.Canonicalize() is unchanged.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant