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