Skip to content

Answer the limits that were left unevaluated, and un-invert a quotient (#536, #335, #333) - #714

Merged
Rafael-SOWNet merged 6 commits into
masterfrom
fix/limit-gaps
Aug 5, 2026
Merged

Rafael-SOWNet merged 6 commits into
masterfrom
fix/limit-gaps

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Closes #536, #335, #333, #347. Adds tests to #596 without closing it.

Six commits, one per finding. d30c4541 is the one to review first: it is a wrong-answer fix in core simplification, not a limits change, and it is reachable from any Simplify of a quotient whose denominator carries a negative factor.

The wrong answer

Four of the rules that take a negative constant out of a product read it from the numerator, where multiplying the rest by it is right. The two that read it from the denominator were written the same way, and there it is not: a / (-b*c) is -(a / (b*c)) and came back as -(b * (c/a)) — the reciprocal. Simplify keeps whichever candidate is shortest, so the inverted form won wherever it was smaller, which is wherever the numerator was 1.

simplify((1/x) / (-1 - 1/x))    was  -(1 + x)

That is -2 at x = 1, where the expression is -1/2. Found from a limit rather than by hand — l'Hôpital's rule simplifies the quotient of derivatives it builds, and this is the shape of one. Five regression cases added, each checking the value at a point rather than the form.

The limits

#536 — limits of piecewise. All five of the reporter's calls came back unevaluated, from two causes. The gate at the top of ComputeLimit admits ContinuousNode only and a Piecewise is not one, so the descent's Piecewise case was unreachable; and that case was dead anyway — allLims.Select(c => c.lim is null).Any() is Any() with no predicate, i.e. "is the sequence non-empty", so it always returned null. Even had it run, it built a piecewise of the cases' limits carrying predicates that still speak about the variable the limit had just removed. Rewritten to pick the case that holds near the destination, reading each predicate from the sign its comparisons keep on the way in. After: -1 at 0-, 1 at 0+, NaN two-sided at 0, -1 at -456, 1 at 123.

#335 — process the parts' limits. The maintainer's own comment names the fix: "cases when one of operands is finite and non-zero". The descent substituted the parts' limits only when both were finite, so lim x->0+ cos(x)/sin(x) was +oo while the same limit written cos(x)*(1/sin(x)) was unevaluated. Sum, difference, product and quotient now take both limits whenever the combination is a number rather than NaN — which is the arithmetic's own test for an indeterminate form. Powers are deliberately excluded: the arithmetic answers 1^(+oo) and (+oo)^0 with 1, and as limits neither is settled.

tan(x)*ln(x) — the gap left open in #712. Two causes. The first is the simplification inversion above. The second: the equivalent-infinitesimal substitution (sin(u) ~ u, tan(u) ~ u) fired only for a quotient, never a product, and was keyed on the function vanishing rather than its argument vanishing. Both corrected. lim x->0+ tan(x)*ln(x): NaN after 4.8 s -> 0 in 0.27 s. The argument check also fixed lim x->pi sin(x)/(x-pi), NaN -> -1 — the old rule rewrote sin(x) as x at pi, giving pi/0.

#333 — limit of arcsin. arcsin(+oo) evaluates to NaN, so substitution had nothing to work with. The library reads arcsin(t) on the side of both cuts below the real axis, which CompiledArcsinBranchTest pins; the limit follows the library rather than introducing a second convention. pi/2 - (+oo)i at +oo, -pi/2 - (+oo)i at -oo, arccos correspondingly. Also caught arcsec, which was "answered" with arcsec(+oo) — a right angle written as a function of an infinity — now pi/2.

#347 — stack overflow. Does not reproduce. "a and x".Limit("x", "+oo") returns an unevaluated limit(a and x, x, +oo) on stock master, no crash, and it is already pinned in AlreadyFixedIssuesTest.Issue347_LimitOfABooleanDoesNotCrash. No change here; the issue is closeable.

#596, and why one part is not fixed

  • x^4 * e^(-x) at +oo is already 0 on master and already tested.
  • 1/ln(x+sqrt(x^2+1)) - 1/ln(x+1) at 0 is -1/2 from either side already on master. The two-sided reading is unevaluated. Tests pin both one-sided values; the two-sided case is not fixed, on purpose. The obvious fix — a two-sided limit is the two one-sided ones agreeing — is exactly the guard that rejects it: AngouriMath's one-sided limits do not stay inside the reals (lim x->0- ln(x) is -oo, lim x->0- x*ln(x) is 0, lim x->0- x^x is 1), so that promotion would also turn lim x->0 x*ln(x) into 0 and lim x->0 x^x into 1 — both deliberately NaN, one pinned by LimitTest.TestNoLimit. The question underneath is whether a one-sided limit may leave the reals, which is a design decision rather than something to settle inside this issue.
  • ((x!)/x^x)^(1/x) at +oo needs an asymptotic for the factorial and is still declined by the documented guard in SolveAsIndeterminatePower. Unevaluated, not wrong.

Measured

base 5f4269e0 branch head
UnitTests 4675 passed, 0 failed, 14 skipped 4746 passed, 0 failed, 14 skipped (71 new)
FSharpWrapperUnitTests 130 130
corpus 111/117, 0 wrong, 0 error, 0 timeout 111/117, 0 wrong, 0 error, 0 timeout

No existing test changed behaviour and nothing was loosened. Suite wall time 3m42s -> 3m31s. One limit got slower: the #596 difference at 0+, 2.4 s -> 3.9 s from extra descent work, well inside budget.

Noticed, not touched

AngouriMath's arcsin on the cuts is the conjugate of C99, Python and Mathematica: arcsin(2) is pi/2 - 1.317i here and pi/2 + 1.317i there. It is internally consistent and pinned by an existing test, so the new limit follows it — but the convention itself probably deserves its own issue.

Every limit of a piecewise came back unevaluated, at a seam or nowhere near
one. Two things stopped it. The gate in front of ComputeLimit admits continuous
nodes only, and a piecewise is not one, so the descent's reading of one was
never reached; and that reading built a piecewise of the cases' limits with
their predicates carried along, which answers nothing, since the predicates
still speak about the variable the limit has just got rid of.

Close enough to the destination a piecewise is one of its cases and nothing
else, so its limit is that case's limit -- and which case that is is decided the
way evaluation decides it, by the first predicate that holds once every earlier
one has failed. Whether a predicate holds on the way in is the sign its
comparisons' differences keep near the destination, which is the reading
DivergesAtAVanishingDivisor already had for a divisor and which is now shared
with it: a non-zero limit fixes the sign on its own, and a vanishing one is read
off the first derivative that does not vanish with it.

Where no case holds throughout the neighbourhood the expression is undefined on
the whole of the way in, and NaN says that. Where a predicate cannot be settled
either way it is left open which case the limit is of, and an unevaluated limit
says that.

The reporter's own piecewise, sign(x) written out, now answers -1 at 0-, 1 at
0+, -1 at -456, 1 at 123, and NaN two-sided at 0, where all five were
unevaluated. Suite 4691 passed, 0 failed, with 16 new cases; corpus unchanged at
111/117 with 0 wrong, 0 error and 0 timeout.
The descent puts each part's own limit in place of the part, and it only did so
where both of those limits were finite. The algebra of limits does not stop
there: where f tends to A and g to B, f * g tends to A * B whenever A * B means
anything at all, and 1 * +oo means +oo as surely as 2 * 3 means 6. The
determinate combinations with an infinity in them were left to the solvers,
which substitute the destination into the expression and read what comes out --
and those answer the same limit differently depending on how it is written.
lim x->0+ cos(x) / sin(x) was +oo and lim x->0+ cos(x) * (1 / sin(x)) was
unevaluated.

A sum, a difference, a product and a quotient now take both parts' limits
whenever the combination of the two is a number rather than an indeterminate
form -- which is exactly the test the arithmetic already performs, since it
answers 0 * oo, oo - oo, oo / oo, 0 / 0 and a non-zero over 0 with NaN. Those
keep falling through to the readings that can take them apart.

Powers are deliberately left out: the arithmetic gives 1 for both 1 ^ (+oo) and
(+oo) ^ 0, and as limits neither is settled, so a power settled this way would
be settled wrongly.

15 cases added here. The suite passes with 0 failed, 4728 at the head of the
branch; corpus unchanged at 111/117 with 0 wrong, 0 error and 0 timeout.
Four of the rules that take a negative constant out of a product read the
constant from the numerator, where multiplying the rest by it is right. The two
that read it from the denominator were written the same way, and there it is
not: a / (-b * c) is -(a / (b * c)) and came back as -(b * (c / a)), which is
the reciprocal of it.

Simplify keeps whichever of its candidates is shortest, so the inverted form won
wherever it was smaller than the right one -- wherever the numerator was 1.
1 / (x * (-1 - 1/x)) simplified to -(1 + x), which is -2 where the expression is
-1/2 at x = 1. Reached from a limit rather than written by hand: l'Hopital's
rule simplifies the quotient of derivatives it builds, and this is the shape of
one.

5 cases added here, each checking the value at a point rather than the form. The
suite passes with 0 failed, 4728 at the head of the branch; corpus unchanged at
111/117 with 0 wrong, 0 error and 0 timeout.
sin(u), tan(u), arcsin(u) and arctan(u) are each equivalent to u where u
vanishes, and it is the ratio of the two forms tending to 1 that licenses
writing one for the other. That says nothing about which of them the rest of the
expression is written over, so a product takes the substitution as much as a
quotient does. Only the quotient had it, so lim x->0+ tan(x) * ln(x) went the
long way round through l'Hopital's rule and came back NaN -- the claim that it
does not exist -- where the same limit written sin(x) * ln(x) is 0.

The substitution was also made on the function vanishing rather than on its
argument vanishing, which are two different conditions. sin(x) vanishes at pi as
surely as at 0 and there it is equivalent to pi - x, so rewriting it as x turned
lim x->pi sin(x) / (x - pi), which is -1, into pi / 0.

lim x->0+ tan(x) * ln(x) is 0 in 0.27s, where it was NaN after 4.8s;
lim x->pi sin(x) / (x - pi) is -1, where it was NaN. 17 cases added here. Suite
4728 passed, 0 failed; corpus unchanged at 111/117 with 0 wrong, 0 error and 0
timeout.
Neither arcsine nor arccosine is real past 1, and both were left unevaluated
where their argument grows without bound. The library does read them there, on
the principal branch taken from below both cuts: arcsin(t) is pi/2 - i*arcosh(t)
for real t past 1 and -pi/2 - i*arcosh(t) below -1, with arccos being
pi/2 - arcsin throughout. arcosh grows without bound, so what is left in the
limit is that real part with an infinite imaginary one, and that is now the
answer.

C99 and Python take the other side of both cuts and answer the conjugates.
CompiledArcsinBranchTest pins the side this library takes, and a limit that
disagreed with the function it is a limit of would be worse than either
convention, so the limit follows the library.

An arcsecant is an arccosine of a reciprocal, so a diverging argument takes it
to a right angle, which is real. Substituting the infinity did settle that one
-- as arcsec(+oo), the right angle written as a function of an infinity rather
than as the right angle -- so it is asked in front of the substitution.

lim x->+oo arcsin(x) is pi/2 - (+oo)i and lim x->+oo arcsec(x) is pi/2, where
the first was unevaluated and the second was arcsec(+oo). 16 cases added here.
Suite 4744 passed, 0 failed; F# wrapper 130 passed; corpus unchanged at 111/117
with 0 wrong, 0 error and 0 timeout.
Of the three limits in the report, the second -- lim x->+oo x^4 * e^(-x) -- is
0 and already has a test. The first, the difference of reciprocal logarithms, is
-1/2 and is answered from either side; the two-sided reading of it is not, and
that is what the reporter asked for. Pinning the two that do answer, so the
mathematics of the reported case is protected while the two-sided reading is
open.

Promoting the agreement of the two one-sided readings into a two-sided answer,
which is what the definition of a two-sided limit would license, is not open
here: the one-sided readings do not stay inside the reals, so lim x->0- ln(x)
is -oo and lim x->0- x * ln(x) is 0, and the same promotion would turn
lim x->0 x * ln(x) into 0 and lim x->0 x^x into 1 where both are deliberately
NaN. Whether a one-sided limit may leave the reals is the question underneath
that, and it is a wider one than this issue.

The third limit, ((x!) / x^x)^(1/x), needs an asymptotic for the factorial and
is still declined by the guard in SolveAsIndeterminatePower.

2 cases added here. Suite 4746 passed, 0 failed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Can't evaluate limits of piecewise

1 participant