Skip to content

Commit e38da2b

Browse files
Promote two agreeing one-sided limits over the reals (#719, step 2; #596) (#756)
A two-sided limit is the two one-sided ones agreeing, and AngouriMath could not say so. The branch that compares them compares two `ComputeLimitDivideEtImpera` results -- the bare descent -- where a caller who names a side gets that descent *and* everything behind it: SolveAsIndeterminatePower, l'Hopital's rule, and the substitution that moves a finite destination out to infinity. The promotion could not be made before because the sides did not stay inside the reals. Over the complex plane `lim x->0- x^x` answers 1 from the continuation, so promoting agreement would give `lim x->0 x^x` the value 1 -- and `x^x` is not real to the left of 0 at all. #755 gave limits a codomain to read; this uses it, and **only under `Domain.Real`**, which is exactly what makes it sound: there that side has no value to agree with, so the case this could get wrong is the case that no longer arises. The expression #596 reported, at 0, over the reals: 1/ln(x + sqrt(x^2+1)) - 1/ln(x+1) left -1/2 already right -1/2 already both unevaluated -> -1/2 What must not be promoted, and is not: x * ln(x), x^x, sqrt(x), ln(x) real on one side only, so unevaluated 1/x, abs(x)/x, e^(1/x), arctan(1/x) sides disagree, so still NaN A second change came with it, and it belongs here rather than in #755 because this is what exposed it. A **two-sided** limit is now withdrawn if *either* approach leaves the reals, where the check asked about one direction only. `lim x->0 sqrt(x)` answered 0 while its own left-hand limit had been withdrawn, which is the two halves disagreeing about the same reading. Asked only where the answer would otherwise be NaN or nothing, so no limit that already answers pays for it, and bounded by a depth of two: each side may reach a two-sided limit of a subexpression, and without a bound the two questions branch into four and so on down the tree. Nothing changes by default. The complex reading answers as it always has, which is what keeps `LimitTest.TestNoLimit` meaning what it meant, and that is pinned. Suite 5135 -> 5147 passed / 0 failed, F# 130/130, corpus 112/117 with every verdict and answer byte-identical, rootcheck 596/596, propcheck 0 failures. Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 parent 52a6861 commit e38da2b

2 files changed

Lines changed: 149 additions & 19 deletions

File tree

‎Sources/AngouriMath/Functions/Continuous/Limits/Solvers/Solvers.Definition.cs‎

Lines changed: 82 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,61 @@ internal static partial class LimitFunctional
8181
return null;
8282
}
8383

