diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 76933adfb..59bd788e7 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -725,6 +725,21 @@ names are keywords now, and were names. | `preimage(x^2, x in RR, {1})` | `UnhandledParseException` | `{ 1, -1 }` | | `{ x in ZZ : x^2 in {1, 4} }` | `{ x in ZZ : x ^ 2 in { 1, 4 } }` — left as written | `{ 1, -1, 2, -2 }` | +### An infinite base has its whole powers, and surjectivity is decided through the image + +`(-oo)^3` was `NaN` — a claim that the value does not exist — and so were `(-oo)^2` and +`(-oo)^(-1)`, while `(+oo)^2` was `+oo`: the finite-base arms did not apply and the polar form +had nothing to say. They are the extended reals' powers now, `-oo`, `+oo` and `0`, so the image of +`(-oo; +oo)` under a cube is `(-oo; +oo)`; and `forall b in B : exists a in A : f(a) = b` — surjectivity +onto `B`, Def 7.4.1 of the reference of [#1409](https://github.com/asc-community/AngouriMath/issues/1409) +— is decided as `B` lying in the image of `A` under `f` where that image evaluates. + +| Input | Was (2.5.0) | Now | +|---|---|---| +| `(-oo)^3` | `NaN` — wrong | `-oo` | +| `(-oo)^2` | `NaN` — wrong | `+oo` | +| `forall b in RR : exists a in RR : a^3 = b` | `UnhandledParseException` (quantifiers are new since; left as written when they arrived) | `True` | +| `forall b in RR : exists a in RR : e^a = b` | `UnhandledParseException` | `False` | ### The binomial coefficient's identities, and its sums in closed form Pascal's rule, the chairperson identity and the symmetry are rewrite rules, each in the direction diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 40ba68a05..b20340290 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -291,6 +291,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [AngouriMath/Functions/NumberTheory/ResidueClasses.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n +[Tests/UnitTests/Core/SurjectivityTest.cs] +file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n + [Tests/UnitTests/Core/BinomialIdentityTest.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n diff --git a/Sources/AngouriMath/Core/Entity/Continuous/Number/Operators.cs b/Sources/AngouriMath/Core/Entity/Continuous/Number/Operators.cs index 7373218ca..ffc8c2ed2 100644 --- a/Sources/AngouriMath/Core/Entity/Continuous/Number/Operators.cs +++ b/Sources/AngouriMath/Core/Entity/Continuous/Number/Operators.cs @@ -498,6 +498,17 @@ static Complex BinaryIntPow(Complex num, EInteger val) && decimalPower.IsInteger() && decimalPower.Abs().CompareTo(EDecimal.FromInt32(1 << 20)) <= 0 => decimalPower.ToEInteger(), _ => null, }; + // An infinite real base to a whole power: (+oo)^n is +oo, (-oo)^n is +oo or -oo by + // the parity of n, and either to a negative power is 0 -- the extended reals' + // arithmetic, which the product of infinities already follows. It fell through + // to the polar form and came back NaN, so the image of (-oo; +oo) under a cube + // had no ends. https://github.com/asc-community/AngouriMath/issues/1409 + if (@base is Real { EDecimal: var infinite } && infinite.IsInfinity() && pow is { } wholeOfInfinity && !wholeOfInfinity.IsZero) + { + if (wholeOfInfinity.Sign < 0) + return Integer.Zero; + return infinite.IsNegative && !wholeOfInfinity.IsEven ? Real.NegativeInfinity : Real.PositiveInfinity; + } if (@base.IsFinite && pow is { }) { // A real base that is not exact -- a decimal, which is what a numerical diff --git a/Sources/AngouriMath/Functions/Boolean/Quantifiers.cs b/Sources/AngouriMath/Functions/Boolean/Quantifiers.cs index 0ef1da4f2..9001f65ce 100644 --- a/Sources/AngouriMath/Functions/Boolean/Quantifiers.cs +++ b/Sources/AngouriMath/Functions/Boolean/Quantifiers.cs @@ -81,6 +81,18 @@ internal enum Kind { All, Some, Unique } set = new FiniteSet(Entity.Boolean.True, Entity.Boolean.False); if (!body.ContainsNode(x)) return Closed(kind, set, body); + // forall b in B : exists a in A : f(a) = b is the statement that B lies in the image + // of A under f -- surjectivity onto B (the reference's Def 7.4.1) -- and the image is + // a set the library computes: listed over a listed A, an interval by interval + // arithmetic, so the subset decision settles it where the image evaluates. + // https://github.com/asc-community/AngouriMath/issues/1409 + if (kind == Kind.All && body is Existsf(Variable a, Set domain, Equalsf(var lhs, var rhs)) + && (lhs == x && !rhs.ContainsNode(x) && rhs.ContainsNode(a) ? rhs : rhs == x && !lhs.ContainsNode(x) && lhs.ContainsNode(a) ? lhs : null) is { } map) + { + var image = new IndexedUnionf(a, domain, new FiniteSet(map)).InnerSimplified(isExact); + if (image is not IndexedUnionf && image is Set imageSet && Core.Sets.SetOperators.Subset(set, imageSet, isExact) is { } covered) + return covered; + } // An equation whose two sides differ by a polynomial that expands to nothing holds // at every member, whatever the set: (x + 1)^2 = x^2 + 2 x + 1 is True of each. if (body is Equalsf(var left, var right) && IsIdentity(left, right)) diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs index 5e2cb04e7..a2ab797b6 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Omni/Evaluation.Omni.Classes.cs @@ -203,9 +203,11 @@ protected override Entity InnerSimplify(bool isExact) // one occurrence and the operations it has images for (#1423): the // reference's 9c/5 + 32 on (0, 100) is (32, 212). Where the arithmetic has // no image the substitution leaves an expression, and the family stays. - if (this is IndexedUnionf && over is Interval && body is FiniteSet { Count: 1 } image + // The reals are the interval (-oo; +oo) for this purpose. + var overAsInterval = over is SpecialSet.Reals ? new Interval(Real.NegativeInfinity, false, Real.PositiveInfinity, false) : over; + if (this is IndexedUnionf && overAsInterval is Interval && body is FiniteSet { Count: 1 } image && image.First() is var f && f.Nodes.Count(node => node == Var) == 1 - && f.Substitute(Var, over).InnerSimplified(isExact) is Set imaged) + && f.Substitute(Var, overAsInterval).InnerSimplified(isExact) is Set imaged) return imaged; if (over is FiniteSet indices) { diff --git a/Sources/Tests/UnitTests/Core/SurjectivityTest.cs b/Sources/Tests/UnitTests/Core/SurjectivityTest.cs new file mode 100644 index 000000000..313e3d880 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/SurjectivityTest.cs @@ -0,0 +1,50 @@ +// +// Copyright (c) 2019-2026 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; + +namespace AngouriMath.Tests.Core +{ + /// + /// forall b in B : exists a in A : f(a) = b -- surjectivity onto B, Def 7.4.1 of the + /// reference (Sullivan and Mackey) -- is the statement that B lies in the image of + /// A under f, and is decided where the image evaluates: listed over a listed + /// A, an interval by interval arithmetic. The cube is onto the reals because + /// (-oo; +oo)^3 is (-oo; +oo), which needed (-oo)^3 to be -oo + /// rather than NaN. + /// + [Trait("Area", "Core")] + public sealed class SurjectivityTest + { + [Theory] + [InlineData("forall b in RR : exists a in RR : a^3 = b", "True")] + [InlineData("forall b in RR : exists a in RR : 2 a + 1 = b", "True")] + [InlineData("forall b in RR : exists a in RR : a^2 = b", "False")] + [InlineData("forall b in [0; +oo) : exists a in RR : a^2 = b", "True")] + [InlineData("forall b in RR : exists a in RR : e^a = b", "False")] + [InlineData("forall b in (0; +oo) : exists a in RR : e^a = b", "True")] + [InlineData("forall b in ZZ : exists a in ZZ : 2 a = b", "False")] + [InlineData("forall b in {1, 4, 9} : exists a in {1, 2, 3} : a^2 = b", "True")] + [InlineData("forall b in {1, 4, 9, 16} : exists a in {1, 2, 3} : a^2 = b", "False")] + public void SurjectivityIsTheImageCoveringTheCodomain(string statement, string expected) + => Assert.Equal(expected.ToEntity(), statement.ToEntity().Evaled); + + /// The extended reals' whole powers: by parity for -oo, and 0 for a negative exponent. Each was NaN. + [Theory] + [InlineData("(-oo)^3", "-oo")] + [InlineData("(-oo)^2", "+oo")] + [InlineData("(-oo)^(-1)", "0")] + [InlineData("(+oo)^3", "+oo")] + [InlineData("(-oo; +oo)^3", "(-oo; +oo)")] + [InlineData("image(x^3, x in RR)", "(-oo; +oo)")] + public void AnInfiniteBaseHasItsWholePowers(string expression, string expected) + => Assert.Equal(expected.ToEntity().Evaled, expression.ToEntity().Evaled); + } +}