Repository navigation
A graph transformation stops when its answer has, not only when the graph has - #1206
Merged
Merged
Conversation
…raph has #1200's inputs -- a rational coefficient beside a variable, x / x * -x, x ^ 2 / x -- run away at the safe ceiling: the quotient-regrouping rules recombine members across classes, so every pass adds fresh e-nodes to the root's class for as long as the budget allows. Traced on x ^ 2 / x, the root extracts x from the third pass on and never stops gaining members. A caller who extracts an answer was paying the whole budget, two seconds, for an answer it had in milliseconds. Saturation.Run takes a caller's own stop, asked after every pass that merged something, and the two transformations that extract -- EqualitySaturation, the cheapest member, and CanonicalizationOverGraph, the least -- pass "the extraction has not changed for two passes". Two rather than one, because a pass can leave the chosen member alone while adding what the next pass improves on. ProvesEqual passes nothing: it needs a union, not an extraction, and keeps saturating. Measured on the corpus gate's forty problems, the nine inputs of #1200 and the five pinned ordinary ones, through both public transformations: every answer identical, and the run of all of them 13,495 ms to 320 ms -- x / x * -x 1,869 to 10 ms, x ^ 2 / x 2,010 to 3 ms, 2 ^ (-1) / sqrt(1/2) 998 to 2 ms. The remark on CanonicalizationOverGraph says what its canonical form is now modulo: these rules, this budget, and the answer having settled. What this does not do is make the rules confluent on that family; the bare graph still runs away and ConstantFoldTest still says so. #1200 stays open as the question about the rules, with its practical cost gone. Part of #746. Full suite 9610 passed, 0 failed. Co-Authored-By: Claude Fable 5.1 <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
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.
The runaways of #1200, made cheap for the callers that matter — without pretending the rules are
confluent.
What the trace showed
x ^ 2 / xat the safe ceiling: the root's class extractsxfrom pass 3 and never stops gainingmembers — the quotient-regrouping rules (
a/(b/c),(a/b)·c,(a/b)/(c/d)…) recombine membersacross classes, so every pass adds fresh e-nodes for as long as the budget allows (nodes 68 → 247
in one pass; 12k in 30 s). A caller who extracts an answer paid the whole budget for an answer it
had in milliseconds.
What changes
Saturation.Runtakes a caller's own stop, asked after every pass that merged something. The twotransformations that extract —
EqualitySaturation(cheapest member) andCanonicalizationOverGraph(least member) — pass "the extraction has not changed for two passes".Two, not one: a pass can leave the chosen member alone while adding what the next pass improves
on.
ProvesEqualpasses nothing — it needs a union, not an extraction — so the perfect-squarecaller (#1201) is unaffected.
Measured
Corpus gate's 40 problems + the 9 inputs of #1200 + the 5 pinned ordinary ones, through both
public transformations, before and after:
x / x * -xx ^ 2 / xx / x * x * 1/22 ^ (-1) / sqrt(1/2)(saturation)The remark on
CanonicalizationOverGraphnow says what its canonical form is modulo: these rules,this budget, and the answer having settled. No
BREAKING-CHANGES.mdrow: no value moved.What it does not do
It does not make the coefficient rules confluent; the bare graph still runs away on this family
and
ConstantFoldTeststill pins that. #1200 stays open as the question about the rules — anormal form for a coefficient's spellings, or an orientation — with its practical cost gone.
Part of #746.
Checks
Full suite 9610 passed, 0 failed, 14 skipped — every pin on the bare graph (ablation, breadth, constant fold, canonical extraction) unchanged, since
Saturation.Runwithout a stop is what they call.🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura