Repository navigation
Implement an algorithm for limits #353
Description
Activity
An algorithm for limits landed in #694: Gruntz's method — the MRV (most-rapidly-varying) set approach from his thesis, with an asymptotic series engine underneath it.
I could not open the ResearchGate link to check it is the same paper you meant, so worth confirming. What is implemented is the one that computes a limit by finding the most rapidly varying subexpression, rewriting the whole expression in terms of it, and expanding as a series — not a pattern table.
What it buys over the rules that were already there is the cases nothing else has any reading of, in particular differences whose terms cancel to every order:
lim x->+oo (e^(x + e^(-x)) - e^x) // 1 lim x->+oo (sqrt(x^2 + 3x) - sqrt(x^2 + 1)) // 3/2 lim x->+oo (x^20 / e^x) // 0, beyond l'Hopital's step boundIt runs last of the readings at infinity, after the cheaper ones, since it is the most expensive.
Leaving this open in case the paper you linked is a different algorithm and you want that one too — tell me which and I will read it. If Gruntz is what you meant, it can be closed.
This looks done. Measured on
masterata45a7256.The paper linked in the body is the Gruntz algorithm, and it is implemented —
Sources/AngouriMath/Functions/Continuous/Limits/Gruntz/holdsGruntz.csandAsymptoticSeries.cs. It answers the cases that distinguish a real algorithm from a table of special cases:limit at +ooanswer e^x / x^10+ooln(x) / x0(1 + 1/x)^xee^x - x+ooThe last is #231's one unticked case, which also now works.
I have not audited it against the paper section by section — that is a larger claim than I can make from behaviour — so treat this as "the algorithm named here exists and answers the hard cases" rather than "the implementation is complete and faithful". But the issue as filed asks for the algorithm to be implemented, and it is.
Decide whether to close after reading the paper and comparing with our implementation
I read the paper and compared it with our implementation, as you asked.
Which paper. The link is Gonnet and Gruntz, Limit Computation in Computer Algebra, ETH Zürich technical report 187, November 1992. ResearchGate refuses the PDF (HTTP 403), and ETH's Research Collection search needs JavaScript, so I read Bruno Salvy's summary of Gruntz's 29 March 1993 talk at the INRIA Algorithms seminar (gruntz.pdf), which states the algorithm step by step. The implementation cites Gruntz's 1996 thesis, which is the same algorithm worked out in full.
Step by step, it is what
Limits/Gruntz/Gruntz.csdoes:The paper Ours mrv(f + g),mrv(f g)are the larger of the parts'Mrv→MrvMax, for sums, differences, products and quotientsmrv(f^c) = mrv(f),mrv(log f) = mrv(f),mrv(x) = xthe matching arms of Mrvmrv(e^f)containse^fexactly whenf → ∞decided by LimitInfof the exponent, for either sign of infinitycompare fandgby `lim logf when one of them is x, replacexbyexp(x)throughoutthe lifting in MrvLeadTermrewrite the set in terms of one member ω Rewrite: the member containing none of the others, inverted if needed so that ω → 0Puiseux expansion in ω, other terms as parameters; recurse on the leading coefficient when ω's exponent is 0 AsymptoticSeries.Expand(rational exponents);LimitInf's exponent-0 branchthe problem reduces to deciding whether an exp-log function is zero the zero test in AsymptoticSeries; outside the exp-log class it declines rather than guessesBut it did not answer the paper's own example. The paper introduces the algorithm with
e^x (exp(1/x + e^(-x)) - exp(1/x))asx → ∞, where expanding in powers of1/xgivesO(x^-k)for everyk. On master and on 2.5.0 it came back as written, whilee^(x + e^(-x)) - e^x,x^x / e^(x ln x)ande^(e^x) / e^(e^x - e^(-e^x))were all answered.GRUNTZ_DEBUG=1shows the algorithm doing the paper's steps correctly: the set{e^(-x), e^x}and the rewrite(e^(w + 1/x) - e^(1/x))/ware right, and then the series engine declines.The cause is that a constant term was taken off by subtracting it.
Exponentiatesubtracts the constant term1/x, leaving1/x + -(1/x)atw^0. Normalising a series divides by the leading coefficient and subtracts 1, leavingx/x + -1. The inner simplification writes out neither as zero, and the zero test cannot decide a coefficient that containsx. So the leading exponent read 0 where it is not, andExponentiatedeclined. The samex/x + -1is what makes the geometric series swell in the trace.Fixed in #1627. The constant term is now removed exactly, the normalised leading coefficient is
1exactly, and the zero test collects like terms and reads0 provided not x = 0as zero. The example is now1, as are two variants with a different scale and parameter. For the whole computation,GRUNTZ_DEBUGprinted 7981 lines before the fix and prints 97 now. The 643 limit tests are unchanged, the suite passes 14153/0, and the gate passes.So the implementation is the paper's algorithm. With that fix it also answers the example the paper is built around, and I'll close this once the fix merges, unless you'd rather keep it open for something the full report covers and the summary does not.
- added a commit that references this issue
on Sep 30, 2026
It's a great-looking approach, located here.