From 8619af881bbeb35a701c7435977d5a25659d7a72 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sat, 8 Aug 2026 00:04:58 +0000 Subject: [PATCH] Read the quotient in the limit instead of gathering it in the simplifier (#802) `a^n / b^n` was gathered into `(a/b)^n` unconditionally, and that is false across the branch cuts: sqrt(2)/sqrt(-3) is -0.8165i where (2/-3)^(1/2) is +0.8165i. It is the quotient twin of #801 and was left out of that fix, because guarding it cost *answers*: `(x^2 + 1)^x / (x^2)^x` stopped having a limit at all, which is the whole of #739 and #740. That framing was wrong, and this is the correction. The gathering was never the point -- #740 wanted it so the limit machinery could read a 1^oo out of a quotient, and its own test comment says so. The right place for the rewrite is therefore the limit reader, not the simplifier, because that is the only place where it can be justified: a limit needs the identity to hold in a neighbourhood of the destination, so requiring both bases to be eventually positive there is enough, and there is a destination to check that against. In the simplifier there is no destination and nothing to check, which is why it was unconditional. So ApplySecondRemarkable now recognises `a^n / b^n` itself, and the simplifier's rule takes the same guard its whole family carries. Every limit survives: (x^2 + 1)^x / (x^2)^x 1 unchanged (x^3 + 1)^x / (x^3)^x 1 unchanged (x - 5)^x / x^x e^(-5) unchanged (sqrt(x) + 1)^x / sqrt(x)^x unchanged sqrt(x) / sqrt(y) sqrt(x/y) -> unchanged, and correct at x=2, y=-3 Eleven tests in PowerQuotientGatheringTest moved from asserting the *mechanism* -- a single power in Simplify's output -- to asserting the *outcome* it existed for, which is that the limit is answered. That distinction is the whole content of this change, and the tests that pinned the mechanism were pinning something unsound. The four with symbolic bases no longer gather at all and now assert that simplifying does not change their value, since nothing can say a symbolic quotient stays on the principal branch. The test recording #802 as open is flipped to assert it stays fixed, which is what it was written to do. Unit 5543 pass 0 fail; F# 130/130; casbench 113/117 0 wrong; rootcheck 596/596; simpsweep 10463/10463; propcheck 0 failures. Co-Authored-By: Claude Opus 5 (1M context) --- .../Continuous/Limits/Transformations.cs | 32 +++++++++++ .../Simplification/Patterns/Patterns.Power.cs | 22 +++++--- .../Common/PowerQuotientGatheringTest.cs | 53 ++++++++++++++----- .../PatternsTest/PowerProductBranchTest.cs | 22 ++++---- 4 files changed, 97 insertions(+), 32 deletions(-) diff --git a/Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs b/Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs index 95d989477..6c350eed6 100644 --- a/Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs +++ b/Sources/AngouriMath/Functions/Continuous/Limits/Transformations.cs @@ -197,9 +197,41 @@ private static Entity ApplySecondRemarkable(Entity expr, Variable x, Entity dest EvalAssumingContinuous((xPlusOne - 1).Limit(x, dest)) == 0 && DivergesInMagnitude(xPower, x, dest) => MathS.e.Pow(xPower * (xPlusOne - 1)), + // a(x)^n / b(x)^n, the same limit written as a quotient. The simplifier used + // to gather this into (a/b)^n for us, which is how the shape reached the rule + // above at all -- and that gathering is false across the branch cuts, since + // sqrt(2)/sqrt(-3) is -0.8165i where (2/-3)^(1/2) is +0.8165i. + // https://github.com/asc-community/AngouriMath/issues/802 + // + // Read here instead, it is sound: a limit only needs the identity to hold in a + // neighbourhood of the destination, and both bases are required to be + // eventually positive on the way there -- where their arguments are both zero + // and there is no turn of the argument to lose. That is checkable, which is + // exactly what it is not in the simplifier, where the expression has no + // destination to be near. + Divf(Powf(var numeratorBase, var power), Powf(var denominatorBase, var powerAgain)) when + power == powerAgain && numeratorBase.ContainsNode(x) && denominatorBase.ContainsNode(x) + && power.ContainsNode(x) + && IsEventuallyPositive(numeratorBase, x, dest) && IsEventuallyPositive(denominatorBase, x, dest) + && EvalAssumingContinuous((numeratorBase / denominatorBase - 1).Limit(x, dest)) == 0 + && DivergesInMagnitude(power, x, dest) => + MathS.e.Pow(power * (numeratorBase / denominatorBase - 1)), + _ => expr }; + /// + /// Whether a base stays positive on the approach to , which is + /// what makes gathering a quotient of two powers into one power sound *here* when it + /// is not sound in general: two positive bases have argument zero apiece, so their + /// quotient's argument cannot leave the principal branch. + /// + private static bool IsEventuallyPositive(Entity expr, Variable x, Entity dest) + { + var limit = EvalAssumingContinuous(expr.Limit(x, dest)); + return limit == Real.PositiveInfinity || limit is Real { IsPositive: true }; + } + /// /// How many times over may be re-read into an /// expression that 's simplification diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs index 8f17ff7d2..4c22c6034 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Power.cs @@ -73,14 +73,20 @@ expr is Sumf(var any1, Mulf(Real { IsNegative: true } const1, var any2)) || (any1.Evaled is Real { IsPositive: true } && any2.Evaled is Real { IsPositive: true })) => new Powf(any1 * any2, any3), - // The quotient form has the same hole -- sqrt(2) / sqrt(-3) is -0.8165i while - // (2 / -3)^(1/2) is +0.8165i -- and is deliberately left unguarded, because - // guarding it costs answers rather than only shapes. It is what lets the limit - // machinery read a 1^oo out of a quotient, so `(x^2 + 1)^x / (x^2)^x` stops - // being answered at all, which is the whole of #739 and #740. Which of the two - // to prefer is a maintainer's call and is filed separately rather than taken - // here. https://github.com/asc-community/AngouriMath/issues/802 - Divf(Powf(var any1, var any3), Powf(var any2, var any3a)) when any3 == any3a => new Powf(any1 / any2, any3), + // Same condition, same reason -- sqrt(2) / sqrt(-3) is -0.8165i where + // (2 / -3)^(1/2) is +0.8165i. https://github.com/asc-community/AngouriMath/issues/802 + // + // This gathering was what let the limit machinery read a 1^oo out of a quotient, + // so guarding it here used to cost `(x^2 + 1)^x / (x^2)^x` its limit. The limit + // reader now recognises the quotient itself, where the identity is checkable + // because there is a destination to be near and the bases can be required to be + // positive on the way to it -- see ApplySecondRemarkable. + Divf(Powf(var any1, var any3), Powf(var any2, var any3a)) + when any3 == any3a + && (any3 is Integer + || (any1.Evaled is Real { IsPositive: true } + && any2.Evaled is Real { IsPositive: true })) + => new Powf(any1 / any2, any3), // {1} ^ n / {2} ^ (c * n) = ({1} / {2} ^ c) ^ n, and the same the other way up. // diff --git a/Sources/Tests/UnitTests/Common/PowerQuotientGatheringTest.cs b/Sources/Tests/UnitTests/Common/PowerQuotientGatheringTest.cs index 66309f0d6..03bc4c1c2 100644 --- a/Sources/Tests/UnitTests/Common/PowerQuotientGatheringTest.cs +++ b/Sources/Tests/UnitTests/Common/PowerQuotientGatheringTest.cs @@ -1,10 +1,11 @@ -// +// // Copyright (c) 2019-2022 Angouri. // AngouriMath is licensed under MIT. // Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. // Website: https://am.angouri.org. // +using System.Linq; using System.Threading.Tasks; using AngouriMath; using AngouriMath.Extensions; @@ -19,6 +20,19 @@ namespace AngouriMath.Tests.Common /// b^(c*p) on the child, on the way up, so by the time the pair is looked at it /// has already happened -- and where it applies to only one of the two, the exponents /// no longer match. https://github.com/asc-community/AngouriMath/issues/740 + /// + /// That gathering no longer happens in Simplify, and these tests moved with + /// it. (a/b)^p is not a^p / b^p across the branch cuts -- + /// sqrt(2)/sqrt(-3) is -0.8165i where (2/-3)^(1/2) is + /// +0.8165i -- so the rule is now conditioned like the rest of its family + /// (https://github.com/asc-community/AngouriMath/issues/802). + /// + /// Nothing is lost by that, because the gathering was a *means*: #740 wanted it so the + /// limit machinery could read a 1^oo out of a quotient. The limit reader now + /// recognises the quotient itself, where the identity is checkable -- there is a + /// destination to be near, and both bases can be required to stay positive on the way to + /// it. So the assertions below moved from the mechanism to the outcome it existed for: + /// they ask whether the limit is answered, not whether Simplify prints one power. /// [Trait("Area", "Common")] public sealed class PowerQuotientGatheringTest @@ -56,15 +70,23 @@ private static void AssertGathersIntoOnePower(string expr) $"{expr} came back as {simplified.Stringize()}, which is not a single power"); } + /// + /// The quotients #740 was about, asked as the question it was really asking: does the + /// limit come out? The shapes it used to assert -- a single power in Simplify's + /// output -- are no longer produced, and should not be: see the note on the class. + /// [Theory] - [InlineData("(a ^ 2 + 1) ^ x / (a ^ 2) ^ x")] [InlineData("(x ^ 2 + 1) ^ x / (x ^ 2) ^ x")] [InlineData("(x ^ 3 + 1) ^ x / (x ^ 3) ^ x")] - [InlineData("(a ^ 2) ^ x / b ^ x")] [InlineData("(x ^ 2) ^ x / (x ^ 2 + 1) ^ x")] - [InlineData("x ^ (2 * a) / y ^ a")] - public void AQuotientOfPowersGathersWhenOneBaseIsItselfAPower(string expr) => - AssertGathersIntoOnePower(expr); + [InlineData("(sqrt(x) + 1) ^ x / sqrt(x) ^ x")] + public void AQuotientOfPowersIsStillAnsweredAsALimit(string expr) + { + var limit = Task.Run(() => expr.ToEntity().Limit("x", "+oo").Simplify()); + Assert.True(limit.Wait(System.TimeSpan.FromSeconds(30)), $"{expr} did not terminate"); + Assert.False(limit.Result.Nodes.Any(node => node is Entity.Limitf), + $"{expr} came back unevaluated: {limit.Result.Stringize()}"); + } [Theory] [InlineData("(a ^ 2 + 1) ^ x / (a ^ 2) ^ x")] @@ -101,14 +123,19 @@ public void AQuotientWithNumericExponentsIsUnaffected(string expr) => Assert.False(Simplified(expr) is Entity.Powf, $"{expr} was gathered into {Simplified(expr).Stringize()}"); - // What already worked, and still does. + /// + /// These used to be asserted to gather into one power. They no longer do, because + /// their bases are symbolic and nothing can say the quotient stays on the principal + /// branch -- which is the whole of #802. What must still hold is that simplifying + /// them does not change what they are, so that is what is asserted. + /// [Theory] [InlineData("(y + 1) ^ x / y ^ x")] [InlineData("a ^ x / b ^ x")] [InlineData("(a ^ 2) ^ x / (b ^ 2) ^ x")] [InlineData("(x + 1) ^ (2 * x) / x ^ (2 * x)")] - public void TheQuotientsThatAlreadyGatheredStillDo(string expr) => - AssertGathersIntoOnePower(expr); + public void TheQuotientsThatNoLongerGatherKeepTheirValue(string expr) => + AssertSameValueAt(expr, ("a", "17/10"), ("b", "23/10"), ("x", "13/10"), ("y", "31/10")); /// /// The limits #739 fixed go through the same gathering, so they are pinned here as @@ -141,11 +168,11 @@ public void TheSecondRemarkableLimitStillReadsWhatGatheringGivesIt( /// run ahead of it. /// [Fact] - public void AFractionalExponentRatioGathersOnceNothingFlattensItFirst() + public void AFractionalExponentRatioKeepsItsValue() { - var simplified = Simplified("(sqrt(x) + 1) ^ x / sqrt(x) ^ x"); - Assert.True(simplified is Entity.Powf, - $"came back as {simplified.Stringize()}"); + // The gathering this used to assert is gone with #802, and the limit it was + // wanted for is covered by AQuotientOfPowersIsStillAnsweredAsALimit above. What + // is checked here is that simplifying still does not change the value. AssertSameValueAt("(sqrt(x) + 1) ^ x / sqrt(x) ^ x", ("x", "13/10")); } } diff --git a/Sources/Tests/UnitTests/PatternsTest/PowerProductBranchTest.cs b/Sources/Tests/UnitTests/PatternsTest/PowerProductBranchTest.cs index c3ba52834..ad4e4ef39 100644 --- a/Sources/Tests/UnitTests/PatternsTest/PowerProductBranchTest.cs +++ b/Sources/Tests/UnitTests/PatternsTest/PowerProductBranchTest.cs @@ -33,6 +33,7 @@ public sealed class PowerProductBranchTest [Theory] [InlineData("x ^ (1/2) * y ^ (1/2)")] [InlineData("sqrt(x) * sqrt(y)")] + [InlineData("sqrt(x) / sqrt(y)")] [InlineData("x ^ (1/3) * y ^ (1/3)")] [InlineData("x ^ (3/2) * y ^ (3/2)")] public void SimplifyingKeepsTheValueAtNegativeBases(string expr) @@ -51,25 +52,24 @@ public void SimplifyingKeepsTheValueAtNegativeBases(string expr) } /// - /// The quotient form has the same hole and is deliberately still open: - /// sqrt(2) / sqrt(-3) is -0.8165i while (2 / -3)^(1/2) is - /// +0.8165i. It is left because guarding it costs *answers* rather than only - /// shapes -- it is what lets the limit machinery read a 1^oo out of a quotient, and - /// with it guarded (x^2 + 1)^x / (x^2)^x stops having a limit at all, which - /// is the whole of #739 and #740. Pinned here so that the day it is fixed, this - /// test fails and says where to look. + /// The quotient form had the same hole -- sqrt(2) / sqrt(-3) is + /// -0.8165i where (2 / -3)^(1/2) is +0.8165i -- and is fixed + /// too. It was left out of the first pass because guarding it cost *answers*: the + /// gathering was what let the limit machinery read a 1^oo out of a quotient. + /// The limit reader now recognises the quotient itself, where the identity is + /// checkable, so the guard costs nothing. /// https://github.com/asc-community/AngouriMath/issues/802 /// [Fact] - public void TheQuotientFormIsStillWrongAndThatIsRecorded() + public void TheQuotientFormKeepsItsValueToo() { var simplified = "sqrt(x) / sqrt(y)".ToEntity().Simplify(); var before = "sqrt(x) / sqrt(y)".ToEntity().Substitute("x", 2).Substitute("y", -3).EvalNumerical(); var after = simplified.Substitute("x", 2).Substitute("y", -3).EvalNumerical(); Assert.True( - Math.Abs(before.ImaginaryPart.EDecimal.ToDouble() - after.ImaginaryPart.EDecimal.ToDouble()) > 1e-9, - $"the quotient form now agrees at x = 2, y = -3 -- #802 looks fixed, so this test " - + $"should become an assertion that it stays fixed. Simplified: {simplified.Stringize()}"); + Math.Abs(before.ImaginaryPart.EDecimal.ToDouble() - after.ImaginaryPart.EDecimal.ToDouble()) < 1e-9, + $"sqrt(x) / sqrt(y) simplified to {simplified.Stringize()}, which at x = 2, y = -3 " + + $"is {after.Stringize()} rather than {before.Stringize()}"); } ///