From fcda989e63dc2ade55f2db4fa9c39e31351c8cc1 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Fri, 30 Oct 2026 09:38:00 +0000 Subject: [PATCH] A quantifier, a subset and a cardinality over a finite set compile forall, exists, exists!, subset and card were refused by both compilers. Over a finite set the set is known when the expression is compiled, so each is a statement or a number about its members. CompiledMembership writes each one out before either compiler sees it: - forall and exists become the conjunction and the disjunction of the body at each member. Over the empty set they are True and False. - exists! becomes exactly one of them, as the disjunction over i of P_i and not P_j for every j other than i, by Kleene's connectives. - A finite set is a subset where each member is a member of the other set, by the membership rewrite of #2223. - card is the number of distinct values among the members. Each member counts, as an Iverson bracket, where it equals none before it, so the count has no value where an equality has none. Each is capped at 64 members, past which the cardinality and exists! grow with the square of the count, and is left as written there. Over any other set it is left as written too, and neither compiler compiles it. At a NaN argument the compiled value is undecided, or the vacuous truth of a quantifier over the empty set. Evaluation differs there for two reasons. 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. Undecided answers nothing wrong, and the vacuous truth is the mathematics, so the difference is pinned by its own test rather than mirrored. FiniteSetStatementCompilationTest compares both compilers with evaluation at 12 points, among them i, 1 + i and the infinities: - nine statements, among them nested quantifiers and quantifiers over the empty set; - three cardinalities; - the NaN cases; - four refusals over sets that are not finite. Part of #2195. Co-Authored-By: Claude Opus 5.5 (1M context) --- BREAKING-CHANGES.md | 20 +++ Sources/.editorconfig | 3 + .../Compilation/CompiledMembership.cs | 58 ++++++++- .../FiniteSetStatementCompilationTest.cs | 115 ++++++++++++++++++ 4 files changed, 194 insertions(+), 2 deletions(-) create mode 100644 Sources/Tests/UnitTests/Common/FiniteSetStatementCompilationTest.cs 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")); + } +}