84+
/// <summary>
85+
/// The limit where the two one-sided limits agree, asked of each side through the
86+
/// whole of <see cref="ComputeLimit"/>, or <see langword="null"/> where either side
87+
/// has no answer, the two differ, or the reading is not of real-valued functions.
88+
/// </summary>
89+
/// <remarks>
90+
/// A two-sided limit is the two one-sided ones agreeing, and the branch that compares
91+
/// them compares two <c>ComputeLimitDivideEtImpera</c> results -- the bare descent --
92+
/// where a caller who names a side gets that descent *and* everything behind it:
93+
/// <see cref="SolveAsIndeterminatePower"/>, l'Hopital's rule, and the substitution
94+
/// that moves a finite destination out to infinity.
95+
/// <para/>
96+
/// **Only under a real codomain, and that is the whole of what makes it sound.** The
97+
/// promotion cannot be made over the complex plane, because there the one-sided limits
98+
/// do not stay inside the reals: `lim x->0- x^x` answers 1 from the continuation, so
99+
/// promoting agreement would give `lim x->0 x^x` the value 1 where `x^x` is not real
100+
/// to the left of 0 at all, and `LimitTest.TestNoLimit` pins it as non-existent.
101+
/// Under <see cref="AngouriMath.Core.Domain.Real"/> that side has no value to agree
102+
/// with, so the case this could get wrong is the case that no longer arises.
103+
/// <para/>
104+
/// Asked only where the answer would otherwise be NaN, so nothing that already answers
105+
/// pays for it, and it can only ever turn a refusal into an answer.
106+
/// <a href="https://github.com/asc-community/AngouriMath/issues/719">#719</a>,
107+
/// <a href="https://github.com/asc-community/AngouriMath/issues/596">#596</a>
108+
/// </remarks>
109+
private static Entity? WhereBothSidesAgree(Entity expr, Variable x, Entity dest)
110+
{
111+
if (MathS.Settings.Codomain.Value is not AngouriMath.Core.Domain.Real
112+
|| bothSidesDepth >= MaxBothSidesDepth)
113+
return null;
114+
bothSidesDepth++;
115+
try
116+
{
117+
if (ComputeLimit(expr, x, dest, ApproachFrom.Left) is not { } fromLeft
118+
|| fromLeft.Evaled == MathS.NaN)
119+
return null;
120+
if (ComputeLimit(expr, x, dest, ApproachFrom.Right) is not { } fromRight
121+
|| fromRight.Evaled == MathS.NaN)
122+
return null;
123+
return fromLeft == fromRight || ExpressionNumerical.AreEqual(fromLeft, fromRight)
124+
? fromLeft : null;
125+
}
126+
finally { bothSidesDepth--; }
127+
}
128+
129+
/// <summary>
130+
/// How deep <see cref="WhereBothSidesAgree"/> may nest. Each one-sided limit it asks
131+
/// for may itself reach a two-sided limit of a subexpression, so without a bound the
132+
/// two questions would branch into four and so on down the tree, for expressions that
133+
/// have no answer either way and where the whole cost buys nothing.
134+
/// </summary>
135+
private const int MaxBothSidesDepth = 2;
136+
137+
[System.ThreadStatic] private static int bothSidesDepth;
138+
84139
private static Entity ExpandLogarithm(Entity expr)
85140
=> expr switch
86141
{
@@ -108,8 +163,15 @@ private static Entity ExpandLogarithm(Entity expr)
108163
// asks for it again, through the same rewrite, without end. Answering here costs
109164
// nothing and asks nothing.
110165
// https://github.com/asc-community/AngouriMath/issues/719
111-
if (RealCodomainWithdraws(expr, x, dest,
112-
side is ApproachFrom.Left ? ApproachFrom.Left : ApproachFrom.Right))
166+
// A two-sided limit is withdrawn if *either* approach leaves the reals, since it
167+
// is the two one-sided ones agreeing and one of them is not there to agree.
168+
// Checking only one direction left lim x->0 sqrt(x) answering 0 while its own
169+
// left-hand limit had been withdrawn, which is the two halves disagreeing about
170+
// the same reading.
171+
if (side is ApproachFrom.BothSides
172+
? RealCodomainWithdraws(expr, x, dest, ApproachFrom.Left)
173+
|| RealCodomainWithdraws(expr, x, dest, ApproachFrom.Right)
174+
: RealCodomainWithdraws(expr, x, dest, side))
113175
return null;
114176

115177
expr = expr.Replace(ExpandLogarithm);
@@ -229,15 +291,27 @@ private static Entity ExpandLogarithm(Entity expr)
229291
return fromLeft;
230292
if (ExpressionNumerical.AreEqual(fromLeft, fromRight) && (acceptNaN || fromLeft.Evaled != MathS.NaN))
231293
return fromLeft;
232-
var lhopital = ApplylHopitalRule(expr, x, dest);
233-
if (lhopital != null) return ComputeLimit(lhopital, x, dest, acceptNaN: true);
234-
else return MathS.NaN; // A two-sided limit cannot exist if the limit from left and right don't match.
294+
if (ApplylHopitalRule(expr, x, dest) is { } lhopital
295+
&& ComputeLimit(lhopital, x, dest, acceptNaN: true) is { } byRule
296+
&& (acceptNaN || byRule.Evaled != MathS.NaN))
297+
return byRule;
298+
// Asking each side properly, which is what the two above were not asked.
299+
// https://github.com/asc-community/AngouriMath/issues/719
300+
if (WhereBothSidesAgree(expr, x, dest) is { } agreed)
301+
return agreed;
302+
return MathS.NaN; // A two-sided limit cannot exist if the limit from left and right don't match.
235303
}
236304
else
237305
{
238-
var lhopital = ApplylHopitalRule(expr, x, dest);
239-
if (lhopital != null) return ComputeLimit(lhopital, x, dest);
240-
else return null;
306+
if (ApplylHopitalRule(expr, x, dest) is { } lhopital
307+
&& ComputeLimit(lhopital, x, dest) is { } byRule)
308+
return byRule;
309+
// The same promotion as above. This branch is reached where the descent
310+
// has nothing to say about one of the sides at all, rather than saying
311+
// something that disagrees -- which is most of what the one-sided
312+
// fallbacks are for, so it is where the promotion is worth the most.
313+
// https://github.com/asc-community/AngouriMath/issues/719
314+
return WhereBothSidesAgree(expr, x, dest);
241315
}
242316
}
243317
throw new AngouriBugException($"Unresolved enum parameter {side}");

‎Sources/Tests/UnitTests/Calculus/RealCodomainLimitTest.cs‎

Lines changed: 67 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -131,21 +131,77 @@ public void TheSettingIsRestoredWhenItGoesOutOfScope()
131131
}
132132

