From 81192db98fe18a21e69f0346ebc3465c903277c6 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 23 Aug 2026 23:29:52 +0000 Subject: [PATCH] Do not answer an exhausted search with the empty set (#1036, #746 tier 4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Solve` returned an empty `FiniteSet` both for an equation shown to have no roots and for one every solver declined. The empty set is a positive claim, so the second was a wrong answer: `x^6 + x*y + 1 = 0` has six roots for every `y` and came back as `{ }`. The two exits that mean "nothing settled this" now answer with the equation as a set builder — the spelling `AnalyticalEquationSolver` already uses for #278 and #964 — while an equation whose emptiness was established keeps `{ }`. Newton's method is included: a search from finitely many starting points inside a bounded region finding nothing is a fact about the search. A conjunction with an unsettled side is answered as the conjunction. Intersecting a finite set with a condition keeps the elements whose membership could not be decided, so `x^6 + x*y + 1 = 0 and x - 1 = 0` would have become `{ 1 }` — one false claim in place of another, since 1 solves the first only at `y = -2`. Four theory rows recorded the old answer as correct. Each pinned an equation the solver gives up on and that has roots, so they move to the new test file with the honest assertion rather than being loosened. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd --- BREAKING-CHANGES.md | 102 ++++++++++ Sources/AngouriMath/Convenience/MathS.cs | 6 +- .../AnalyticalEquationSolver.cs | 38 +++- .../Solvers/EquationSolver/SolveStatement.cs | 21 ++- .../Continuous/Solvers/Solvers.Definition.cs | 2 +- .../Algebra/SolveTest/SolveOneEquation.cs | 4 - .../Algebra/SolveTest/UnsolvedEquationTest.cs | 174 ++++++++++++++++++ 7 files changed, 335 insertions(+), 12 deletions(-) create mode 100644 Sources/Tests/UnitTests/Algebra/SolveTest/UnsolvedEquationTest.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 8a3449e9b..fe17f59d0 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -21,6 +21,9 @@ read first. | Silent? | What | Was | Is | |---|---|---|---| +| **Silent** | `"x6 + x y + 1 = 0".ToEntity().Solve("x")`, and every equation no solver settles | `{ }` — there are no roots | `{ x : 1 + x ^ 6 + x * y = 0 }` — these are the roots, whichever they are | +| **Silent** | `"(x - 1) * (x6 + x y + 1) = 0".ToEntity().Solve("x")` | `{ 1 }` | `{ 1 } \/ { x : 1 + x ^ 6 + x * y = 0 }` | +| **Silent** | `"x6 + x y + 1 = 0 and x - 1 = 0".ToEntity().Solve("x")` | `{ }` | `{ x : x ^ 6 + x * y + 1 = 0 and x - 1 = 0 }` | | | `"x ^ 3 - x > 0".ToEntity().Solve("x")`, and every polynomial inequality of degree three or more | `NotSufficientlySupportedException: Only linear and quadratic polynomial inequalities are supported` | `(-1; 0) \/ (1; +oo)` — the solution set | | **Silent** | `"a implies (b implies c)".ToEntity().Stringize()` | `a implies b implies c`, which reads back as `(a implies b) implies c` | `a implies (b implies c)` | | | `"(a implies b) implies c".ToEntity().Stringize()` | `(a implies b) implies c` | `a implies b implies c` | @@ -35,6 +38,105 @@ read first. | | `Compile` to a nullable integral return type in a NativeAOT app | `AngouriBugException: IsNaN method expected for type System.Double`, which took the process down | the compiled function | | **Silent** | an app publishing with `PublishTrimmed` or NativeAOT | `AngouriMath.dll` was copied in whole, being unmarked | it is trimmed with the rest, since the assembly now declares `IsTrimmable` | +### An equation nothing settled is no longer answered with the empty set + +`Solve` and `SolveEquation` returned an empty `FiniteSet` for two different things: an equation +shown to have no roots, and an equation every solver in the chain declined. The empty set is a +positive claim — *no x satisfies this* — so the second of those was a wrong answer rather than a +graceful failure ([#1036](https://github.com/asc-community/AngouriMath/issues/1036), +[#746](https://github.com/asc-community/AngouriMath/issues/746) tier 4). + +**Was** — indistinguishable, and false for the second column: + +``` +"x6 + x y + 1 = 0".ToEntity().Solve("x") { } six roots for every y +"sin(x) + x + y = 0".ToEntity().Solve("x") { } +"e^x + x + y = 0".ToEntity().Solve("x") { } +"x6 + x y + 1".ToEntity().SolveEquation("x") { } +"e^x = 0".ToEntity().Solve("x") { } genuinely none +"abs(x) = -1".ToEntity().Solve("x") { } genuinely none +``` + +**Is** — the equation itself, as the set of the x that satisfy it. It names the same set and +asserts of it only what was established: + +``` +"x6 + x y + 1 = 0".ToEntity().Solve("x") { x : 1 + x ^ 6 + x * y = 0 } +"sin(x) + x + y = 0".ToEntity().Solve("x") { x : sin(x) + x = -y } +"e^x + x + y = 0".ToEntity().Solve("x") { x : e ^ x + x = -y } +"x6 + x y + 1".ToEntity().SolveEquation("x") { x : 1 + x ^ 6 + x * y = 0 } +"e^x = 0".ToEntity().Solve("x") { } unchanged +"abs(x) = -1".ToEntity().Solve("x") { } unchanged +``` + +Turning Newton's method off leaves nothing numerical either, and those answers move the same way. +A search over finitely many starting points inside a bounded region finding nothing is a fact about +the search: + +``` +using var _ = MathS.Settings.AllowNewton.Set(false); + +"x5 + 3x + 1 = 0".ToEntity().Solve("x") was { } is { x : x ^ 5 + 3 * x = -1 } +"sin(x) * x - 3 = 0".ToEntity().Solve("x") was { } is { x : sin(x) * x = 3 } + +"x + sqrt(x^0.1 + a) + c".ToEntity().SolveEquation("x") + was { } is { x : sqrt(a + x ^ (1/10)) + c + x = 0 } +"(x + 6)^(1/6) + x + x3 + a".ToEntity().SolveEquation("x") + was { } is { x : (6 + x) ^ (1/6) + x + x ^ 3 = -a } +"2 ^ (x sin(x)) + 4 ^ (x sin(x)) + c".ToEntity().SolveEquation("x") + was { } + is { x : sin(x) * x = ln(((-1 - sqrt(1 - 4 * c)) / 2) ^ (1 / ln(2))) + or sin(x) * x = ln(((-1 + sqrt(1 - 4 * c)) / 2) ^ (1 / ln(2))) } +``` + +The last of those is the shape of it: the exponential solver did settle the equation in +`2 ^ (x sin(x))`, and it was the inversion of `x * sin(x)` that had nothing to say. What comes back +now is the half that was solved, with the half that was not left standing as a condition. + +An answer that is partly settled keeps the part that is, so a product one of whose factors was +solved comes back as a union rather than as the factor's roots alone: + +``` +"(x - 1) * (x6 + x y + 1) = 0".ToEntity().Solve("x") + was { 1 } + is { 1 } \/ { x : 1 + x ^ 6 + x * y = 0 } + +"x6 + x y + 1 = 0 or x - 1 = 0".ToEntity().Solve("x") + was { 1 } + is { 1 } \/ { x : 1 + x ^ 6 + x * y = 0 } + +"x6 + x y + 1 = 0 implies x - 1 = 0".ToEntity().Solve("x") + was { 1 } \/ BB + is { 1 } \/ (BB \ { x : 1 + x ^ 6 + x * y = 0 }) +``` + +A conjunction with an unsettled side is answered as the conjunction. Intersecting a finite set with +a condition keeps the elements whose membership could not be decided, so taking the intersection +here would have replaced one false claim with another — `{ 1 }` says 1 solves +`x^6 + x*y + 1 = 0`, and it does so only at `y = -2`: + +``` +"x6 + x y + 1 = 0 and x - 1 = 0".ToEntity().Solve("x") + was { } + is { x : x ^ 6 + x * y + 1 = 0 and x - 1 = 0 } +``` + +**What this means for callers.** `Solve` has always been typed `Set` and has always been able to +return an `Interval`, a `ConditionalSet` or a union; what changes is how often it does. Code that +casts the result to `FiniteSet`, or that reads an empty result as "no solutions", has to say which +of the two it means: + +```csharp +var answer = equation.Solve(x); +if (answer is FiniteSet roots) { /* these are all of them */ } +else if (answer.IsSetEmpty) { /* shown to have none */ } +else { /* not settled, or not finite */ } +``` + +Nothing that solved before stops solving, and no equation that was shown to have no roots gains +any. Solving `x2 - 4 = 0`, `sin(x) = 1/2`, `x2 + 1 = 0` and the system solver's answers are +unchanged, as is `Solve` on an inequality. + ### A polynomial inequality of degree three or more is answered **Was** — every univariate polynomial inequality above degree two was refused outright, whatever its diff --git a/Sources/AngouriMath/Convenience/MathS.cs b/Sources/AngouriMath/Convenience/MathS.cs index c8a00f93b..fb38e4434 100644 --- a/Sources/AngouriMath/Convenience/MathS.cs +++ b/Sources/AngouriMath/Convenience/MathS.cs @@ -5652,7 +5652,9 @@ internal static EDecimal DowncastingTolerance } /// - /// If you only need analytical solutions and an empty set if no analytical solutions were found, disable Newton's method + /// If you only need analytical solutions, disable Newton's method. What comes back + /// where there are none is the equation itself as a set builder: the empty set + /// would say the equation has no roots, which is a claim nothing established. /// /// /// @@ -5671,7 +5673,7 @@ internal static EDecimal DowncastingTolerance /// { 1.0050669478588620808778841819730587303638458251953125 + 0.93725915669289194820379407246946357190608978271484375i, /// ... omitting here most of the output, because it's huge /// } - /// { } // nothing was found for 5-degree polynomial without numeric solution + /// { x : x ^ 5 + 3 * x = -1 } // no analytical solution was found for this quintic /// /// public static Setting AllowNewton { get; } = true; diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/AnalyticalEquationSolver.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/AnalyticalEquationSolver.cs index bc0d23715..46d4f61b7 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/AnalyticalEquationSolver.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/AnalyticalEquationSolver.cs @@ -330,11 +330,43 @@ bool ProductIsDefinedAt(Entity root) // TODO: Solve factorials (Needs Lambert W function) // https://mathoverflow.net/a/28977 - // if nothing has been found so far + // A numerical search that comes back with nothing has not shown there is + // nothing to find: Newton's method is started from finitely many points inside + // a bounded region, so an empty result is a fact about the search rather than + // about the equation. Where it does find roots the answer is theirs, unchanged. if (MathS.Settings.AllowNewton && expr.Vars.Count == 1) - return expr.SolveNt(x).Select(ent => TryDowncast(expr, x, ent)).ToSet(); + return expr.SolveNt(x).Select(ent => TryDowncast(expr, x, ent)).ToSet() + is FiniteSet { IsSetEmpty: false } found ? found : Unsolved(expr, x); - return Enumerable.Empty().ToSet(); + return Unsolved(expr, x); } + + /// + /// The answer when every solver above has declined: the equation itself, as the set + /// of the that satisfy it. + /// + /// + /// The empty set is a positive claim -- that no satisfies + /// -- and returning it from an exhausted search asserts + /// something nothing here established. x^6 + x*y + 1 = 0 has six roots for + /// every y and was answered { }. A condition asserts only what was + /// established, which is that these are the roots, whichever they are; the set is + /// still exactly the solution set, so nothing downstream is told anything false. + /// + /// The spelling is the one + /// and the #278 + /// case above already use, rather than a second way of saying the same thing. + /// #1036, + /// #746 + /// + private static Set Unsolved(Entity equation, Variable x) + // Written back as an equation between the two sides where there are two, rather + // than as the residual the solvers pass around. A compensated call is handed its + // equation unsimplified on purpose, so the difference survives for them to read, + // and stating it as it stands leaves the reader `x^5 + 3*x - (-1) = 0` where the + // question was whether `x^5 + 3*x` is -1. The two admit the same x. + => new ConditionalSet(x, equation is Minusf(var lhs, var rhs) + ? lhs.Equalizes(rhs) + : equation.Equalizes(0)); } } diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs index cda428515..be14c2c79 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/EquationSolver/SolveStatement.cs @@ -148,6 +148,23 @@ private static EDecimal LargestTerm(Entity substituted) return largest; } + /// + /// Where both sides of a conjunction were settled, its solution set is the + /// intersection of theirs. + /// + /// + /// Where one of them is a condition nothing settled, it is not: intersecting a + /// finite set with one keeps an element whose membership could not be decided, so + /// x^6 + x*y + 1 = 0 and x - 1 = 0 comes back as { 1 } — and 1 is a + /// root of the first only when y is -2. The conjunction as written asserts + /// exactly what is known about it and nothing more. + /// #1036 + /// + private static Set Conjunction(Set left, Set right, Entity statement, Variable x) + => (left, right) is (ConditionalSet, FiniteSet) or (FiniteSet, ConditionalSet) + ? new ConditionalSet(x, statement) + : (Set)MathS.Intersection(left, right); + internal static Set Solve(Entity expr, Variable x) => expr switch { @@ -161,8 +178,8 @@ internal static Set Solve(Entity expr, Variable x) Equalsf => Empty, - Andf(var left, var right) => - MathS.Intersection(Solve(left, x), Solve(right, x)), + Andf(var left, var right) => + Conjunction(Solve(left, x), Solve(right, x), expr, x), Orf(var left, var right) => MathS.Union(Solve(left, x), Solve(right, x)), Impliesf(var left, var right) => diff --git a/Sources/AngouriMath/Functions/Continuous/Solvers/Solvers.Definition.cs b/Sources/AngouriMath/Functions/Continuous/Solvers/Solvers.Definition.cs index 0c0fc5ef9..d1f88d9c2 100644 --- a/Sources/AngouriMath/Functions/Continuous/Solvers/Solvers.Definition.cs +++ b/Sources/AngouriMath/Functions/Continuous/Solvers/Solvers.Definition.cs @@ -84,7 +84,7 @@ partial record Entity /// { 9.08837698687877... } /// ----------------- /// sin(x) * x - 3 = 0 - /// { } + /// { x : sin(x) * x = 3 } /// /// public Set Solve(Variable var) diff --git a/Sources/Tests/UnitTests/Algebra/SolveTest/SolveOneEquation.cs b/Sources/Tests/UnitTests/Algebra/SolveTest/SolveOneEquation.cs index e50b8c79d..976788849 100644 --- a/Sources/Tests/UnitTests/Algebra/SolveTest/SolveOneEquation.cs +++ b/Sources/Tests/UnitTests/Algebra/SolveTest/SolveOneEquation.cs @@ -189,9 +189,6 @@ public void InvertedFunctions(string func, int rootAmount) public void CDSolver(string expr, int rootCount, string? verifyRoots) => TestSolver(expr, rootCount, verifyRoots: verifyRoots); [Theory] - [InlineData("x + sqrt(x^0.1 + a) + c", 0)] - [InlineData("(x + 6)^(1/6) + x + x3 + a", 0)] - [InlineData("sqrt(x + 1) + sqrt(x + 2) + a + x", 0)] [InlineData("(x + 1)^(1/3) - x - a", 3)] public void FractionedPoly(string expr, int rootCount) => TestSolver(expr, rootCount); @@ -233,7 +230,6 @@ public void InvertedFunctions(string func, int rootAmount) [InlineData("4^x - a", 1, "{ log(4, a) }")] [InlineData("a^x + (a^2)^x - c", 2)] [InlineData("e^x + (e2)^x - 1", 2)] - [InlineData("2 ^ (x sin(x)) + 4 ^ (x sin(x)) + c", 0)] [InlineData("2^x - 4^x", 1, "{ 0 }")] public void TestExponentialSolver(string equation, int rootCount, string? verifyRoots = null) => TestSolver(equation, rootCount, verifyRoots: verifyRoots); diff --git a/Sources/Tests/UnitTests/Algebra/SolveTest/UnsolvedEquationTest.cs b/Sources/Tests/UnitTests/Algebra/SolveTest/UnsolvedEquationTest.cs new file mode 100644 index 000000000..a8c69bf73 --- /dev/null +++ b/Sources/Tests/UnitTests/Algebra/SolveTest/UnsolvedEquationTest.cs @@ -0,0 +1,174 @@ +// +// 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 AngouriMath; +using AngouriMath.Extensions; +using Xunit; +using static AngouriMath.Entity.Set; + +namespace AngouriMath.Tests.Algebra.SolveTest +{ + /// + /// An equation the solvers exhaust themselves on, against one that has been shown to + /// have no roots. Both were the empty set. + /// https://github.com/asc-community/AngouriMath/issues/1036 + /// + /// + /// The empty set is a positive mathematical claim, so it is only available where + /// something established it. Where nothing did, the answer is the equation as a set + /// builder: it names the same set, and asserts of it only what is known. + /// + [Trait("Area", "Algebra")] + public sealed class UnsolvedEquationTest + { + /// An equation no solver settles comes back as a condition, not as no roots. + [Theory] + [InlineData("x6 + x y + 1 = 0")] + [InlineData("sin(x) + x + y = 0")] + [InlineData("e^x + x + y = 0")] + [InlineData("x y + sin(x) ^ 2 + ln(x) = 0")] + public void ExhaustedIsNotEmpty(string equation) + { + var answer = equation.ToEntity().Solve("x"); + Assert.False(answer.IsSetEmpty, $"{equation} answered the empty set"); + Assert.IsType(answer); + } + + /// + /// The same for the entry point that takes the equation as an expression read as + /// equal to zero, which reaches the solver by its own route. + /// + [Theory] + [InlineData("x6 + x y + 1")] + [InlineData("sin(x) + x + y")] + public void ExhaustedIsNotEmptyThroughSolveEquation(string expression) + { + Assert.False(expression.ToEntity().SolveEquation("x").IsSetEmpty); + Assert.False(MathS.SolveEquation(expression.ToEntity(), "x").IsSetEmpty); + } + + /// + /// An equation shown to have no roots keeps the empty set. e^x is never zero + /// and abs(x) is never negative, and in both cases the solver reached that by + /// inverting rather than by running out of ideas. + /// + [Theory] + [InlineData("e^x = 0")] + [InlineData("abs(x) = -1")] + public void ImpossibleIsStillEmpty(string equation) + { + var answer = equation.ToEntity().Solve("x"); + Assert.IsType(answer); + Assert.True(answer.IsSetEmpty, $"{equation} stopped answering the empty set"); + } + + /// + /// The two are distinguishable, which is the whole point: one is empty and the other + /// is not, where before both were { }. + /// + [Fact] + public void ExhaustedAndImpossibleDisagree() + { + var exhausted = "x6 + x y + 1 = 0".ToEntity().Solve("x"); + var impossible = "e^x = 0".ToEntity().Solve("x"); + Assert.NotEqual(exhausted.IsSetEmpty, impossible.IsSetEmpty); + } + + /// + /// The condition admits a root that the empty set denied. x^6 + x*y + 1 = 0 + /// has six roots for every y; at y = -2 one of them is 1. + /// + [Fact] + public void TheConditionAdmitsARootTheEmptySetDenied() + { + var answer = Assert.IsType("x6 + x y + 1 = 0".ToEntity().Solve("x")); + var atTheRoot = answer.Predicate.Substitute("y", -2).Substitute("x", 1).Simplify(); + Assert.Equal(Entity.Boolean.True, atTheRoot); + } + + /// + /// Newton's method is asked from finitely many starting points inside a bounded + /// region, so finding nothing is a fact about the search. With it turned off there + /// is nothing numerical left either, and both of these were { }. + /// + [Theory] + [InlineData("x5 + 3x + 1 = 0")] + [InlineData("sin(x) * x - 3 = 0")] + [InlineData("2 ^ (x sin(x)) + 4 ^ (x sin(x)) + c = 0")] + [InlineData("x + sqrt(x^0.1 + a) + c = 0")] + [InlineData("(x + 6)^(1/6) + x + x3 + a = 0")] + [InlineData("sqrt(x + 1) + sqrt(x + 2) + a + x = 0")] + public void WithoutNewtonTheAnswerIsTheEquation(string equation) + { + using var _ = MathS.Settings.AllowNewton.Set(false); + var answer = equation.ToEntity().Solve("x"); + Assert.False(answer.IsSetEmpty, $"{equation} answered the empty set"); + Assert.IsType(answer); + } + + /// + /// And where Newton does find roots they are still the answer, so nothing that + /// answered before stops answering. + /// + [Theory] + [InlineData("x5 + 3x + 1 = 0")] + [InlineData("sin(x) * x - 3 = 0")] + public void NewtonStillAnswers(string equation) + { + var answer = Assert.IsType(equation.ToEntity().Solve("x")); + Assert.False(answer.IsSetEmpty); + } + + /// + /// A conjunction with an unsettled side must not name a root. Intersecting a finite + /// set with a condition keeps an element whose membership could not be decided, so + /// { 1 } here would say 1 is a root of x^6 + x*y + 1, which it is only + /// at y = -2. + /// + [Fact] + public void AConjunctionDoesNotNameARootItCannotCheck() + { + var answer = "x6 + x y + 1 = 0 and x - 1 = 0".ToEntity().Solve("x"); + Assert.IsType(answer); + Assert.False(answer.TryContains(1, out var contains) && contains, + "the conjunction asserted that 1 is a solution"); + } + + /// A conjunction of two settled sides still intersects them. + [Fact] + public void ASettledConjunctionStillIntersects() + { + var answer = Assert.IsType( + "(x - 3) * (x - 6) = 0 and (x - 3) * (x - 7) = 0".ToEntity().Solve("x")); + Assert.Equal(new FiniteSet(3), answer); + } + + /// + /// A disjunction is a union, and a union with an unsettled side is exactly right: + /// the roots that were found, together with the ones nothing settled. + /// + [Fact] + public void ADisjunctionKeepsTheRootsItFound() + { + var answer = "x6 + x y + 1 = 0 or x - 1 = 0".ToEntity().Solve("x"); + Assert.True(answer.TryContains(1, out var contains) && contains, + "the disjunction lost the root it had"); + } + + /// + /// An equation that solves is untouched, including the one that has every complex + /// number as a root and the one that has none because it says nothing about x. + /// + [Theory] + [InlineData("x2 - 4 = 0", 2)] + [InlineData("x2 + 1 = 0", 2)] + [InlineData("(x - 1)(x2 - 3) = 0", 3)] + [InlineData("sin(x) = 1/2", 2)] + public void SolvingIsUnchanged(string equation, int rootCount) + => Assert.Equal(rootCount, Assert.IsType(equation.ToEntity().Solve("x")).Count); + } +}