From d5655b8edd7feb60977943727673110a61c13a8f Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Wed, 12 Aug 2026 01:11:51 +0000 Subject: [PATCH] Stop pulling an exponent out of a logarithm over an undecided argument (#902) log_b(a^c) = c * log_b(a) holds where c * ln(a) stays inside the strip Im in (-pi, pi] that ln maps onto, and the rule asked for nothing. ln(e^x) came back as x, which at x = 3*pi*i is 9.4247i where the expression is pi*i -- e^(3*pi*i) being -1, so the two differ by exactly the turn the principal branch discards. The rewritten form is shorter, so it won the complexity contest and this is what an ordinary caller got. Codomain defaults to Complex, so it was unsound on the library's own default reading; a negative real base breaks it too, log(2, 64) being 6 where 2 * log(2, -8) is 6 + 9.0647i. The rule now wants a base that is decidably a positive real and an exponent that may be taken as real -- the reading says so, the node's declared codomain says so, or its value is one. A symbolic exponent under the complex reading is none of those and the expression is left as written, which is the treatment the four inverse-trigonometric rules of #884 got. ln(e^3) still folds, and so does ln(e^x) under Codomain.Set(Domain.Real). Two limits are lost with it, both from right answer to no answer, and both recorded in BREAKING-CHANGES.md and in a test of their own that asserts the unevaluated node: lim x->+oo (x^2)^x / e^(2*x*ln(x)) 1 -> unevaluated lim x->+oo x^x / e^(x*ln(x) - ln(x)) +oo -> unevaluated They want the identity that just went away: d/dx (x^2)^x carries ln(x^2) and l'Hopital's rule reached it through Simplify. On the way to +oo the base really is positive, so it is true there and the limit machinery has no way to say so. Supplying it from the limit side was implemented and measured, at three insertion points: the pull fires and gives 2 * ln(x) correctly, and the limits stay unevaluated, because Simplify's own candidate search writes (x^2)^x back into a logarithm and needs the identity again. It is load-bearing inside the search, so restoring these wants an assumption travelling with the expression -- #746 tier 1 and #721 -- rather than another pass. That code is not in this commit; only the finding is. A wrong answer reachable from ln(e^x) is worse than two unevaluated limits by the ordering in AGENTS.md, and this file already records two integrals lost the same way. boundcheck 4 disagreements -> 2, the remaining two being log(x, x) and ln(x) + ln(x+1), each recorded elsewhere as wanting a decision rather than a guard. Suite 6342 passed, F# wrapper 130 passed, casbench 117/119 with 0 wrong, rootcheck 596/596, simpsweep 10463/10463, propcheck 1340 checks 0 failures, crashcheck 1652 cases 0 crashes. Co-Authored-By: Claude Opus 5 (1M context) --- BREAKING-CHANGES.md | 53 +++++++++++++++++++ .../Simplification/Patterns/Patterns.Power.cs | 38 ++++++++++++- .../Calculus/GruntzMovingExponentTest.cs | 35 +++++++++++- .../Common/SimplificationRegressionTest.cs | 40 ++++++++++++++ 4 files changed, 163 insertions(+), 3 deletions(-) diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 306a9046f..5bbcc7934 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -68,6 +68,8 @@ read first. | loud | a known gap, e.g. a cubic inequality | `AngouriBugException`, asking to be reported | `NotSufficientlySupportedException` | | **silent** | `arcsin(sin(x))` and three siblings | `x`, wrong wherever `x` leaves the principal interval | left as written unless `x` is a real in that interval | | **silent** | `abs(sgn(x))` and `sgn(abs(x))` | `1`, wrong at `x = 0` where both are `0` | left as written unless the argument's value can be read | +| **silent** | `ln(e^x)`, `log(2, 2^x)`, `ln(x^2)` | `x`, `x`, `2 * ln(x)` — wrong off the real line | left as written unless the argument is decidable | +| **silent** | two limits over `(x^2)^x` and `x^x` | answered correctly | unevaluated — a deliberate loss | | **silent** | `arctan(x) + arccotan(x)` | `pi/2`, wrong for every negative `x` | `pi/2` or `-pi/2` where the sign is known, else left as written | | **silent** | `log(1, 1)` | `0` | `NaN`, since it is `0/0` | | **silent** | `log(b, 1)` | `0` for any base | `0 provided not b = 1` | @@ -350,6 +352,57 @@ Found by `boundcheck`, a harness that composes every unary function node with ev compares against the original at points where an assumption fails rather than at sampled points. Issue [#887](https://github.com/asc-community/AngouriMath/issues/887). +### An exponent is no longer pulled out of a logarithm over an undecided argument + +`log_b(a^c) = c * log_b(a)` holds where `c * ln(a)` stays inside the strip `Im in (-pi, pi]` that `ln` +maps onto. It was applied to any argument at all, and the rewritten form is shorter, so it is what an +ordinary caller got: + +| | was | is | +|---|---|---| +| `ln(e^x)` | `x` | left as written | +| `log(2, 2^x)` | `x` | left as written | +| `ln(x^2)` | `2 * ln(x)` | left as written | +| `ln(e^3)`, `log(2, 2^5)` | `3`, `5` | unchanged | +| `ln(e^x)` under `Codomain.Set(Domain.Real)` | `x` | `x`, unchanged | + +`ln(e^x) -> x` is wrong wherever `Im x` leaves that strip. At `x = 3*pi*i` the expression is `pi*i`, +because `e^(3*pi*i)` is `-1`, while `x` is `9.4247...i` — the two differ by exactly the full turn the +principal branch discards. `MathS.Settings.Codomain` defaults to `Domain.Complex`, so this was unsound +on the library's own default reading. It is also unsound for a negative real base: `log(2, 64)` is `6` +where `2 * log(2, -8)` is `6 + 9.0647...i`. + +The rule now asks for a base that is decidably a positive real, and an exponent that may be taken as +real — because the reading is real analysis, because the node's declared codomain says so, or because +its value is a real. A symbolic exponent under the default complex reading is none of those, so the +expression is left as written: decide, or decline, as with the four inverse-trigonometric rules above. + +**Two limits are lost, and that is the cost of this entry rather than an oversight.** + +| | was | is | +|---|---|---| +| `lim x->+oo (x^2)^x / e^(2*x*ln(x))` | `1` | unevaluated | +| `lim x->+oo x^x / e^(x*ln(x) - ln(x))` | `+oo` | unevaluated | + +Both are right answers becoming no answer, which this file has recorded before for two integrals, and +which the ordering in [AGENTS.md](AGENTS.md) prefers to a wrong answer reachable from `ln(e^x)`. They +are unevaluated rather than `NaN`: the caller is told nothing was settled, not that the limit does not +exist. + +They want the identity that was just removed. `d/dx (x^2)^x` carries `ln(x^2)`, and l'Hopital's rule +reached it through `Simplify`. On the way to `+oo` the base genuinely is positive, so the identity is +true there — the limit machinery simply has no way to say so to the simplifier. Supplying it from the +limit side was tried and does not reach: rewriting the expression before `Simplify` is called does pull +the exponent out, and `Simplify`'s own candidate search then writes `(x^2)^x` back into a logarithm and +needs the identity again. It is load-bearing *inside* the search, so what would restore these two is an +assumption travelling with the expression — `#746`'s tier 1 and the subject of +[#721](https://github.com/asc-community/AngouriMath/issues/721) — and not another pass. The two rows +have their own test asserting the unevaluated node, so a future fix flips them back deliberately. + +`boundcheck` drops from four disagreements to two; the remaining two are `log(x, x)` and +`ln(x) + ln(x+1)`, both recorded elsewhere as wanting a decision rather than a guard. Issue +[#902](https://github.com/asc-community/AngouriMath/issues/902). + ### `abs(sgn(x))` and `sgn(abs(x))` are not `1` at zero `|sgn(z)|` and `sgn(|z|)` are `1` for every `z` except `0`, where both are `0`, because `sgn(0)` is diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs index 4c22c6034..2f19b0296 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs @@ -155,7 +155,16 @@ expr is Sumf(var any1, Mulf(Real { IsNegative: true } const1, var any2)) // x * {} ^ {} = {} ^ {} * x Mulf(Variable var1, Powf(var any1, var any2)) => new Powf(any1, any2) * var1, - Logf(var any1, Powf(var any2, var any3)) => any3 * MathS.Log(any1, any2), + // log_b(a^c) = c * log_b(a) holds where c * ln(a) stays inside the strip + // Im in (-pi, pi] that ln maps onto, and not in general: ln(e^(3*pi*i)) is pi*i + // while 3*pi*i is not, the two differing by exactly the 2*pi*i the principal branch + // discards. A base that is a positive real makes ln(a) real, and a real exponent then + // keeps the product real, so there is nothing to discard. Anything else is left as + // written -- including a symbolic exponent under the default complex reading, where + // the question is not decidable. + // https://github.com/asc-community/AngouriMath/issues/902 + Logf(var any1, Powf(var any2, var any3)) + when IsPositiveReal(any2) && MayBeTakenAsReal(any3) => any3 * MathS.Log(any1, any2), Logf(var any1, var any1a) when any1 == any1a => new Providedf(1, any1 > 0), Logf(Divf(Integer(1), var any1), Divf(Integer(1), var any2)) => MathS.Log(any1, any2), Logf(var any1, Divf(Integer(1), var any2)) => -MathS.Log(any1, any2), @@ -263,6 +272,33 @@ internal static Entity GatherPowersOfOneBase(Entity x) /// a -- the same guard the ({}^{})^{} rule above carries, and for the /// same reason. https://github.com/asc-community/AngouriMath/issues/752 /// + /// + /// Whether is a real strictly above zero, decided rather than + /// assumed. ln of such a number is a real, so a real multiple of it stays on the + /// real line and inside ln's principal strip. + /// + /// + /// Finiteness is checked separately because is + /// !IsNegative && !IsZero, which NaN and +oo both satisfy. + /// + private static bool IsPositiveReal(Entity entity) + => entity.Evaled is Real { EDecimal.IsFinite: true } value && value.IsPositive; + + /// + /// Whether this operand may be taken as real: because the expression is being read as a + /// real-valued one, because the node's own declared codomain says so, or because its value + /// is a real to begin with. + /// + /// + /// The first two are the disjunction Patterns.EqualityInequality.cs uses to ask the + /// same question. A bare is Domain.Any, so a symbol under the + /// default complex reading answers here -- which is the point. + /// + private static bool MayBeTakenAsReal(Entity entity) + => MathS.Settings.Codomain.Value is AngouriMath.Core.Domain.Real + || IsKnownReal(entity) + || entity.Evaled is Real { EDecimal.IsFinite: true }; + private static (Entity Base, Entity Exponent) Decompose(Entity factor) { if (factor is not Powf(var @base, var exponent)) diff --git a/Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs b/Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs index a10ea3922..359576ce4 100644 --- a/Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs +++ b/Sources/Tests/UnitTests/Calculus/GruntzMovingExponentTest.cs @@ -42,7 +42,6 @@ private static void AssertLimit(string expression, string expected) => [InlineData("x ^ x / e ^ (x * ln(x))", "1")] [InlineData("e ^ (x * ln(x)) / x ^ x", "1")] [InlineData("x ^ (2 * x) / e ^ (2 * x * ln(x))", "1")] - [InlineData("(x ^ 2) ^ x / e ^ (2 * x * ln(x))", "1")] public void APowerAndItsExponentialAreOneFunction(string expression, string expected) => AssertLimit(expression, expected); @@ -53,11 +52,43 @@ public void APowerAndItsExponentialAreOneFunction(string expression, string expe /// [Theory] [InlineData("x ^ x / e ^ (x * ln(x) - x)", "+oo")] - [InlineData("x ^ x / e ^ (x * ln(x) - ln(x))", "+oo")] [InlineData("x ^ x / e ^ (x * ln(x) + x)", "0")] public void WhatIsLeftOverDecidesIt(string expression, string expected) => AssertLimit(expression, expected); + /// + /// Two of the cases above are no longer answered, and they are lost honestly: each comes + /// back as an unevaluated limit node rather than as a value, so the caller is told + /// that nothing was settled instead of being told something false. + /// + /// + /// Both need ln(a^c) = c * ln(a) — d/dx (x^2)^x carries ln(x^2), and + /// l'Hopital's rule reached it through Simplify. That identity is false off + /// ln's principal strip, so the simplifier no longer applies it + /// (https://github.com/asc-community/AngouriMath/issues/902), and as x -> +oo the base + /// really is positive, so what is missing here is a way to say so. + /// + /// Supplying it from the limit side does not reach: rewriting the expression before + /// Simplify is called does pull the exponent out, and Simplify's own + /// candidate search then writes (x^2)^x back into a logarithm and needs the + /// identity again. It is load-bearing *inside* the search, so restoring these two wants + /// an assumption travelling with the expression rather than another pre-pass. + /// + /// An unevaluated node is asserted rather than NaN deliberately: NaN would + /// claim the limit does not exist, and it does. If a value comes back here, the + /// assumption mechanism has arrived and these two rows belong back in the theories above. + /// + [Theory] + [InlineData("(x ^ 2) ^ x / e ^ (2 * x * ln(x))")] + [InlineData("x ^ x / e ^ (x * ln(x) - ln(x))")] + public void AnExponentUnderALogarithmIsNotReadForNow(string expression) + { + var limit = expression.ToEntity().Limit("x", "+oo".ToEntity()); + Assert.True(limit is Entity.Limitf, + $"{expression} came back as {limit.Stringize()}, which is a value rather than an " + + "unevaluated limit -- see this test's remarks before changing it"); + } + /// /// The claim the expected values above rest on, checked at a point rather than argued: /// the ratio is not merely close to 1, it is 1. diff --git a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs index 675df53fa..188b76c60 100644 --- a/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs +++ b/Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs @@ -585,6 +585,46 @@ public void ComposingAFunctionOverItsOwnInverseIsStillTheIdentity(string input) static double Magnitude(Entity difference) => ((System.Numerics.Complex)difference.EvalNumerical()).Magnitude; + // https://github.com/asc-community/AngouriMath/issues/902 + // log_b(a^c) = c * log_b(a) needs c * ln(a) to stay inside the strip Im in (-pi, pi] that + // ln maps onto, and it was applied to anything at all. ln(e^x) came back as x, which at + // x = 3*pi*i is 9.42i where the expression is pi*i -- e^(3*pi*i) being -1. The rewrite + // wins on complexity, so it is what an ordinary caller gets. + [Theory] + [InlineData("ln(e^x)")] + [InlineData("log(2, 2^x)")] + [InlineData("ln(x^2)")] + [InlineData("log(2, x^2)")] + public void AnExponentIsNotPulledOutOfALogarithmOverAnUndecidedArgument(string expression) => + Assert.Equal(expression.ToEntity(), expression.ToEntity().Simplify()); + + // The value is the point, so it is the value that is checked: at 3*pi*i the two forms + // differ by the full turn the principal branch discards. + [Fact] + public void TheLogarithmOfAPowerKeepsItsValueOffTheRealLine() + { + var original = "ln(e^x)".ToEntity(); + var at = "3 * pi * i".ToEntity(); + Assert.Equal(original.Substitute("x", at).EvalNumerical(), + original.Simplify().Substitute("x", at).EvalNumerical()); + } + + // Where both sides are decidable it still fires, and a real reading is enough to decide + // it: under Domain.Real the exponent is real by the reading itself. + [Theory] + [InlineData("ln(e^3)", "3")] + [InlineData("log(2, 2^5)", "5")] + [InlineData("ln(e^(1/2))", "1/2")] + public void AnExponentIsPulledOutWhereTheArgumentIsDecidable(string expression, string expected) => + Assert.Equal(expected.ToEntity().Simplify(), expression.ToEntity().Simplify()); + + [Fact] + public void ARealReadingDecidesTheExponent() + { + using var _ = MathS.Settings.Codomain.Set(AngouriMath.Core.Domain.Real); + Assert.Equal("x".ToEntity(), "ln(e^x)".ToEntity().Simplify()); + } + // https://github.com/asc-community/AngouriMath/issues/890 // log_b(1) is ln(1)/ln(b), which is 0/ln(b) -- so 0 for every base except 1, where it // is 0/0. The rewrite answered 0 for any base at all, so log(1, 1) was 0 where every