Skip to content

lim x->+oo (x!/x^x)^(1/x) is unevaluated: the base needs a limit before the exponent can be judged #754

Description

@Rafael-SOWNet

Two things, one measured while attempting the other. Measured on f9759c95.

1. A wrong answer

"(x!) ^ (1/x)".Limit("x", "+oo")   // 1

It is +oo. By Stirling, (x!)^(1/x) ~ x/e, which diverges — (10!)^(1/10) is already 3.6 and (100!)^(1/100) is 37.99. The library is definite about a limit that does not exist finitely, which is worse than leaving it unevaluated.

Neighbours, for contrast:

lim x->+oo x!                    +oo          correct
lim x->+oo ln(x!)                +oo          correct
lim x->+oo x! / x^x              unevaluated  (it is 0)
lim x->+oo (x! / x^x) ^ (1/x)    unevaluated  (it is 1/e — this is the corpus miss)

So the 1 is not a general failure to handle factorials; it is specific to this shape reaching something that substitutes and is definite about the result.

2. The corpus miss is blocked one step earlier than recorded

lim x->+oo ((x!) / x^x)^(1/x) = 1/e is the last lim:factorial problem in work/casbench and the only remaining miss that is not impossible. The write-up so far said the blocker is the guard in SolveAsIndeterminatePower that refuses when the base cannot be differentiated — a factorial's derivative wants the digamma function, which the library does not have — and that the fix is to compute that guard on the rewritten exponent rather than on the base, since ln(x!) written out as x*ln(x) - x + ln(2*pi*x)/2 is differentiable.

That was implemented and it changes nothing, because the rule never reaches the guard:

var baseLimit = EvalAssumingContinuous(@base.Limit(x, dest, side));
if (baseLimit != 0 && !IsInfiniteNode(baseLimit))
    return null;                      // <-- returns here

lim x->+oo x! / x^x is unevaluated, so baseLimit is neither zero nor infinite and the rule declines before the guard is consulted. The base's own limit is the missing piece.

For the record, the rewrite that was written and reverted — it is correct as far as it goes and worth keeping in view:

// ln(f!) -> f*ln(f) - f + ln(2*pi*f)/2, where f -> +oo and the dropped term cannot matter
private static Entity ExpandLogFactorial(Entity expr, Variable x, Entity dest, Entity power)
{
    if (expr is not Logf(var logBase, Factorialf(var argument))
        || logBase != MathS.e || !argument.ContainsNode(x)) return expr;
    if (EvalAssumingContinuous(argument.Limit(x, dest)) != Real.PositiveInfinity) return expr;
    // what Stirling drops is 1/(12f) + O(1/f^3), and it gets multiplied by the exponent
    // this sits under -- at power = x^2 and f = x that contributes a term growing like x
    if (EvalAssumingContinuous((power / argument).Limit(x, dest)) != 0) return expr;
    return argument * MathS.Ln(argument) - argument + MathS.Ln(2 * MathS.pi * argument) / 2;
}

The soundness condition is the part worth keeping: the expansion of ln(f!) has a vanishing error, 1/(12f) + O(1/f^3), where the expansion of f! itself has only a relative one — but vanishing is not enough, because the dropped term is multiplied by the exponent the rewrite sits under. Asking that power / f tend to zero is what makes the remainder disappear. For this expression that ratio is 1/x^2.

What it would take

The base needs a limit before the exponent can be judged, and x! / x^x is the base. Writing f! as e^(ln(f!)) and expanding that logarithm gives it cheaply:

x! / x^x  =  e^(ln(x!) - x*ln(x))  =  e^(-x + ln(2*pi*x)/2)  ->  e^(-oo)  =  0

which never forms (x/e)^x — the term measured earlier at over twenty seconds. That is a second rewrite with its own soundness condition and its own measurement, so it is written down here rather than attempted alongside.

It is also plausible that (1) and (2) are the same defect from two sides: something is willing to be definite about (x!)^(1/x) while declining x!/x^x, and both come down to what the machinery believes a factorial does at infinity.

