diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index cfb539286..148ef6384 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -388,6 +388,26 @@ truth value at any other ([#2195](https://github.com/asc-community/AngouriMath/i | `"x in [0; 1]".ToEntity().Compile("x").Call(0.5)` | `UncompilableNodeException` | `(1, 0)` | | `"3 divides x".ToEntity().Compile("x").Call(6)` | `UncompilableNodeException` | `(1, 0)` | +### A quantifier, a subset and a cardinality over a finite set compile + +**Not silent: what was refused is compiled.** A quantifier, a subset and a cardinality were refused by both +compilers with `UncompilableNodeException`. Over a finite set, of at most 64 members, each now compiles to what +evaluation gives: +- `forall` and `exists` are the conjunction and the disjunction of the body at each member, and `exists!` is + exactly one of them, by Kleene's connectives; +- a finite set is a subset where each of its members is a member of the other set; +- a cardinality is the number of distinct values among the members. + +Over any other set each is refused as before. At a `NaN` argument the compiled value is undecided, or the vacuous +truth of a quantifier over the empty set, where evaluation drops a `NaN` member from a finite set +([#2195](https://github.com/asc-community/AngouriMath/issues/2195)). + +| Input | Was (2.6.0) | Now | +|---|---|---| +| `"forall t in { 1, 2, 3 } : t < x".ToEntity().Compile("x").Call(4)` | `UncompilableNodeException` | `(1, 0)` | +| `"{ x } subset [0; 3]".ToEntity().Compile("x")(0.5)` | `UncompilableNodeException` | `True` | +| `"card({ 1, x })".ToEntity().Compile("x").Call(1)` | `UncompilableNodeException` | `(1, 0)` | + ### A congruence compiles **Not silent: what was refused is compiled.** `a = b (mod n)` was refused by both compilers with diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 60be78b3b..eae3ab026 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -917,6 +917,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [Tests/UnitTests/Common/StatementInANumericPositionTest.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/Common/FiniteSetStatementCompilationTest.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/Convenience/EulerGammaTest.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/Functions/Compilation/CompiledMembership.cs b/Sources/AngouriMath/Functions/Compilation/CompiledMembership.cs index 54d0c384c..b08606684 100644 --- a/Sources/AngouriMath/Functions/Compilation/CompiledMembership.cs +++ b/Sources/AngouriMath/Functions/Compilation/CompiledMembership.cs @@ -25,10 +25,64 @@ namespace AngouriMath.Core.Compilation internal static class CompiledMembership { internal static Entity Rewritten(Entity expression) - => expression.Nodes.Any(node => node is Inf) - ? expression.Replace(node => node is Inf(var element, var set) && Statement(element, set) is { } statement ? statement : node) + => expression.Nodes.Any(node => node is Inf or Subsetf or Cardf or Quantifier) + ? expression.Replace(Rewrite) : expression; + // Past this many members a statement over a finite set is left as written: the cardinality and the + // unique existence grow with the square of the count. + private const int LargestExpanded = 64; + + // A subset, a cardinality and a quantifier over a finite set are statements about its members, as evaluation + // decides them, and any other is left as written, which neither compiler compiles. + // https://github.com/asc-community/AngouriMath/issues/2195 + private static Entity Rewrite(Entity node) => node switch + { + Inf(var element, var set) => Statement(element, set) ?? node, + Subsetf(FiniteSet sub, var super) when sub.Count <= LargestExpanded + => sub.Select(member => Statement(member, super)).ToList() is var each && each.All(statement => statement is not null) + ? each.Aggregate(Boolean.True as Entity, (all, statement) => all & statement!) + : node, + Cardf(FiniteSet set) when set.Count <= LargestExpanded => Cardinality(set.ToList()), + Forallf(var variable, FiniteSet over, var body) when over.Count <= LargestExpanded + => over.Aggregate(Boolean.True as Entity, (all, member) => all & body.Substitute(variable, member)), + Existsf(var variable, FiniteSet over, var body) when over.Count <= LargestExpanded + => over.Aggregate(Boolean.False as Entity, (any, member) => any | body.Substitute(variable, member)), + ExistsUniquef(var variable, FiniteSet over, var body) when over.Count <= LargestExpanded + => ExactlyOne(over.Select(member => body.Substitute(variable, member)).ToList()), + _ => node + }; + + // The number of distinct values among the members: each counts where it equals none before it, and the + // count has no value where an equality has none. + private static Entity Cardinality(System.Collections.Generic.List members) + { + Entity count = Number.Integer.Zero; + for (var i = 0; i < members.Count; i++) + { + Entity unseen = Boolean.True; + for (var j = 0; j < i; j++) + unseen &= !members[i].Equalizes(members[j]); + count += new Iversonf(unseen); + } + return count; + } + + // Exactly one of the statements holds, by Kleene's connectives. + private static Entity ExactlyOne(System.Collections.Generic.List statements) + { + Entity any = Boolean.False; + for (var i = 0; i < statements.Count; i++) + { + var alone = statements[i]; + for (var j = 0; j < statements.Count; j++) + if (j != i) + alone &= !statements[j]; + any |= alone; + } + return any; + } + private static Entity? Statement(Entity element, Entity set) => set switch { Unionf(var left, var right) => Statement(element, left) is { } inLeft && Statement(element, right) is { } inRight ? inLeft | inRight : null, diff --git a/Sources/Tests/UnitTests/Common/FiniteSetStatementCompilationTest.cs b/Sources/Tests/UnitTests/Common/FiniteSetStatementCompilationTest.cs new file mode 100644 index 000000000..7a0efd953 --- /dev/null +++ b/Sources/Tests/UnitTests/Common/FiniteSetStatementCompilationTest.cs @@ -0,0 +1,115 @@ +// +// 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 System.Numerics; +using AngouriMath; +using AngouriMath.Core.Exceptions; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Common +{ + /// + /// A quantifier, a subset and a cardinality over a finite set compile, in FastExpression and in the LINQ compiler, to + /// what evaluation gives: a quantifier as the connective of its body at each member, a subset as the memberships of + /// its members, and a cardinality as the number of distinct values among them. Each was refused, and over any other + /// set still is. + /// #2195 + /// + [Trait("Area", "Common")] + public sealed class FiniteSetStatementCompilationTest + { + // Not at NaN: see AtNaNTheValueIsUndecidedOrTheVacuousTruth. + private static readonly string[] points = { "-1", "0", "1/2", "1", "2", "5/2", "3", "4", "i", "1 + i", "+oo", "-oo" }; + + private static Complex Numeric(string value) => ((Entity.Number.Complex)value.ToEntity().Evaled).ToNumerics(); + + private static Entity At(string expression, string point) => expression.ToEntity().Substitute("x", point); + + private static bool Same(Complex expected, Complex actual) + => double.IsNaN(expected.Real) || double.IsNaN(expected.Imaginary) + ? double.IsNaN(actual.Real) || double.IsNaN(actual.Imaginary) + : expected == actual; + + [Theory] + [InlineData("forall t in { 1, 2, 3 } : t < x")] + [InlineData("exists t in { 1, 2, 3 } : t = x")] + [InlineData("exists! t in { 1, 2, 3 } : t > x")] + [InlineData("forall t in { 1, 2 } : exists s in { 2, 3 } : s > t + x")] + [InlineData("forall t in { } : t = x")] + [InlineData("exists t in { } : t = x")] + [InlineData("{ x } subset [0; 3]")] + [InlineData("{ x, 2 } subset ZZ")] + [InlineData("{ } subset { x }")] + public void AStatementOverAFiniteSetIsWhatEvaluationSays(string statement) + { + var fast = statement.ToEntity().Compile("x"); + var linq = statement.ToEntity().Compile("x"); + var compared = 0; + foreach (var a in points) + { + var evaluated = At(statement, a).Evaled; + if (evaluated is not Entity.Boolean && !evaluated.IsNaN) + continue; + bool? expected = evaluated is Entity.Boolean truth ? (bool)truth : null; + var x = Numeric(a); + var value = fast.Call(x); + bool? fastTruth = value == 1 ? true : value == 0 ? false : null; + Assert.True(expected == fastTruth, $"{statement} at {a}: {expected?.ToString() ?? "none"} evaluated, {value} by FastExpression"); + Assert.True(expected == linq(x), $"{statement} at {a}: {expected?.ToString() ?? "none"} evaluated, {linq(x)?.ToString() ?? "none"} by LINQ"); + compared++; + } + Assert.True(compared >= points.Length / 2, $"only {compared} of {statement} decided"); + } + + [Theory] + [InlineData("card({ 1, x })")] + [InlineData("card({ 1, 2, x, x^2 })")] + [InlineData("card({ })")] + public void ACardinalityIsWhatEvaluationSays(string expression) + { + var fast = expression.ToEntity().Compile("x"); + var linq = expression.ToEntity().Compile("x"); + var compared = 0; + foreach (var a in points) + { + if (At(expression, a).Evaled is not Entity.Number.Complex evaluated) + continue; + var expected = evaluated.ToNumerics(); + var x = Numeric(a); + Assert.True(Same(expected, fast.Call(x)), $"{expression} at {a}: {expected} evaluated, {fast.Call(x)} by FastExpression"); + Assert.True(Same(expected, linq(x)), $"{expression} at {a}: {expected} evaluated, {linq(x)} by LINQ"); + compared++; + } + Assert.True(compared >= points.Length / 2, $"only {compared} of {expression} evaluated"); + } + + /// + /// At NaN the compiled value is undecided, or the vacuous truth of a quantifier over the empty set, where + /// evaluation differs: a finite set drops a member whose value is NaN, so { NaN } is { } and + /// card({ 1, NaN }) is 1, and a NaN anywhere in a quantifier's body makes the quantifier NaN. + /// + [Theory] + [InlineData("{ x } subset [0; 3]", double.NaN)] + [InlineData("card({ 1, x })", double.NaN)] + [InlineData("forall t in { } : t = x", 1)] + [InlineData("exists t in { } : t = x", 0)] + public void AtNaNTheValueIsUndecidedOrTheVacuousTruth(string expression, double expected) + { + var value = expression.ToEntity().Compile("x").Call(double.NaN); + Assert.True(double.IsNaN(expected) ? double.IsNaN(value.Real) : value == expected, $"{expression} at NaN: {value}"); + } + + [Theory] + [InlineData("forall t in [0; 1] : t < x")] + [InlineData("exists t in ZZ : t = x")] + [InlineData("{ x } subset QQ")] + [InlineData("card([0; x])")] + public void OverAnyOtherSetItIsRefused(string expression) + => Assert.Throws(() => expression.ToEntity().Compile("x")); + } +}