Repository navigation
Stop reading an indeterminate power form off as its value (#754) - #760
Conversation
Where nothing else had a reading of a limit, it was answered by substituting the destination and evaluating. That is right wherever the expression is continuous there, and an indeterminate form is exactly where it is not. Almost all of them already declined without any help, because they evaluate to NaN and every caller reads NaN as "no limit": 0 * oo, oo - oo, oo / oo, and 0^0. The two that do not are oo^0 and 1^oo, which this library's arithmetic answers with 1, so a limit that assembled either read that 1 off as its answer: lim x->+oo (e^x)^(1/ln(x)) was 1, is +oo lim x->+oo (x^2)^(1/ln(x)) was 1, is e^2 lim x->+oo (x!)^(1/x) was 1, is unevaluated -- it is +oo lim x->+oo (x!)^(1/ln(x)) was 1, is unevaluated -- it is +oo (x^2)^(1/ln x) is e^(2*ln(x)/ln(x)), that is e^2 at every x, so the old answer was not merely imprecise; (x!)^(1/x) grows like x/e by Stirling, and (100!)^(1/100) is already 37.99. Both were verified numerically rather than argued. Guarded at the two places that assemble such a form: SolveBySubstitution, which puts the destination into the whole expression, and the Powf descent, which puts each part's own limit in place of the part. The sum, the product and the quotient were already guarded there by IsDeterminate; the power was not. What this does not do is change what (+oo)^0 or 1^oo evaluate to as expressions. Both are still 1, the same convention SymPy and IEEE 754's pow use -- the change is that a limit no longer reads its answer off one. 0^0 is deliberately left out for the opposite reason: its NaN is how the library says lim x->0 x^x does not exist, pinned by LimitTest.TestNoLimit, and declining it would turn a considered "does not exist" into "not settled". Guarding it broke exactly those three tests, which is what located the distinction. The cost, recorded in BREAKING-CHANGES.md: three limits answered 1 are now unevaluated. (x!)^(1/x^2) is 1 and was right by luck -- the same substitution gave 1 for (x!)^(1/x), where the answer is +oo, and the two are indistinguishable where the value is read off; answering it wants the Stirling expansion, which is #754's second half. The other two are two-sided limits at 0 whose base has no two-sided limit and which are not real to the left of 0, and their one-sided readings are unchanged. Measured over 225 generated powers at 0 and +oo: 2 wrong values -> right ones, 3 wrong values -> unevaluated, 1 NaN -> unevaluated, 3 right values -> unevaluated. Unit tests 5201 -> 5225 passing with 24 added, F# 130, casbench 112/117 with 0 wrong, propcheck 0 failures, rootcheck 596/596, simpsweep 0 disagreements. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
One thing worth flagging for review, since the measurement does not show it. The It is included anyway because it is the same defect — an indeterminate form whose arithmetic gives If you would rather this PR stayed strictly to the |
A power whose base holds a factorial had no limit at all. f^g is e^(g * ln f), and SolveAsIndeterminatePower computes the limit of that exponent -- but every route out of ln(f) runs through differentiating f, and a factorial's derivative wants the digamma function, which this library does not have. The rule declined and nothing behind it had a reading either, so lim x->+oo ((x!)/x^x)^(1/x) was the last lim:factorial miss in the corpus. Stirling's expansion is stated for exactly that logarithm: ln(f!) = f*ln(f) - f + ln(2*pi*f)/2 + 1/(12f) + O(1/f^3). Applied to the exponent rather than substituted for the factorial in the base, and that is the whole of what makes it sound -- what is dropped here *vanishes*, where the asymptotic for f! itself has an error that is merely relative and survives being raised to a power. Vanishing is still not sufficient, because the dropped term is multiplied by the exponent the rewrite sits under: an error of 1/(12f) in the logarithm contributes power/(12f) to the exponent, so power/f -> 0 is required. For ((x!)/x^x)^(1/x) that ratio is 1/x^2. (x!)^x fails it and is left alone. The factorial's own logarithm is not visible until the logarithm of the base is taken apart -- ln(x!/x^x) is one node and nothing simplifies it -- so ln is split over products, quotients and powers, confined to logarithms that actually hold a diverging factorial. That split assumes the parts are positive on the approach, which is the same assumption the simplifier's ln(a) + ln(b) = ln(a*b) already makes, and it is reached only by expressions that have no answer at all without it. Three tests from PR #760 pinned these as unsettled and are updated rather than loosened: each is now answered, and (x!)^(1/x^2) -- recorded there as the one thing that change cost, right by luck rather than by reading -- comes back as 1 by reading. Every value checked numerically at up to x = 1e9 before being claimed, since SymPy 1.14.0 answers (x!/x^x)^(1/x) with 0 and is not a usable oracle here. Measured over 225 generated powers: six results differ from master and all six are an unevaluated node becoming a value, with no answer changed. casbench 112/117 -> 113/117 with 0 wrong. Unit tests 5291 -> 5307 passing with 16 added, F# 130, propcheck 0 failures, rootcheck 596/596, simpsweep 0 disagreements. Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Fixes the first half of #754 — the wrong answer. The corpus miss (its second half) needs Stirling's expansion of
ln(x!)and is left for its own PR, as the issue itself proposes.What was wrong
Where nothing else had a reading of a limit, it was answered by substituting the destination and evaluating. That is right wherever the expression is continuous there, and an indeterminate form is exactly where it is not.
Almost all of them already declined without any help, because they evaluate to
NaNand every caller readsNaNas "no limit":0 * oo,oo - oo,oo / oo,0^0. The two that do not areoo^0and1^oo, which this library's arithmetic answers with1— so a limit that assembled either read that1off as its answer:(x^2)^(1/ln x)ise^(2*ln(x)/ln(x)), that ise^2at everyx, so the old answer was not merely imprecise.(x!)^(1/x)grows likex/e—(100!)^(1/100)is already37.99. Both checked numerically at up tox = 1e9rather than argued.Where it is guarded
The two places that assemble such a form:
LimitSolvers.SolveBySubstitution, which puts the destination into the whole expression — this is where(x!)^(1/x)became(+oo)!^(1/(+oo));Powfdescent inLimit.Classes.cs, which puts each part's own limit in place of the part. The sum, the product and the quotient are already guarded there byIsDeterminate; the power was not.Both were needed — fixing only the first left the descent to reassemble
(+oo)!^0for itself.What it deliberately does not do
It does not change what
(+oo)^0or1^ooevaluate to. Both are still1, the same convention SymPy and IEEE 754'spowuse. The change is that a limit no longer reads its answer off one. #738's evaluation half is untouched.0^0is deliberately not guarded. ItsNaNis how the library sayslim x->0 x^xdoes not exist —x^xis not real to the left of0— andLimitTest.TestNoLimitpins it. Including0^0broke exactly those three tests, which is what located the distinction: the guard is for indeterminate forms the arithmetic answers with a value, not for the ones it already answers withNaN.What it costs
Three limits answered
1are now unevaluated:The first was right by luck: the same substitution gave
1for(x!)^(1/x), where the answer is+oo, and the two cannot be told apart at the point where the value is read off. Answering it properly wants the Stirling expansion — #754's second half — and it is pinned here so that work has a target.The other two are two-sided limits at
0whose base has no two-sided limit at all and which are not real to the left of0, so the1came from the complex continuation. Their one-sided readings are unchanged:lim x->0+ (1/x)^xis still1,lim x->0+ (1/x)^(1/ln x)is still1/e.Recorded in
BREAKING-CHANGES.md.Measured
225 generated powers at
0and+oo— bases includingx!,1+1/x,e^x,ln(x),(x+1)/(x+2), exponents including1/x,1/x^2,1/ln(x),x,x^2— diffed againstmaster:NaN→ unevaluatedSuites and harnesses, from a clean build of this branch:
casbench112/117 solved, 0 wrong, 0 error, 0 timeout — unchangedpropcheck0 failures of 1337 checksrootcheck596/596 cleansimpsweep0 disagreements of 10463