Repository navigation
Compare a moving-exponent power against the right thing (#735) - #736
Conversation
lim x->+oo x^x / e^(x * ln(x)) came back 0. The two sides are one function, so the expression is identically 1 -- and the library's own evaluator says so: (50 ^ 50) / e^(50 * ln(50)) is exactly 1. Gruntz's algorithm collects the subexpressions of the fastest comparability class into a set and then rewrites the expression by substituting each member by name. Mrv reads a power b^p whose exponent moves as exp(p * ln(b)) and puts that constructed node in the set, but nothing rewrote the expression itself, so Rewrite's Substitute had nothing to find. The set came back holding the same exponential twice -- once as the constructed e^(x * ln(x)) and once as the denominator's own e^(ln(x) * x), the same product with its factors the other way round, since simplification had sorted the copy already in the expression and the constructed one was never sorted. Only the second was found. x^x went into the series unchanged, its leading exponent read as +1, and w^positive tends to zero. Fixed where the reading is made rather than where it is used: every power whose exponent moves is written as an exponential once, at the entry, so that Mrv's reading of a node and the node itself are the same syntax by construction. That also collapses the duplicate, since the two spellings now normalise together. This assumes the base is positive, which is what Mrv's own reading of the same node already assumed -- the algorithm is scoped to the exp-log functions, and a moving exponent over a base that changes sign is outside that class either way. Checked: (-2)^x still answers NaN and (-1)^x / x is still declined, as before. A backstop alongside it, because the failure was silent rather than loud: if any member is still in the expression after the substitution, decline. A member left in the series is read as part of a coefficient, and the conclusion is then drawn from a leading term that is not the leading term. There is nothing to salvage from that -- no answer is a limit, a wrong answer is not. Five wrong answers and one hang: | | before | after | |---|---|---| | `x^x / e^(x * ln(x))` (is 1) | 0 | 1 | | `e^(x * ln(x)) / x^x` (is 1) | no answer in 20 s | 1, in 226 ms | | `x^x / e^(x * ln(x) - x)` (is e^x) | 0 | +oo | | `x^x / e^(x * ln(x) - ln(x))` (is x) | 0 | +oo | | `x^(2 * x) / e^(2 * x * ln(x))` (is 1) | 0 | 1 | | `(x^2)^x / e^(2 * x * ln(x))` (is 1) | 0 | 1 | x^x / e^x and x^x / 2^x were right before and are unchanged: this needs the two sides to be in the same comparability class, which is exactly when Gruntz's algorithm is the rule that answers rather than an earlier one. Full suite 4904 passed / 0 failed with this change alone -- the 15 above master's 4889 are the ones added here -- and every pre-existing GruntzTest case passes unchanged. F# 130/130, corpus 112/117 with 0 wrong, 0 error, 0 timeout. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
bcdd865 to
910e01f
Compare
|
Note on the The failing assertion was Assert.True(task.Wait(TimeSpan.FromSeconds(30)), "the limit did not terminate");-- so it was a timeout, not a wrong answer. Three separate grounds for calling it a flake:
Worth recording separately, since it is not this PR's doing: that macOS job took 13 m 22 s against about 3.5 min locally, and the guarded limit runs in parallel with the other ~4900 tests. A 30 s wall-clock budget on a 1 s operation under that much contention is inherently fragile. The budget exists to catch a hang rather than to measure duration, so it could be raised substantially without weakening what it checks -- but that is a change to a test unrelated to this one, so I have left it alone rather than bundle it here. |
* Re-read the second remarkable limit after simplification (#738) `lim x->+oo (x - 5)^x / x^x` came back 1 where it is `e^(-5)`, and so did every quotient of two powers whose base ratio tends to 1. The rule that reads a `1^oo` runs once, at the top of `ComputeLimit`, against the expression as it was written. A quotient of powers is not a `1^oo` at that point -- it is a quotient -- so the rule had nothing to match on. The descent then reaches `SimplifyAndComputeLimitToInfinity`, whose first act is to simplify, and `(x - 5)^x / x^x` becomes `((x - 5)/x)^x`: a `1^oo` which nothing now re-reads, because the rule that reads one has already run. Straight on into the solvers, where `1^(+oo)` evaluates to 1. Neither the simplification nor the rule is wrong. What was wrong is that a form *created* by simplification was judged by rules that ran before it existed. So the same rule is asked again where the expression is in the form the solvers read it in, which is also where every destination has already been normalised to `+oo`. Guarded by a depth counter like the other rules here, since each level of it asks for limits of its own. This closes both of the routes the issue separates, because both of them run through that one point after the simplification has happened: the `SolveBySubstitution` route, where `(1 + 1/x)^x` substitutes to an exact `1^(+oo)`, and the `Powf` descent route, where `((x - 5)/x)^x` builds `1^x` and that simplifies to 1. It also turns out not to need PR #736 underneath it, which the earlier tracing had expected: the rewrite answers these outright rather than dropping them through to Gruntz. Measured, at x -> +oo: (x - 5)^x / x^x 1 -> 1/e^5 (309 ms) (x + 1)^x / x^x 1 -> e (16 ms) (x + 3)^x / x^x 1 -> e^3 (21 ms) x^x / (x + 1)^x 1 -> 1/e (57 ms) x^x / (x - 5)^x 1 -> e^5 (50 ms) (2x + 1)^x / (2x)^x 1 -> sqrt(e) (59 ms) (x - 1)^x / x^x unevaluated in 5.2 s -> 1/e in 163 ms and the neighbouring quotients, where the base ratio does not tend to 1, are untouched: `(2x)^x / x^x` and `(x^2)^x / x^x` are still `+oo`, `x^x / (2x)^x` still 0. What this does not reach: `(x^2 + 1)^x / (x^2)^x`, which `Simplify` leaves written as a quotient, so no `1^oo` is created for anything to re-read. That one is left unevaluated rather than answered wrongly, and its cause is in the simplification rather than in the limits -- the same quotient written `((x^2 + 1) / x^2)^x` is answered 1 without any of this. Filed separately. The other half of #738 -- that `1^(+oo)` evaluates to 1 at all -- reaches everything that evaluates a power rather than only limits, and wants its own measurement rather than being bundled in here. Left open. Full suite 4909 passed / 0 failed (4889 + 20 new), F# 130/130, corpus 112/117 with 0 wrong, 0 error, 0 timeout, and the suite still runs in 3 m 30 s. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Pin the destinations the re-read reaches by a different road The cases already here all approach +oo, which is the one destination that arrives at SimplifyAndComputeLimitToInfinity unsubstituted. The others get there by a substitution first, and that is a different road to the same rule, so it is worth pinning that they arrive at all. x -> -oo was wrong in the same way and is fixed by the same change: lim x->-oo (x - 5)^x / x^x answered 1 on master and now answers e^(-5), which is right -- (1 - 5/x)^x for x -> -oo is 1/(1 + 5/t)^t at t -> +oo. Measured against stock master at 318ac9f. The finite destinations were never wrong, because (1 + x)^(1/x) is already a 1^oo as written and the rule catches it at the top of ComputeLimit without anything needing to be re-read. They are pinned because the re-read runs on that path too and must not disturb it, and measuring confirmed it does not. Full suite 4913 passed / 0 failed, 3 m 22 s. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Fixes #735.
x ^ xande ^ (x * ln(x))are one function, so this is identically1:The library's own evaluator disagrees with its own limit:
(50 ^ 50) / e ^ (50 * ln(50))is exactly1.Cause
Gruntz's algorithm collects the subexpressions of the fastest comparability class into a set, then rewrites the expression by substituting each member by name.
Mrvreads a powerb ^ pwhose exponent moves asexp(p * ln(b))and puts that constructed node in the set -- but nothing rewrote the expression, soRewrite'sSubstitutehad nothing to find.With
GRUNTZ_DEBUG=1:The same exponential is in the set twice -- once as the constructed
e ^ (x * ln(x)), once as the denominator's owne ^ (ln(x) * x), the same product with its factors the other way round, because simplification had sorted the copy already in the expression and the constructed one was never sorted. Only the second is found.x ^ xgoes into the series unchanged, its leading exponent reads as+1, andw ^ positivetends to zero.Fix
Fixed where the reading is made rather than where it is used: every power whose exponent moves is written as an exponential once, at the entry, so
Mrv's reading of a node and the node itself are the same syntax by construction. That also collapses the duplicate, since the two spellings now normalise together.This assumes the base is positive, which is what
Mrv's own reading of the same node already assumed -- the algorithm is scoped to the exp-log functions, and a moving exponent over a base that changes sign is outside that class either way. Checked:(-2) ^ xstill answersNaNand(-1) ^ x / xis still declined, both as before.A backstop alongside it, because the failure was silent rather than loud: if any member is still in the expression after the substitution, decline. A member left in the series is read as part of a coefficient and the conclusion is then drawn from a leading term that is not the leading term.
Measured
x ^ x / e ^ (x * ln(x))(is1)01e ^ (x * ln(x)) / x ^ x(is1)1, in 226 msx ^ x / e ^ (x * ln(x) - x)(ise ^ x)0+oox ^ x / e ^ (x * ln(x) - ln(x))(isx)0+oox ^ (2 * x) / e ^ (2 * x * ln(x))(is1)01(x ^ 2) ^ x / e ^ (2 * x * ln(x))(is1)01x ^ x / e ^ xandx ^ x / 2 ^ xwere right before and are unchanged: this needs the two sides to be in the same comparability class, which is exactly when Gruntz's algorithm is the rule that answers rather than an earlier one.Full suite 4904 passed / 0 failed with this change alone -- the 15 above master's 4889 are the ones added here -- F# 130/130, corpus 112/117 with 0 wrong, 0 error, 0 timeout. All pre-existing
GruntzTestcases pass unchanged.🤖 Generated with Claude Code