133133
/// <summary>
134-
/// What this does not yet do. Promoting two agreeing one-sided limits to a two-sided
135-
/// one is the point of the setting and is deliberately not part of it: step 1 changes
136-
/// what every one-sided limit answers under a real codomain, and that wants measuring
137-
/// on its own before anything is built on top. Pinned so the next step has somewhere
138-
/// to land and so the current state is a decision rather than an oversight.
134+
/// The point of the setting. Two agreeing one-sided limits are a two-sided one, and
135+
/// the promotion is safe here for the reason it was unsafe before: over the complex
136+
/// plane it would give <c>lim x-&gt;0 x^x</c> the value 1, and over the reals that
137+
/// side has no value to agree with.
138+
/// <a href="https://github.com/asc-community/AngouriMath/issues/596">#596</a> is the
139+
/// expression that reported it.
139140
/// </summary>
140141
[Fact]
141-
public void AgreeingOneSidedLimitsAreNotYetPromoted()
142+
public void AgreeingOneSidedLimitsArePromoted()
143+
{
144+
const string reported = "1 / ln(x + sqrt(x ^ 2 + 1)) - 1 / ln(x + 1)";
145+
// Both sides answer, and agree.
146+
Assert.Equal("-1/2".ToEntity().Evaled, LimitOverTheReals(reported, "0", ApproachFrom.Left).Evaled);
147+
Assert.Equal("-1/2".ToEntity().Evaled, LimitOverTheReals(reported, "0", ApproachFrom.Right).Evaled);
148+
149+
using var _ = MathS.Settings.Codomain.Set(Domain.Real);
150+
var twoSided = reported.ToEntity().Limit("x", 0).Simplify();
151+
Assert.Equal("-1/2".ToEntity().Evaled, twoSided.Evaled);
152+
}
153+
154+
/// <summary>
155+
/// The two the promotion must not reach, and the reason it could not be made at all
156+
/// before the codomain existed. Each is real on one side only, so under this reading
157+
/// there is nothing on the other side to agree with.
158+
/// </summary>
159+
[Theory]
160+
[InlineData("x * ln(x)")]
161+
[InlineData("x ^ x")]
162+
[InlineData("sqrt(x)")]
163+
[InlineData("ln(x)")]
164+
public void AFunctionRealOnOneSideOnlyIsNotPromoted(string expr)
165+
{
166+
using var _ = MathS.Settings.Codomain.Set(Domain.Real);
167+
Assert.True(IsUnevaluated(expr.ToEntity().Limit("x", 0).Simplify()),
168+
$"{expr} was given a two-sided limit over the reals");
169+
}
170+
171+
/// <summary>
172+
/// And the ones that genuinely have no limit keep saying so: the promotion asks
173+
/// whether the sides *agree*, not merely whether they exist.
174+
/// </summary>
175+
[Theory]
176+
[InlineData("1 / x")]
177+
[InlineData("abs(x) / x")]
178+
[InlineData("e ^ (1/x)")]
179+
[InlineData("arctan(1/x)")]
180+
public void SidesThatDisagreeStillHaveNoTwoSidedLimit(string expr)
142181
{
143182
using var _ = MathS.Settings.Codomain.Set(Domain.Real);
144-
// Both sides are 0 and the two-sided answer is still NaN.
145-
Assert.Equal(Entity.Number.Integer.Create(0),
146-
Limit("x * ln(x)", "0", ApproachFrom.Right).Evaled);
147-
Assert.Equal(MathS.NaN.Evaled,
148-
"x * ln(x)".ToEntity().Limit("x", 0).Simplify().Evaled);
183+
Assert.Equal(MathS.NaN.Evaled, expr.ToEntity().Limit("x", 0).Simplify().Evaled);
149184
}
185+
186+
/// <summary>
187+
/// The promotion is opt-in with everything else. Over the complex plane these answer
188+
/// exactly as they always have, which is what keeps <c>LimitTest.TestNoLimit</c>
189+
/// meaning what it meant.
190+
/// </summary>
191+
[Theory]
192+
[InlineData("sqrt(x)", "0")]
193+
[InlineData("sin(x) / x", "1")]
194+
public void TheDefaultReadingIsUnchangedForTwoSidedLimitsToo(string expr, string expected) =>
195+
Assert.Equal(expected.ToEntity().Evaled,
196+
expr.ToEntity().Limit("x", 0).Simplify().Evaled);
197+
198+
// The two the real reading withdraws are, by default, still the definite NaN they
199+
// always were -- which is what keeps LimitTest.TestNoLimit meaning what it meant.
200+
[Theory]
201+
[InlineData("x ^ x")]
202+
[InlineData("x * ln(x)")]
203+
public void TheDefaultReadingStillCallsTheseNonExistent(string expr) =>
204+
Assert.Equal(MathS.NaN.Evaled, expr.ToEntity().Limit("x", 0).Simplify().Evaled);
205+
150206
}
151207
}

0 commit comments

Comments
 (0)