Activity

  1. Rafael-SOWNet commented on Aug 6, 2026

    @Rafael-SOWNet
    MemberAuthor

    Part 1 is fixed and merged — PR #760. Part 2 is untouched and is all that remains of this issue.

    The cause was not what this issue guessed

    I wrote that (1) and (2) were plausibly "the same defect from two sides", and that something was "willing to be definite about (x!)^(1/x) while declining x!/x^x". That is wrong, and the factorial had nothing to do with it.

    A limit that no rule has a reading of is answered by substituting the destination and evaluating. That is correct wherever the expression is continuous there — and an indeterminate form is exactly where it is not. Almost every indeterminate form already declines without any help, because it evaluates to NaN and every caller reads NaN as "no limit": 0 * oo, oo - oo, oo / oo, 0^0. The two that do not are oo^0 and 1^oo, which this library's arithmetic answers with 1. So the 1 was that form's value, read off as though it were the limit.

    The factorial was only the reason nothing else could answer first. The same defect was sitting on two expressions with no factorial in them at all:

    lim x->+oo (e^x)^(1/ln(x))    was 1, is +oo
    lim x->+oo (x^2)^(1/ln(x))    was 1, is e^2
    lim x->+oo (x!)^(1/ln(x))     was 1, is unevaluated  (it is +oo)
    lim x->+oo (x!)^(1/x)         was 1, is unevaluated  (it is +oo)
    

    (x^2)^(1/ln x) is e^(2*ln(x)/ln(x)), that is e^2 at every x — so the old answer was not an approximation that got worse at infinity, it was wrong everywhere.

    Guarded in the two places that assemble such a form: LimitSolvers.SolveBySubstitution and the Powf descent in Limit.Classes.cs. The sum, product and quotient descents were already guarded there by IsDeterminate; the power was not. Both sites were needed — fixing only the first left the descent to reassemble (+oo)!^0 for itself.

    0^0 is deliberately not guarded: its NaN is how the library says lim x->0 x^x does not exist, which LimitTest.TestNoLimit pins. Including it broke exactly those three tests, and that is what located the distinction — the guard belongs on the indeterminate forms whose arithmetic gives a value, not on the ones that already give NaN. Nothing about what (+oo)^0 or 1^oo evaluate to as expressions has changed; both are still 1, as in SymPy and IEEE 754's pow.

    Cost, recorded in BREAKING-CHANGES.md: three limits answered 1 are now unevaluated, of which (x!)^(1/x^2) is the one that was genuinely right — and it was right by luck, since the same substitution gave 1 for (x!)^(1/x) where the answer is +oo, and the two cannot be told apart where the value is read off. It is pinned as a test so the work below has a target. The other two are two-sided limits at 0 whose base has no two-sided limit and which are not real to the left of 0; their one-sided readings are unchanged.

    Measured over 225 generated powers: 2 wrong values became right, 3 wrong values became unevaluated, 1 NaN became unevaluated, 3 right values became unevaluated.

    What remains: part 2, unchanged

    lim x->+oo ((x!) / x^x)^(1/x) = 1/e is still the last lim:factorial miss in the corpus, and the plan in the issue body still stands — first a limit for the base by writing f! as e^(ln(f!)) and expanding that logarithm, then the Stirling expansion of ln(f!) with the guard computed on the rewritten exponent. Nothing in #760 moves it: the base's limit is still what is missing.

    One correction to the expected value, for whoever picks this up. SymPy 1.14.0 answers this limit 0:

    >>> limit((factorial(x)/x**x)**(1/x), x, oo)   # x = Symbol('x', positive=True)
    0

    That is wrong, and the corpus is right. Checked numerically with mpmath at 50 digits:

    x        (x!/x^x)^(1/x)
    1e3      0.3694916635
    1e6      0.3678823205
    1e9      0.3678794453      1/e = 0.3678794412
    

    Worth knowing before anyone uses SymPy as the oracle for this one.

  2. changed the title [-]lim x->+oo (x!)^(1/x) answers 1 where it is +oo, and the factorial corpus miss is blocked earlier than recorded[/-] [+]lim x->+oo (x!/x^x)^(1/x) is unevaluated: the base needs a limit before the exponent can be judged[/+] on Aug 6, 2026
  3. added theissue type on Sep 22, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions