Bound a gcd's intermediates separately from its inputs (#920) - #923
Merged
Conversation
PolynomialGcd.Gcd declined on inputs well inside every documented limit, because an
intermediate of the subresultant remainder sequence went past MultivariatePolynomial.MaxTerms
while neither input nor answer came close:
left (b + c + 1) * (a + b) * (a + b + c + d) 19 terms
right (a^2 + b*c + d) * (a + b + c + d) * (a + b + c + d) 29 terms
gcd a + b + c + d 4 terms was declined
A multivariate pseudo-remainder multiplies through by a leading coefficient that is itself a
polynomial. The subresultant divisions bound how large the coefficients get -- which is what
the class remark is about, and it holds -- but nothing bounds the monomial count, and three
steps in a 25-term lead times a 159-term remainder passes 512.
Raising MaxTerms is the one-line version and it is the wrong shape, which the measurement
shows rather than the reasoning: at 2048 three documented refusals become answers, including
TermCountsPastTheCeilingAreRefused, whose subject is a direct product of two 495-term inputs,
and RefusedRatherThanAnsweredWrongly, whose input has 1001 terms and is meant to be stopped at
the door. The bound on what may be *asked* was never too small. What was too small was the
bound on what may be passed through on the way to an answer that is itself small.
So MaxIntermediateTerms is a second constant, 4096, threaded as an optional argument through
Multiply, Power and DivideExact and passed only by the gcd's remainder sequence. Everything
reached any other way keeps MaxTerms by default, so the entry bound that protects the hot path
is untouched and all three of those refusals still refuse.
3000 drawn triples 7 declined -> 0 declined
the pair above declined -> a + b + c + d, checked as a greatest common divisor
The sweep now asserts the count is zero rather than at most seven, so a refusal coming back
fails there instead of passing quietly under a ceiling.
Performance, which is the part #920 asked not be guessed at: TryCancel runs on every quotient
the simplifier builds, so simpsweep is the hot path. Two runs at 4096 took 3m26.8s and 3m40.7s,
one at 512 took 3m45.3s. The spread between repeats of the same setting is as large as the gap
between the settings, so this supports no regression and does not support a speedup. The gcd
test class is unchanged at 1 s.
Verified: 6944 C# tests and 130 F# tests pass, 0 fail. propcheck 1340 checks 0 failures,
simpsweep 10463/10463 agree 0 disagreements, rootcheck 596/596 clean, casbench 117/119 with
0 wrong, 0 error and 0 timeout.
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 14, 2026
…rary is (#746) (#928) * State what canonical form means here, and measure how far off the library is (#746) #746's tier 1 asks for "canonical forms with a written specification of what canonical means for each node class, and a stated distinction between canonical and simplest", and its item 65 asks whoever does it to take a position, write it down, and let the engine be checked against it. This is the document; the checking is a new harness in the analysis workspace, and every number here came out of it rather than out of an argument. **The position.** Canonical is about identity and simplest is about presentation. A canonical form exists to make equality a structural comparison; a simplest form is the best-rated member of a class under a cost metric that the caller chooses, so it is only defined relative to one. **A complete canonical form does not exist, and that is a theorem rather than a gap.** Zero- equivalence is undecidable for the class the library accepts -- rationals, pi, exp, the trigonometric functions, abs and composition (Richardson 1968) -- and a canonical form would decide it. So the specification is a canonical form on a decidable sublanguage with the boundary written down, a normalisation everywhere else that must not be mistaken for one, and a search that is not required to be canonical at all. That is Moses' three-way split from 1971 and it costs nothing but saying so. **Three properties, none needing an oracle, measured against both candidates:** InnerSimplified Simplify idempotence 1 failed of 834 0 failed of 120 order independence 2024 failed of 2738 8 failed of 72 listed agreements 20 failed of 30 6 failed of 30 Neither is canonical, and Simplify is much the closer of the two -- which is the opposite of what the names suggest. InnerSimplified does not order the operands of a sum or a product at all, so it fails three quarters of the order checks by construction. Simplify reorders as a side effect of rating candidates, and its eight failures are all ties settled by generation order. **The finding that matters most to anyone writing a rule or a test:** `(x + y) + a` and `x + (y + a)` both print as `x + y + a` and are different trees. Associativity is normalised in the printer, not in the expression, so a comparison of printed forms calls them equal and a comparison of entities does not. The harness compares entities, which is why it saw this. **Two defects rather than decisions**, each measured and each reproducible on its own: cos(0 ^ y).InnerSimplified -(-1) provided ... then 1 provided ... not idempotent cos(-x).Simplify() cos(-x) while cos(-2 * x) -> cos(2 * x) The first is a rewrite building `-(-1)` above already-normalised children and returning without re-normalising; `-(-1)` on its own folds immediately. The second is the parity identities keyed on a shape a bare negation does not have -- sin, tan and abs behave the same way. Per node class the file states the target rather than describing today, marking each line met or not. One line is flagged as needing a maintainer's yes before anyone implements it: making subtraction and division sugar for a sum and a product, which is what makes the commutative laws reachable and is also a breaking change to everything that matches on Divf. And it names where a canonical form is actually available now: rational functions over Q, where zero-equivalence is decidable and the parts -- multivariate GCD, expansion, a monomial order -- landed with the polynomial layer in #918 and #923. That is the piece to build first because it is the piece that is possible. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Correct the specification: the total order exists, and the obstacle is confluence (#746) The first version of this file said a total order on operands was owed. It is not: the library has one, at three granularities, and measuring it changes what the document should ask for. `RewriteRules.CanonicalOrderExact` sorts and groups the operands of sums, products, conjunctions, disjunctions and set operations by the whole subtree. Applied before the normalisation it makes order independence **perfect** -- 0 failures of 2738, against 2024 without it. So the piece a specification would normally have to invent is built; what is missing is that the normalisation does not run it, which is also most of why `Simplify` agrees so much more often than `InnerSimplified`. And the reason it cannot simply be moved there is now measured rather than guessed at. Sorting and then normalising is **not idempotent** -- 21 of 834 -- and every failure is the same phenomenon, the sort and `Patterns.NumericNeatRules` disagreeing about where a numeric operand belongs and each undoing the other: 1 / 2 - x -> -x + 1/2 -> 1/2 + -x -> ... Neither is wrong on its own. Until they are made to agree, applying the order inside the normalisation trades 2024 order failures for a form that never settles. So §8's first item is no longer "specify and implement a total order" but "make the order and the normalisation confluent", which is a much smaller and much better defined question, and it is the one actually in the way of everything else in tier 1's canonicaliser. The measurement table gains the third column, §4's commutative rows say ordered-but-not-run rather than not-ordered, and §7 records that the harness now runs all three properties over all three candidate forms -- the differences between the columns being the point rather than any one number. Also: the two defects §3 lists are fixed, in #929 and #930, so the table is labelled with the build it was taken on and with what it reads without them. A harness report records a build. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Compose the canonicaliser out of what exists: normalise, order, normalise (#746) The previous revision said the order and the normalisation had to be made to agree, and left that as the open question. It is not a disagreement between rules and nothing has to be decided between them. The sort's key depends on a node's class and the normalisation changes classes. In 1/2 - x the constant reaches the sort as 1 * 2 ^ (-1), a product, and is ordered against -x as one; the normalisation folds it to the number 1/2, and the next sort orders it the other way. So the sort was ordering a shape about to stop existing. Normalising first gives both properties at once: InnerSimplified order then normalise normalise, order, normalise idempotence 0 of 834 21 of 834 0 of 834 order independence 2024 of 2738 0 of 2738 0 of 2738 x + (-1/2), whose constant is already a number when the sort reads it, was stable throughout, which is the control that makes this the explanation rather than a guess. So §8's first item is now to expose that composition as the canonicaliser rather than to reconcile anything. It needs no rule changed. What it needs is a decision about where it runs: opt-in changes nothing, and inside InnerSimplified every commutative operand order in every printed answer moves at once. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * The canonicaliser reaches associativity too, and it now exists (#746) Two corrections, both from a test that failed the way round I did not expect. Nesting goes with order. The sort works over commutative *chains* rather than over one node, so it flattens as it sorts: (x + y) + a and x + (y + a) both reach a + x + y and reach it as the same tree. I had written a test asserting they stay different and it failed, which is how this was found. So flattening is no longer owed -- what is owed is that InnerSimplified on its own does neither, and InnerSimplified is what every rule and every cache in the library actually sees. And the composition now exists under a name, Transformation.Canonicalisation (PR #933), so §8's first item is no longer to build it but to decide where it runs. Offering it changes nothing; putting it inside InnerSimplified moves every commutative operand order in every printed answer at once. The warning in §3 stands unsoftened for the same reason: the canonicaliser makes those two trees one, and almost nothing calls the canonicaliser. #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Name what is actually missing for the rational-function form (#934) §8's remaining build item is smaller and more specific than 'a rational-function canonical form'. The greatest common divisor is already there and already verifies itself; what is missing is that nothing in the library puts an expression over a common denominator, so 1/x + 1/y and (x+y)/(x*y) cannot be brought to a common form by any existing route -- measured through Simplify, InnerSimplified and Factorize alike, and Simplify actively prefers the split form. Filed as #934 with the design and that measurement, so the next person starts from what is missing rather than from what it is called. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> --------- 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
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 #920.
PolynomialGcd.Gcddeclined on inputs well inside every documented limit, because an intermediate of the subresultant remainder sequence went pastMultivariatePolynomial.MaxTermswhile neither input nor answer came close:A multivariate pseudo-remainder multiplies through by a leading coefficient that is itself a polynomial. The subresultant divisions bound how large the coefficients get — which is what the class remark is about, and it holds — but nothing bounds the monomial count, and three steps in, a 25-term lead times a 159-term remainder passes 512.
Why not just raise
MaxTerms#920 offers that as the one-line option and asks for a measurement rather than a guess. The measurement rules it out. At
MaxTerms = 2048, three documented refusals become answers:TermCountsPastTheCeilingAreRefused— whose subject is a direct product of two 495-term inputsRefusedRatherThanAnsweredWrongly— whose input has 1001 terms and is meant to be stopped at the doorOnly the third is the bug. The bound on what may be asked was never too small; what was too small was the bound on what may be passed through on the way to an answer that is itself small.
The shape
MaxIntermediateTerms = 4096is a second constant, threaded as an optional argument throughMultiply,PowerandDivideExact, and passed only by the gcd's remainder sequence. Everything reached any other way keepsMaxTermsby default, so the entry bound protecting the hot path is untouched and all three refusals above still refuse.The sweep now asserts the count is zero rather than at most seven, so a refusal coming back fails there instead of passing quietly under a ceiling. The pinned refusal test is rewritten to assert the answer deliberately, as its own remark asked for.
Performance
TryCancelruns on every quotient the simplifier builds, sosimpsweepis the hot path.The spread between repeats of the same setting is as large as the gap between the settings. This supports no regression; it does not support a speedup, and I am not claiming one. The gcd test class is unchanged at 1 s.
Verification
propcheck1340 checks, 0 failuressimpsweep10463/10463 agree, 0 disagreements, 0 timeoutsrootcheck596/596 clean, 0 incomplete, 0 unsoundcasbench117/119, 0 wrong, 0 error, 0 timeout🤖 Generated with Claude Code