Skip to content

Commit a268bb1

Browse files
Compute limits at infinity by Gruntz's algorithm (#694)
After D. Gruntz, "On Computing Limits in a Symbolic Manipulation System", ETH 1996. What it adds are the limits nothing here had any reading of, above all the ones whose parts 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 (was unevaluated) lim x -> +oo x / sqrt(x^2 + 1) = 1 (was unevaluated) The first of those is the standard demonstration: expanding the two exponentials separately gives two divergent series whose difference cancels entirely, so no amount of differentiating both halves arrives anywhere. Rewriting the whole expression in w = e^(-x) gives (e^w - 1)/w, whose leading term is 1. Two pieces. AsymptoticSeries is a power series in w about 0 with real exponents and symbolic coefficients, which is not a Taylor series and could not be one: the coefficients are expressions in x, and the exponents may be negative and fractional. It takes the value of log(w) from outside, since w is an exponential and its logarithm is an ordinary expression -- without it the constant term of log(c w^e) cannot be told from zero. How far to carry it is not known in advance, so the caller raises the order until a leading term survives the cancellation. Gruntz itself finds the subexpressions in the fastest comparability class, writes every one of them as a power of one of their number, and reads the answer off the leading term. Three things the thesis is emphatic about are honoured: the exponential exp(s - c t) is never split into a product, which would put back a function of a faster class; the member everything is written in terms of is one with no other member inside it; and the leading coefficient is checked to be free of w before its exponent is trusted. Scope is the exp-log functions, which is what the algorithm is stated for, because those are eventually monotone and so comparable at all. A sine has no limit at infinity and no comparability class, so this declines rather than guesses, and that is pinned. So is the factorial, which needs Stirling and a tractable-function mechanism this does not have. Only for a destination at infinity. A limit at a finite point reaches infinity too by substituting for x, but there this would be replacing answers the existing rules already give rather than adding ones they do not -- lim x -> 0 x^x comes out as 1, against an existing test that pins it as having no limit, and that is a change to argue on its own evidence rather than to make as a side effect. 21 tests. 4028 in all, 127 F#, corpus 104/117 with nothing wrong, in error or timing out, and 1320 property checks.
1 parent 020f6a0 commit a268bb1

6 files changed

Lines changed: 863 additions & 22 deletions

File tree

