Gruntz answers the example it is introduced with - #1627
Merged
Merged
Conversation
lim e^x (exp(1/x + e^(-x)) - exp(1/x)), x -> oo, is the example Gonnet and
Gruntz introduce the algorithm with, and it came back as written. The
algorithm did its steps right -- the mrv set {e^(-x), e^x}, the rewrite
(e^(w + 1/x) - e^(1/x))/w -- and the series engine then read a leading
term where there is none, in three places:
- a constant term was taken off by subtracting it, which left 1/x - 1/x
at w^0 in the argument of an exponential, and Exponentiate declined an
argument it took to run off to infinity;
- normalising a series divided the leading coefficient by itself, and the
inner simplification leaves x/x as written, so the rest carried
x/x - 1 at w^0 and the geometric series multiplied it out term by term;
- e^(1/x) - e^(1/x), the two exponentials' constant terms, was not known
to be zero: collecting like terms gives 0 provided not x = 0, a zero
wherever the coefficient is defined.
The constant term is now removed exactly, the normalised leading
coefficient is 1 exactly, and the zero test collects like terms and reads
a conditional zero as zero. Part of #353.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Co-Authored-By: Claude Opus 5.5 (1M context) <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.
Gonnet and Gruntz introduce their limit algorithm with
lim e^x (exp(1/x + e^(-x)) - exp(1/x))asx → ∞. Expanding in powers of1/xgivesO(x^-k)for everykand settles nothing. On master it came back as written.GRUNTZ_DEBUG=1shows the algorithm doing the paper's steps right: the mrv set{e^(-x), e^x}, and the rewrite(e^(w + 1/x) - e^(1/x))/w. The series engine then read a leading term where there is none, in three places:Exponentiatesubtracted the constant term1/xof its argument, leaving1/x + -(1/x)atw^0. It then declined, taking the argument to run off to infinity.x/xas written, so the rest of the series carriedx/x + -1atw^0. The geometric series then multiplied that out term by term. For the whole computation,GRUNTZ_DEBUGprinted 7981 lines on master and prints 97 now.e^(1/x) - e^(1/x)was not known to be zero. These are the two exponentials' constant terms. Collecting like terms gives0 provided not x = 0, which is zero wherever the coefficient is defined. The excluded point says nothing aboutx → ∞, which is the readingGruntz.Barealready makes.The constant term is now removed exactly (
WithoutConstant), the normalised leading coefficient is1exactly, and the zero test collects like terms and reads a conditional zero as zero. The paper's example and two variants are inGruntzTest.TheExampleTheAlgorithmIsIntroducedWith, all1.Suite, net10.0, at
b204d304on masterad02ebb7: 14153 passed, 0 failed. Every target framework builds; the 643 limit tests all pass.Gate: allocation is what the baseline says on all 19 gated benchmarks.
BREAKING-CHANGES.mdhas the three rows, measured onv2.5.0, where all three were left as written.Part of #353, where the comparison of the paper with the implementation is posted.
🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura