A quantifier, a subset and a cardinality over a finite set compile

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<double, bool>("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

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
 

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<Entity> 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<Entity> 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,

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
+{
+    /// <summary>
+    /// 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.
+    /// <a href="https://github.com/asc-community/AngouriMath/issues/2195">#2195</a>
+    /// </summary>
+    [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<Complex, bool?>("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<Complex, Complex>("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");
+        }
+
+        /// <summary>
+        /// 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 <c>{ NaN }</c> is <c>{ }</c> and
+        /// <c>card({ 1, NaN })</c> is 1, and a NaN anywhere in a quantifier's body makes the quantifier NaN.
+        /// </summary>
+        [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<UncompilableNodeException>(() => expression.ToEntity().Compile("x"));
+    }
+}