Settle a difference of squared reciprocals instead of denying it (#727) - #728
Merged
Merged
Conversation
lim x->0 (1/x^2 - 1/sin(x)^2) answered NaN, which is not "unevaluated" but the claim that the limit does not exist. It is -1/3. The mirrored difference was the same and csc(x)^2 - 1/x^2 came back unevaluated where it is 1/3. The difference is put over a common denominator already, and what comes out is an ordinary 0/0 -- (sin(x)^2 - x^2) / (x^2 * sin(x)^2). l'Hopital's rule refused its first step. The rule's growth guard allowed eight nodes, which is what growth looks like when the divisor is a power of the variable: differentiating that shrinks it, so only the dividend grows and it grows by addition. A divisor that is a product of vanishing factors grows by the product rule instead, so the chain grows before it collapses -- 17 -> 26 -> 33 -> 46 nodes -- and four steps then settle it. The guard is now the larger of eight nodes and three fifths again, proportional where the growth is proportional and unchanged for the small quotients it was measured on. It is wider than the old rule everywhere, so nothing that answered before is turned away now, and it costs nothing on the shape the flat budget was measured against: x^(3/2) * sqrt(1 + 1/x^2) / x^2 at +oo grows 19 -> 31 nodes at its first step, which is over both budgets, so it stops where it stopped before and still answers 0 in 240 ms. That step adds twelve nodes and the next twenty-six; the old comment's eighteen was measured on an earlier build and is corrected here. The cosecant is a second cause, not the same one. csc(x) is written 1/sin(x) in front of the descent, so csc(x)^2 arrives as (1/sin(x))^2 with its denominator inside the power, and SplitProduct did not look there -- the term was read as having no denominator and the sum was never combined at all. Only whole powers are split this way: (a/b)^n is a^n/b^n exactly for those, while at a half it is not, and the limit of the rewritten form would be the limit of a different function. lim x->0 (1/x^2 - 1/sin(x)^2) NaN -> -1/3 lim x->0 (1/sin(x)^2 - 1/x^2) NaN -> 1/3 lim x->0 (csc(x)^2 - 1/x^2) unevaluated -> 1/3 4855 unit tests and 130 F# tests pass; corpus unchanged at 112/117 with no wrong answers, errors or timeouts, and its total time within noise. 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
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.
Closes #727.
lim x->0 (1/x^2 - 1/sin(x)^2)answeredNaN, which is not "unevaluated" but the claimthat the limit does not exist. It is
-1/3. The mirrored difference was the same, andcsc(x)^2 - 1/x^2came back unevaluated where it is1/3.lim x->0 (1/x^2 - 1/sin(x)^2)NaN-1/3lim x->0 (1/sin(x)^2 - 1/x^2)NaN1/3lim x->0 (csc(x)^2 - 1/x^2)1/3The unsquared forms already answered, so this sits next to #714 rather than being a
regression of it.
Two causes.
The difference is put over a common denominator already, and what comes out is an
ordinary
0/0--(sin(x)^2 - x^2) / (x^2 * sin(x)^2). l'Hopital's rule refused itsfirst step. The rule's growth guard allowed a quotient eight more nodes than the one it
came from, which is what growth looks like when the divisor is a power of the variable:
differentiating that shrinks it, so only the dividend grows and it grows by addition. A
divisor that is a product of vanishing factors grows by the product rule instead, so
the chain grows before it collapses --
17 -> 26 -> 33 -> 46nodes -- and four stepsthen settle it. The guard is now the larger of eight nodes and three fifths again:
proportional where the growth is proportional, unchanged for the small quotients it was
measured on.
That rule is wider than the old one everywhere, so no chain that reached an answer before
is turned away now, and it costs nothing on the shape the flat budget was measured
against:
x^(3/2) * sqrt(1 + 1/x^2) / x^2at+oogrows19 -> 31nodes at its firststep, over both budgets, so it stops where it stopped before and still answers
0in240 ms.
The cosecant is a separate cause.
csc(x)is written1/sin(x)in front of the descent,so
csc(x)^2arrives as(1/sin(x))^2with its denominator inside the power, andSplitProductdid not look there -- the term was read as having no denominator and thesum was never combined at all. Only whole powers are split this way:
(a/b)^nisa^n/b^nexactly for those, while at a half it is not (sqrt(1/(-1))isiandsqrt(1)/sqrt(-1)is-i), and the limit of the rewritten form would be the limit of adifferent function.
Measured. 4855 unit tests and 130 F# tests pass. The 117-problem solver corpus is
unchanged at 112/117 with no wrong answers, errors or timeouts, and its total time is
within noise of where it was.
🤖 Generated with Claude Code