Lines changed: 353 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,353 @@
1+
//
2+
// Copyright (c) 2019-2022 Angouri.
3+
// AngouriMath is licensed under MIT.
4+
// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.
5+
// Website: https://am.angouri.org.
6+
//
7+
8+
using AngouriMath.Core.Multithreading;
9+
using PeterO.Numbers;
10+
using System;
11+
using System.Collections.Generic;
12+
using System.Linq;
13+
using static AngouriMath.Entity;
14+
using static AngouriMath.Entity.Number;
15+
16+
namespace AngouriMath.Functions.Algebra
17+
{
18+
/// <summary>
19+
/// A power series in <c>w</c> around <c>w -> 0+</c>, truncated at a known exponent, whose
20+
/// coefficients are arbitrary expressions not containing <c>w</c>.
21+
/// </summary>
22+
/// <remarks>
23+
/// <para>
24+
/// This is what Gruntz's algorithm expands in, and it is not a Taylor series: the
25+
/// exponents may be negative and fractional, and the coefficients are symbolic rather
26+
/// than numeric. What is wanted from it in the end is only the leading term, but the
27+
/// leading terms of a sum can cancel -- which is the whole point of the algorithm, since
28+
/// e^(x + e^-x) - e^x cancels to every order when its two parts are expanded separately
29+
/// -- so the series has to be carried far enough to see past the cancellation, and how
30+
/// far that is is not known in advance. The caller raises the order until a leading term
31+
/// survives.
32+
/// </para>
33+
/// <para>
34+
/// The value of <c>log(w)</c> is supplied from outside rather than left as a logarithm of
35+
/// a symbol. Gruntz chooses w as an exponential, so its logarithm is an ordinary
36+
/// expression in x, and expanding a logarithm needs it: without it the constant term of
37+
/// <c>log(c * w^e)</c> cannot be told from zero.
38+
/// </para>
39+
/// </remarks>
40+
internal sealed class AsymptoticSeries
41+
{
42+
/// <summary>Coefficients by exponent, ascending. None of them contain w.</summary>
43+
internal SortedDictionary<ERational, Entity> Terms { get; }
44+
45+
/// <summary>Nothing is known at or beyond this exponent.</summary>
46+
internal ERational Order { get; }
47+
48+
private AsymptoticSeries(SortedDictionary<ERational, Entity> terms, ERational order)
49+
=> (Terms, Order) = (terms, order);
50+
51+
/// <summary>
52+
/// The order of a series that is not truncated at all. A constant, a power of w, and
53+
/// anything built from those by the four operations is known exactly, and saying so
54+
/// matters: a series carrying a finite order is one whose terms beyond it have been
55+
/// thrown away, and multiplying by it would throw away the other factor's terms too.
56+
/// </summary>
57+
[ConstantField] internal static readonly ERational Exact = ERational.FromInt32(1 << 24);
58+
59+
internal static AsymptoticSeries Constant(Entity value)
60+
{
61+
var terms = new SortedDictionary<ERational, Entity>();
62+
if (!IsKnownZero(value))
63+
terms[ERational.Zero] = value;
64+
return new AsymptoticSeries(terms, Exact);
65+
}
66+
67+
/// <summary>The one term <c>coefficient * w^power</c>.</summary>
68+
internal static AsymptoticSeries Monomial(Entity coefficient, ERational power)
69+
{
70+
var terms = new SortedDictionary<ERational, Entity>();
71+
if (!IsKnownZero(coefficient))
72+
terms[power] = coefficient;
73+
return new AsymptoticSeries(terms, Exact);
74+
}
75+
76+
/// <summary>
77+
/// The leading coefficient and its exponent, or <see langword="null"/> if every term
78+
/// known so far cancelled and the series is indistinguishable from zero at this order.
79+
/// </summary>
80+
internal (Entity Coefficient, ERational Power)? LeadingTerm()
81+
{
82+
foreach (var term in Terms)
83+
if (!IsKnownZero(term.Value))
84+
return (term.Value, term.Key);
85+
return null;
86+
}
87+
88+
/// <summary>
89+
/// Whether the coefficient is zero on the evidence available. A coefficient that
90+
/// cannot be decided is kept, so that a leading term is never claimed for something
91+
/// that might have cancelled.
92+
/// </summary>
93+
private static bool IsKnownZero(Entity coefficient)
94+
{
95+
if (coefficient == Integer.Zero)
96+
return true;
97+
var simplified = coefficient.InnerSimplified;
98+
if (simplified == Integer.Zero)
99+
return true;
100+
return simplified.Evaled is Complex { IsZero: true };
101+
}
102+
103+
private static SortedDictionary<ERational, Entity> Fresh() => new();
104+
105+
internal AsymptoticSeries WithOrder(ERational order)
106+
{
107+
if (order.CompareTo(Order) >= 0)
108+
return this;
109+
var terms = Fresh();
110+
foreach (var term in Terms)
111+
if (term.Key.CompareTo(order) < 0)
112+
terms[term.Key] = term.Value;
113+
return new AsymptoticSeries(terms, order);
114+
}
115+
116+
internal AsymptoticSeries Add(AsymptoticSeries other)
117+
{
118+
var order = Order.CompareTo(other.Order) <= 0 ? Order : other.Order;
119+
var terms = Fresh();
120+
foreach (var term in Terms.Concat(other.Terms))
121+
{
122+
if (term.Key.CompareTo(order) >= 0)
123+
continue;
124+
terms[term.Key] = terms.TryGetValue(term.Key, out var already)
125+
? (already + term.Value).InnerSimplified
126+
: term.Value;
127+
}
128+
return new AsymptoticSeries(terms, order);
129+
}
130+
131+
internal AsymptoticSeries Negate()
132+
{
133+
var terms = Fresh();
134+
foreach (var term in Terms)
135+
terms[term.Key] = (-term.Value).InnerSimplified;
136+
return new AsymptoticSeries(terms, Order);
137+
}
138+
139+
internal AsymptoticSeries Multiply(AsymptoticSeries other)
140+
{
141+
// Everything below the leading exponent of one factor is unknown in the product,
142+
// so the order of the product is each order raised by the other's leading power.
143+
var mine = LeadingTerm()?.Power ?? Order;
144+
var theirs = other.LeadingTerm()?.Power ?? other.Order;
145+
var order = Min(Order.Add(theirs), other.Order.Add(mine));
146+
var terms = Fresh();
147+
foreach (var left in Terms)
148+
foreach (var right in other.Terms)
149+
{
150+
var power = left.Key.Add(right.Key);
151+
if (power.CompareTo(order) >= 0)
152+
continue;
153+
var product = (left.Value * right.Value).InnerSimplified;
154+
terms[power] = terms.TryGetValue(power, out var already)
155+
? (already + product).InnerSimplified
156+
: product;
157+
}
158+
return new AsymptoticSeries(terms, order);
159+
}
160+
161+
private static ERational Min(ERational a, ERational b) => a.CompareTo(b) <= 0 ? a : b;
162+
163+
/// <summary>
164+
/// The series divided by its own leading term, which leaves a series starting at 1.
165+
/// </summary>
166+
private AsymptoticSeries? Normalised(out Entity coefficient, out ERational power)
167+
{
168+
coefficient = Integer.Zero;
169+
power = ERational.Zero;
170+
if (LeadingTerm() is not var (c, e))
171+
return null;
172+
(coefficient, power) = (c, e);
173+
var terms = Fresh();
174+
foreach (var term in Terms)
175+
if (term.Key.CompareTo(e) >= 0)
176+
terms[term.Key.Subtract(e)] = (term.Value / c).InnerSimplified;
177+
return new AsymptoticSeries(terms, Order.Subtract(e));
178+
}
179+
180+
/// <summary>
181+
/// The reciprocal, by the geometric series on what is left once the leading term is
182+
/// taken out. Declines if the leading term cannot be found, since dividing by a
183+
/// series that might be zero is not something to guess at.
184+
/// </summary>
185+
internal AsymptoticSeries? Invert(ERational requested)
186+
{
187+
if (Normalised(out var coefficient, out var power) is not { } unit)
188+
return null;
189+
// 1/(1 + d) = 1 - d + d^2 - ..., which terminates because d starts above w^0.
190+
var rest = unit.Add(Constant(-1));
191+
var sum = Constant(1);
192+
var term = Constant(1);
193+
for (var i = 0; i < MaxExpansionTerms; i++)
194+
{
195+
term = term.Multiply(rest.Negate());
196+
if (term.LeadingTerm() is not var (_, at) || at.CompareTo(requested) >= 0)
197+
break;
198+
sum = sum.Add(term);
199+
}
200+
return sum.WithOrder(requested).Multiply(Monomial((1 / coefficient).InnerSimplified, power.Negate()));
201+
}
202+
203+
/// <summary>How many terms of a geometric, exponential or logarithmic series to take.</summary>
204+
private const int MaxExpansionTerms = 24;
205+
206+
/// <summary>
207+
/// The exponential of the series. The argument must not run off to infinity -- a
208+
/// leading exponent below zero would mean the exponential belongs to a faster
209+
/// comparability class than w, which the algorithm has already ruled out by putting
210+
/// it in the set of most rapidly varying subexpressions instead.
211+
/// </summary>
212+
internal AsymptoticSeries? Exponentiate(ERational requested)
213+
{
214+
var constant = Terms.TryGetValue(ERational.Zero, out var atZero) ? atZero : Integer.Zero;
215+
var rest = Add(Constant(-constant));
216+
if (rest.LeadingTerm() is var (_, least) && least.CompareTo(ERational.Zero) <= 0)
217+
return null;
218+
// exp(constant) is left unexpanded on purpose: it is a coefficient, and opening
219+
// it up would reveal a function of a faster class than w.
220+
var scale = MathS.Pow(MathS.e, constant).InnerSimplified;
221+
var sum = Constant(1);
222+
var term = Constant(1);
223+
for (var i = 1; i < MaxExpansionTerms; i++)
224+
{
225+
term = term.Multiply(rest).Multiply(Constant(Rational.Create(1, i)));
226+
if (term.LeadingTerm() is not var (_, at) || at.CompareTo(requested) >= 0)
227+
break;
228+
sum = sum.Add(term);
229+
}
230+
return sum.WithOrder(requested).Multiply(Constant(scale));
231+
}
232+
233+
/// <summary>
234+
/// The logarithm of the series, given the value of <c>log(w)</c>. The leading term
235+
/// has to be found, since <c>log</c> of something that might be zero is not something
236+
/// to guess at.
237+
/// </summary>
238+
internal AsymptoticSeries? Logarithm(Entity logarithmOfW, ERational requested)
239+
{
240+
if (Normalised(out var coefficient, out var power) is not { } unit)
241+
return null;
242+
var head = (MathS.Ln(coefficient) + Rational.Create(power) * logarithmOfW).InnerSimplified;
243+
// log(1 + d) = d - d^2/2 + d^3/3 - ...
244+
var rest = unit.Add(Constant(-1));
245+
var sum = Constant(head);
246+
var term = Constant(1);
247+
for (var i = 1; i < MaxExpansionTerms; i++)
248+
{
249+
term = term.Multiply(rest);
250+
if (term.LeadingTerm() is not var (_, at) || at.CompareTo(requested) >= 0)
251+
break;
252+
sum = sum.Add(term.Multiply(Constant(Rational.Create(i % 2 == 1 ? 1 : -1, i))));
253+
}
254+
return sum.WithOrder(requested);
255+
}
256+
257+
/// <summary>
258+
/// The series of <paramref name="expr"/> in <paramref name="w"/> about zero, carried
259+
/// to <paramref name="order"/>, or <see langword="null"/> if some part of it is not
260+
/// something this can expand.
261+
/// </summary>
262+
internal static AsymptoticSeries? Expand(Entity expr, Variable w, Entity logarithmOfW, ERational order)
263+
{
264+
MultithreadingFunctional.ExitIfCancelled();
265+
if (!expr.ContainsNode(w))
266+
return Constant(expr);
267+
if (expr == w)
268+
return Monomial(1, ERational.One);
269+
switch (expr)
270+
{
271+
case Sumf(var left, var right):
272+
return Both(left, right, (a, b) => a.Add(b));
273+
case Minusf(var left, var right):
274+
return Both(left, right, (a, b) => a.Add(b.Negate()));
275+
case Mulf(var left, var right):
276+
return Both(left, right, (a, b) => a.Multiply(b));
277+
case Divf(var left, var right):
278+
return Expand(right, w, logarithmOfW, order) is { } divisor
279+
&& divisor.Invert(order) is { } inverted
280+
&& Expand(left, w, logarithmOfW, inverted.Order) is { } dividend
281+
? dividend.Multiply(inverted)
282+
: null;
283+
case Powf(var @base, var power) when @base == MathS.e:
284+
return Expand(power, w, logarithmOfW, order)?.Exponentiate(order);
285+
case Powf(var @base, var power) when !power.ContainsNode(w):
286+
return RaiseToConstant(@base, power, w, logarithmOfW, order);
287+
case Powf(var @base, var power):
288+
// b^p with w in the exponent is exp(p log b), which the two cases above
289+
// between them can expand.
290+
return Expand(MathS.Pow(MathS.e, power * MathS.Ln(@base)), w, logarithmOfW, order);
291+
case Logf(var @base, var antilog) when !@base.ContainsNode(w):
292+
return Expand(antilog, w, logarithmOfW, order)?.Logarithm(logarithmOfW, order) is { } logarithm
293+
? logarithm.Multiply(Constant((1 / MathS.Ln(@base)).InnerSimplified))
294+
: null;
295+
default:
296+
return null;
297+
}
298+
299+
AsymptoticSeries? Both(Entity left, Entity right, Func<AsymptoticSeries, AsymptoticSeries, AsymptoticSeries> combine)
300+
=> Expand(left, w, logarithmOfW, order) is { } a && Expand(right, w, logarithmOfW, order) is { } b
301+
? combine(a, b)
302+
: null;
303+
}
304+
305+
private static AsymptoticSeries? RaiseToConstant(
306+
Entity @base, Entity power, Variable w, Entity logarithmOfW, ERational order)
307+
{
308+
var requested = order;
309+
if (Expand(@base, w, logarithmOfW, order) is not { } expanded)
310+
return null;
311+
if (power.Evaled is not Rational exponent)
312+
return null;
313+
var wanted = exponent.ERational;
314+
// A whole power is a product, which keeps the coefficients as they are.
315+
if (wanted.IsInteger() && wanted.Abs().CompareTo(ERational.FromInt32(MaxExpansionTerms)) <= 0)
316+
{
317+
var times = wanted.ToEIntegerIfExact().ToInt32Checked();
318+
if (times == 0)
319+
return Constant(1);
320+
if (times < 0)
321+
return expanded.Invert(order) is { } inverted ? Repeated(inverted, -times) : null;
322+
return Repeated(expanded, times);
323+
}
324+
// Otherwise take the leading term out and use the binomial series on the rest.
325+
if (expanded.Normalised(out var coefficient, out var leading) is not { } unit)
326+
return null;
327+
var rest = unit.Add(Constant(-1));
328+
var sum = Constant(1);
329+
var term = Constant(1);
330+
for (var i = 1; i < MaxExpansionTerms; i++)
331+
{
332+
// The binomial coefficient built up one factor at a time, so that it works
333+
// for a fractional exponent as much as a whole one.
334+
var factor = (Rational.Create(wanted) - (i - 1)) / i;
335+
term = term.Multiply(rest).Multiply(Constant(factor.InnerSimplified));
336+
if (term.LeadingTerm() is not var (_, at) || at.CompareTo(requested) >= 0)
337+
break;
338+
sum = sum.Add(term);
339+
}
340+
sum = sum.WithOrder(requested);
341+
var scaled = MathS.Pow(coefficient, power).InnerSimplified;
342+
return sum.Multiply(Monomial(scaled, wanted.Multiply(leading)));
343+
}
344+
345+
private static AsymptoticSeries Repeated(AsymptoticSeries series, int times)
346+
{
347+
var result = Constant(1);
348+
for (var i = 0; i < times; i++)
349+
result = result.Multiply(series);
350+
return result;
351+
}
352+
}
353+
}

0 commit comments

Comments
 (0)