diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 9384bf7c3..76933adfb 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -725,6 +725,25 @@ 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 }` | +### 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 +that collects (`binomial(n - 1, k) + binomial(n - 1, k - 1)` → `binomial(n, k)`, +`n binomial(n - 1, k - 1)` → `k binomial(n, k)`, `binomial(n, n - k)` → `binomial(n, k)`), so the +identities are `True` as statements of symbols; a sum written with `binomial(n, k)` is the binomial +theorem read backwards, as the factorial spelling already was (`sum(binomial(n, k) x^k y^(n - k), k, 0, n)` +is `(x + y)^n` for `n >= 0`). **Wrong answer fixed** in the alternating sum, in both spellings: +`sum(binomial(n, k) (-1)^k, k, 0, n)` is `1` at `n = 0` and `0` above, and the closed form `0^n` +carried a condition the piecewise read as no value, so the sum was `0` at `n = 0` +([#1409](https://github.com/asc-community/AngouriMath/issues/1409), the reference's §8.4). + +| Input | Was (2.5.0) | Now | +|---|---|---| +| `"binomial(n, k) = binomial(n, n - k)".ToEntity().Simplify()` | `UnhandledParseException` — `binomial` is new since, and was left as written when it arrived | `True` | +| `"binomial(n - 1, k) + binomial(n - 1, k - 1)".ToEntity().Simplify()` | `UnhandledParseException` | `binomial(n, k)` | +| `"sum(binomial(n, k), k, 0, n)".ToEntity().Evaled` | `UnhandledParseException` | `piecewise((2 ^ n) provided (n >= 0), 0 provided True)` | +| `"sum(n! / (k! (n - k)!) (-1)^k, k, 0, n)".ToEntity().Evaled` | `piecewise(0 provided True)` — wrong at `n = 0` | `piecewise(1 provided (n = 0), 0 provided True)` | + ### `binomial(n, k)` is a function **Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 45c516d2e..40ba68a05 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/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 + [Tests/UnitTests/Algebra/ConjunctionFilterTest.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/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index efac99430..383d1c03d 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -856,7 +856,43 @@ is var (divided, remainder) node, bound["x"], bound["y"], (Number)bound["a"], Integer.Create(0)), Soundness.SoundUnderAssumptions, // Left Unknown: as above, the answer's size is the offset's. - description: "(x + a)! * y = (x + a + 1)!, where y is the next term")); + description: "(x + a)! * y = (x + a + 1)!, where y is the next term"), + + // The binomial coefficient's three identities, each in the direction that collects: + // Pascal's rule, the chairperson identity and the symmetry. The reference's + // Props 8.4.1-8.4.3 (Sullivan and Mackey), which it proves by counting in two ways; + // here they are identities of the falling factorial for a whole lower index and of + // the gamma function elsewhere. https://github.com/asc-community/AngouriMath/issues/1409 + new MatchedRule( + "two-binomial-coefficients-of-one-upper-index-and-adjacent-lower-indices-add-by-pascals-rule", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("k")), + MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("j"))), + (node, bound) => Functions.Patterns.PascalsRule(node, bound["n"], bound["k"], bound["j"]), + Soundness.SoundUnderAssumptions, + // Left Unknown: which of the two lower indices is the larger is decided by the + // helper, and the answer is one coefficient where there were two. + description: "binomial(n, k) + binomial(n, k - 1) = binomial(n + 1, k)"), + + new MatchedRule( + "a-number-times-a-binomial-coefficient-of-the-number-less-one-is-the-chairperson-identity", + MatchPattern.Commutative( + MatchPattern.Any("n"), + MatchPattern.Node(MatchPattern.Any("m"), MatchPattern.Any("j"))), + (node, bound) => Functions.Patterns.ChairpersonsRule(node, bound["n"], bound["m"], bound["j"]), + Soundness.SoundUnderAssumptions, + // Left Unknown: fires only where the multiplier is one more than the upper + // index, and the answer is written with the lower index one more. + description: "n * binomial(n - 1, k - 1) = k * binomial(n, k)"), + + new MatchedRule( + "a-binomial-coefficient-whose-lower-index-is-the-complement-is-the-symmetric-one", + MatchPattern.Node(MatchPattern.Any("n"), MatchPattern.Any("d")), + (node, bound) => Functions.Patterns.SymmetricBinomial(node, bound["n"], bound["d"]), + Soundness.SoundUnderAssumptions, + // Left Unknown: fires only where the complement of the lower index is the + // smaller expression, and the answer is the coefficient with that. + description: "binomial(n, n - k) = binomial(n, k)")); /// /// , as data. diff --git a/Sources/AngouriMath/Docs/Contributing/WritingARule.md b/Sources/AngouriMath/Docs/Contributing/WritingARule.md index 2e3f61703..4b30172d2 100644 --- a/Sources/AngouriMath/Docs/Contributing/WritingARule.md +++ b/Sources/AngouriMath/Docs/Contributing/WritingARule.md @@ -18,7 +18,7 @@ effect". This is how to supply those seven things. ## Where a rule goes `Core/Transformations/Matching/MatchedRules.cs`, as a value in a `MatchedRuleSet`. **33** sets and -**332** rules live there today. +**335** rules live there today. The `switch` statements in `Functions/Simplification/Patterns` are the older form. **All thirty registered sets now run as data and describe what they run**; none executes its `switch` any more. @@ -64,7 +64,7 @@ in a name and putting the identity in brackets after it: 2. Tangent is sine over cosine (tan(a) = sin(a) / cos(a)), so tan(x) becomes sin(x) / cos(x). ``` -So the name has to be a clause that survives being read that way. **All 303 distinct rule names are, +So the name has to be a clause that survives being read that way. **All 306 distinct rule names are, and `StepAsASentenceTest` holds them to it** — a name with a capital, a bracket or an underscore fails that test rather than degrading the prose quietly. @@ -91,7 +91,7 @@ debugged for an afternoon. | `Left.ToString()` | `Divf(var a, Divf(var b, var c))` — how the matcher spells it | Write the identity with `=`, not `->`: it is an equality, and the arrow belongs to the direction the -rule happens to be applied in. **329** rules carry one today; a new rule should. +rule happens to be applied in. **332** rules carry one today; a new rule should. ## The pattern language @@ -137,7 +137,7 @@ A pattern replacement gets: - **an exact growth**, counted from the two patterns rather than declared. A code replacement gets neither, and its growth is `Unknown` unless you declare one. That is the -honest default — **123** rules sit at `Unknown` — but declare it where you can justify it: +honest default — **126** rules sit at `Unknown` — but declare it where you can justify it: ```csharp // The Chebyshev expansion of sin(n * a) is a sum of n terms where the pattern is one node, @@ -226,7 +226,7 @@ limit, against nothing for handing the node over. | `SoundUnderAssumptions` | holds given something the rule does not check | | `Heuristic` | usually right | -**186** of the 332 rules are `Sound` and **146** are conditional. Every one of the thirty registered +**186** of the 335 rules are `Sound` and **149** are conditional. Every one of the thirty registered *sets* declares `SoundUnderAssumptions`, because a set's tier is the **minimum** over its rules — so the set grain says nothing and the rule grain says everything. A derivation reports the rule's tier (`RewriteStep.Soundness`), which is why getting it right matters beyond the label. diff --git a/Sources/AngouriMath/Functions/Algebra/Polynomials/BinomialSum.cs b/Sources/AngouriMath/Functions/Algebra/Polynomials/BinomialSum.cs index 93b81458b..40333282d 100644 --- a/Sources/AngouriMath/Functions/Algebra/Polynomials/BinomialSum.cs +++ b/Sources/AngouriMath/Functions/Algebra/Polynomials/BinomialSum.cs @@ -70,6 +70,12 @@ internal static class BinomialSum } switch (factor) { + // The coefficient written as the node it is, binomial(N, k) or binomial(N, N - k): + // the three factorials at once. https://github.com/asc-community/AngouriMath/issues/1409 + case Binomialf(var top, var bottom) when top == upper && (bottom == index || IsUpperMinusIndex(bottom, upper, index)) + && !sawTop && !sawBottomK && !sawBottomRest: + sawTop = sawBottomK = sawBottomRest = true; + break; case Powf(Factorialf(var argument), var power) when power == Integer.MinusOne && argument == index && !sawBottomK: sawBottomK = true; break; @@ -98,7 +104,27 @@ internal static class BinomialSum Entity closed; if (angle is null) - closed = MathS.Pow((powerOfK ?? Integer.One) + (powerOfRest ?? Integer.One), upper); + { + var @base = ((powerOfK ?? Integer.One) + (powerOfRest ?? Integer.One)).InnerSimplified; + // A base that is zero, sum((-1)^k binomial(N, k)): 0^N is 1 at N = 0 and 0 for + // every N above it, and 0^N written as a power carries a condition that the + // piecewise below would read as "no value", making the sum 0 at N = 0 where it + // is 1. Said outright instead. + if (@base.Evaled is Complex { IsZero: true } || @base.Simplify().Evaled is Complex { IsZero: true }) + { + if (!sawTop) + return null; + Entity zeroPower = upper.Evaled is Integer whole + ? (whole.EInteger.IsZero ? Integer.One : Integer.Zero) + : MathS.Piecewise(new[] + { + new Providedf(Integer.One, new Equalsf(upper, Integer.Zero)), + new Providedf(Integer.Zero, Entity.Boolean.True), + }); + return (constant * zeroPower).InnerSimplified; + } + closed = MathS.Pow(@base, upper); + } else { var half = angle / 2; diff --git a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Factorial.cs b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Factorial.cs index 3f49077b6..9f4f3e6ae 100644 --- a/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Factorial.cs +++ b/Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Factorial.cs @@ -101,9 +101,57 @@ internal static Entity FactorizeFactorialMultiplications(Entity expr) GatherFactorial(expr, any1, any1a, const1, 0), Mulf(Factorialf(Sumf(Number const1, var any1)), var any1a) => GatherFactorial(expr, any1, any1a, const1, 0), + + // The binomial coefficient's three identities, in the direction that collects. + // https://github.com/asc-community/AngouriMath/issues/1409 + Sumf(Binomialf(var top1, var k), Binomialf(var top2, var j)) when top1 == top2 => PascalsRule(expr, top1, k, j), + Mulf(var n, Binomialf(var top, var j)) => ChairpersonsRule(expr, n, top, j), + Mulf(Binomialf(var top, var j), var n) => ChairpersonsRule(expr, n, top, j), + Binomialf(var top, var d) => SymmetricBinomial(expr, top, d), _ => expr }; + /// + /// binomial(a, k) + binomial(a, k - 1) is binomial(a + 1, k) -- Pascal's rule, + /// an identity of the falling factorial for every a and whole k, and of the + /// gamma function elsewhere -- read in either order of the two, with the lower index that + /// is one less found by simplifying the difference; where neither is. + /// + internal static Entity PascalsRule(Entity whole, Entity top, Entity k, Entity j) + { + if (PartialFractions.Bare((k - j).Simplify()) == Integer.One) + return new Binomialf((top + 1).InnerSimplified, k); + if (PartialFractions.Bare((j - k).Simplify()) == Integer.One) + return new Binomialf((top + 1).InnerSimplified, j); + return whole; + } + + /// + /// n * binomial(n - 1, k - 1) is k * binomial(n, k) -- the chairperson identity, + /// choosing the chair first or the committee first -- where the multiplier is one more + /// than the upper index; otherwise. + /// + internal static Entity ChairpersonsRule(Entity whole, Entity n, Entity top, Entity j) + { + if (n.ContainsNode(top) || top.ContainsNode(n) ? PartialFractions.Bare((n - top).Simplify()) != Integer.One : (n - top).InnerSimplified != Integer.One) + return whole; + var k = (j + 1).InnerSimplified; + return k * new Binomialf(n, k); + } + + /// + /// binomial(n, n - k) is binomial(n, k), taken where the complement is the + /// smaller expression: the symmetry of the coefficient, an identity of the gamma + /// function; where the lower index is already the smaller. + /// + internal static Entity SymmetricBinomial(Entity whole, Entity top, Entity d) + { + if (!d.ContainsNode(top) || top is Number) + return whole; + var complement = PartialFractions.Bare((top - d).Simplify()); + return complement.Complexity < d.Complexity ? new Binomialf(top, complement) : whole; + } + /// /// The factorial one term further on, where the term multiplying it is the next one — and /// where it is not. A static method for the same reason diff --git a/Sources/AngouriMath/Functions/Simplification/Simplificator.cs b/Sources/AngouriMath/Functions/Simplification/Simplificator.cs index 733b53cfa..6fe463a65 100644 --- a/Sources/AngouriMath/Functions/Simplification/Simplificator.cs +++ b/Sources/AngouriMath/Functions/Simplification/Simplificator.cs @@ -306,7 +306,9 @@ void __IterAddHistory(Entity expr) AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.InequalityEquality))); } - if (res.Nodes.Any(child => child is Factorialf)) + // A binomial coefficient is three factorials, and its identities live in the + // gathering set. https://github.com/asc-community/AngouriMath/issues/1409 + if (res.Nodes.Any(child => child is Factorialf or Binomialf)) { AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.ExpandFactorialDivisions))); AddHistory(res = Simplified(recording, res.Rewrite(RewriteRules.FactorizeFactorialMultiplications))); diff --git a/Sources/Tests/UnitTests/Core/BinomialIdentityTest.cs b/Sources/Tests/UnitTests/Core/BinomialIdentityTest.cs new file mode 100644 index 000000000..3331bf1a7 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/BinomialIdentityTest.cs @@ -0,0 +1,77 @@ +// +// 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 +{ + /// + /// The binomial coefficient's identities: Pascal's rule, the chairperson identity and the + /// symmetry as rewrite rules, and the binomial theorem read backwards for a sum written + /// with binomial(n, k). Item 7 of the reference's docket (Sullivan and Mackey, + /// §8.4: Props 8.4.1–8.4.4, Thm 8.4.8, Ex 8.4.9, §8.4.5 Try 3). + /// + /// + [Trait("Area", "Core")] + public sealed class BinomialIdentityTest + { + /// Props 8.4.1–8.4.3 as equalities of symbols, decided by rewriting one side into the other. + [Theory] + [InlineData("binomial(n, k) = binomial(n, n - k)")] + [InlineData("binomial(n, k) = binomial(n - 1, k) + binomial(n - 1, k - 1)")] + [InlineData("binomial(n + 1, k + 1) = binomial(n, k + 1) + binomial(n, k)")] + [InlineData("k * binomial(n, k) = n * binomial(n - 1, k - 1)")] + public void AnIdentityIsTrue(string identity) + => Assert.Equal(Boolean.True, identity.ToEntity().Simplify()); + + /// The rewrites themselves, each in the direction that collects. + [Theory] + [InlineData("binomial(n - 1, k) + binomial(n - 1, k - 1)", "binomial(n, k)")] + [InlineData("binomial(n, n - 2)", "binomial(n, 2)")] + [InlineData("binomial(n, n - k)", "binomial(n, k)")] + [InlineData("n * binomial(n - 1, k - 1)", "binomial(n, k) * k")] + [InlineData("binomial(7, 3) + binomial(7, 2)", "56")] + public void ARewriteCollects(string input, string expected) + => Assert.Equal(expected.ToEntity(), input.ToEntity().Simplify()); + + /// The symmetry fires only where the complement is the smaller expression: binomial(n, 2) stays. + [Fact] + public void TheSymmetryPrefersTheSmallerLowerIndex() + { + Assert.Equal("binomial(n, 2)".ToEntity(), "binomial(n, 2)".ToEntity().Simplify()); + Assert.Equal("binomial(n, k)".ToEntity(), "binomial(n, k)".ToEntity().Simplify()); + } + + /// Thm 8.4.8, Prop 8.4.4, §8.4.5 Try 3 and Ex 8.4.9: the sum written with the node, in closed form. + [Theory] + [InlineData("sum(binomial(n, k), k, 0, n)", "piecewise((2 ^ n) provided (n >= 0), 0 provided True)")] + [InlineData("sum(binomial(n, k) * 2^(n - k), k, 0, n)", "piecewise((3 ^ n) provided (n >= 0), 0 provided True)")] + [InlineData("sum(binomial(n, k) * x^k * y^(n - k), k, 0, n)", "piecewise(((x + y) ^ n) provided (n >= 0), 0 provided True)")] + [InlineData("sum(binomial(n, n - k) * x^k, k, 0, n)", "piecewise(((x + 1) ^ n) provided (n >= 0), 0 provided True)")] + [InlineData("sum(binomial(4, k) * 2^(4 - k), k, 0, 4)", "81")] + [InlineData("sum(binomial(10, k), k, 0, 10)", "1024")] + public void ABinomialSumIsTheTheoremReadBackwards(string sum, string expected) + => Assert.Equal(expected.ToEntity().Evaled, sum.ToEntity().Evaled); + + /// + /// Ex 8.4.9: the alternating sum is 0^n, which is 1 at n = 0 and + /// 0 above it. Written as the power it carried a condition the piecewise read as + /// no value, and the sum was 0 at n = 0 where it is 1 -- in the + /// factorial spelling too, which is fixed by the same arm. + /// + [Theory] + [InlineData("sum(binomial(n, k) * (-1)^k, k, 0, n)", "piecewise(1 provided (n = 0), 0 provided True)")] + [InlineData("sum(n! / (k! * (n - k)!) * (-1)^k, k, 0, n)", "piecewise(1 provided (n = 0), 0 provided True)")] + [InlineData("sum(binomial(0, k) * (-1)^k, k, 0, 0)", "1")] + [InlineData("sum(binomial(4, k) * (-1)^k, k, 0, 4)", "0")] + public void TheAlternatingSumIsOneAtZero(string sum, string expected) + => Assert.Equal(expected.ToEntity().Evaled, sum.ToEntity().Evaled); + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs b/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs index 34e73502c..7b241bbb3 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/AddressableRulesTest.cs @@ -299,7 +299,7 @@ public void TheRegistryIsAddressableAsFarAsItSaysItIs() // are thirty-three; NumericNeat's sixteen are eleven, six of them being three rules // written once per side a negative factor can sit on; and the two factorial sets are // eight arms each written as three. Every other repointed set is one arm for one rule. - Assert.Equal(329, withRules.Sum(set => set.Rules.Count)); + Assert.Equal(332, withRules.Sum(set => set.Rules.Count)); } /// diff --git a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs index 6a4e837e5..fe564b571 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ReversibleRuleTest.cs @@ -123,6 +123,7 @@ public void EveryDataRuleIsClassifiedAsWritten() Assert.Equal( new[] { + "a-binomial-coefficient-whose-lower-index-is-the-complement-is-the-symmetric-one: ReplacementIsCode", "a-chain-of-greaters-implies-its-own-ends: ReplacementIsCode", "a-chain-of-lesss-implies-its-own-ends: ReplacementIsCode", "a-common-factor-is-collected-out-of-a-whole-sum: ReplacementIsCode", @@ -224,6 +225,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "a-number-plus-a-variable-puts-the-variable-first: ReplacementIsCode", "a-number-raised-to-a-logarithm-of-itself-is-the-antilogarithm: ReplacementIsCode", "a-number-raised-to-a-multiple-of-a-logarithm-of-itself-is-a-power-of-the-antilogarithm: ReplacementIsCode", + "a-number-times-a-binomial-coefficient-of-the-number-less-one-is-the-chairperson-identity: ReplacementIsCode", "a-numeric-coefficient-is-gathered-over-a-surd: ReplacementIsCode", "a-numeric-factor-comes-out-of-a-power-of-a-product: ReplacementIsCode", "a-numeric-factor-floats-out-of-a-product-of-functions: ReplacementIsCode", @@ -377,6 +379,7 @@ public void EveryDataRuleIsClassifiedAsWritten() "the-two-truth-values-are-the-boolean-domain: ReplacementIsCode", "two-added-fractions-take-a-common-denominator: ReplacementIsCode", "two-arctangents-of-numbers-add-by-the-tangent-formula: ReplacementIsCode", + "two-binomial-coefficients-of-one-upper-index-and-adjacent-lower-indices-add-by-pascals-rule: ReplacementIsCode", "two-comparisons-of-one-pair-that-exclude-each-other-are-false: ReplacementIsCode", "two-comparisons-of-one-pair-that-leave-no-case-are-true: ReplacementIsCode", "two-functions-in-a-sum-come-together: ReplacementIsCode", diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs index c5c866dba..61f57eeae 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleAuthoringGuideTest.cs @@ -43,7 +43,7 @@ private static void Stated(int stated, int measured, string claim) public void WhereARuleGoes() { Stated(33, MatchedRules.All.Count, "the number of rule sets written as data"); - Stated(332, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); + Stated(335, MatchedRules.All.Sum(set => set.Rules.Count), "the number of rules written as data"); Stated(30, RewriteRules.All.Count, "the number of registered sets"); // Two families register under one name and run a data set under another -- // CommonDenominator over MatchedRules.CommonDenominator(level), CanonicalOrder over @@ -64,7 +64,7 @@ public void TheNameIsASentence() { var names = MatchedRules.All.SelectMany(set => set.Rules) .Select(rule => rule.Name).Distinct(StringComparer.Ordinal).ToList(); - Stated(303, names.Count, "the number of distinct rule names"); + Stated(306, names.Count, "the number of distinct rule names"); var words = names.Select(name => name.Split('-').Length).ToList(); Stated(4, words.Min(), "the shortest rule name in words"); @@ -73,7 +73,7 @@ public void TheNameIsASentence() [Fact] public void TheIdentityIsNotTheName() - => Stated(329, + => Stated(332, MatchedRules.All.SelectMany(set => set.Rules).Count(rule => rule.Description is not null), "how many rules carry an identity"); @@ -89,7 +89,7 @@ public void ReplacementAPatternOrCode() "how many rules have a pattern on both sides"); Stated(32, rules.Count(rule => rule.Reversed is not null), "how many two-sided rules have a direction"); - Stated(123, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), + Stated(126, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown), "how many rules sit at Unknown growth"); // The rest of the census, because `Saturation.RulesUpTo` argues from it in prose and @@ -134,7 +134,7 @@ public void SoundnessIsPerRule() var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); Stated(186, rules.Count(rule => rule.Soundness is Soundness.Sound), "how many rules are Sound"); - Stated(146, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), + Stated(149, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions), "how many rules are SoundUnderAssumptions"); Assert.All(RewriteRules.All, set => Assert.Equal(Soundness.SoundUnderAssumptions, set.Soundness)); diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs index 81800cba9..6f8c9c8a5 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs @@ -88,9 +88,9 @@ public void AddressableGrowthIsTheRulesOwnAnswer() public void SoundnessIsFinerPerRuleThanPerSet() { var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); - Assert.Equal(332, rules.Count); + Assert.Equal(335, rules.Count); Assert.Equal(186,rules.Count(rule => rule.Soundness is Soundness.Sound)); - Assert.Equal(146, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); + Assert.Equal(149, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); // And every set still reports the weakest of them, which is what makes the set grain // uninformative rather than wrong. @@ -174,7 +174,7 @@ public void EveryRuleOfARepointedSetCarriesItsIdentity() var repointed = RewriteRules.All .Where(set => set.Rules.Count > 0 && set.Rules.All(rule => rule.Soundness is not null)) .ToList(); - Assert.Equal(329, repointed.Sum(set => set.Rules.Count)); + Assert.Equal(332, repointed.Sum(set => set.Rules.Count)); Assert.All(repointed, set => Assert.All(set.Rules, rule => Assert.NotNull(rule.Description))); } diff --git a/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs index 3c7ec72b4..b413eeaf4 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs @@ -144,7 +144,7 @@ private static SortedSet Subsumptions() /// /// /// Over every rule rather than within a set, because the relation is about patterns and - /// nothing about it stops at a set boundary: 963 ordered pairs claim subsumption, + /// nothing about it stops at a set boundary: 969 ordered pairs claim subsumption, /// 502 of them (501 before the constant antilogarithm rule of #994 subsumed the symbolic one) are put to the test by the corpus containing something the narrower /// pattern matches, and none is contradicted across 85,153 nodes. All three counts /// are asserted — a corpus that stopped reaching these shapes would otherwise turn this @@ -205,7 +205,7 @@ public void SubsumptionIsNeverContradictedByMatching() if (put) witnessed++; } - Assert.Equal(963, claims.Count); + Assert.Equal(969, claims.Count); Assert.Equal(502, witnessed); // Asserted so the two figures in the remark above cannot go stale in silence: the // whole point of `witnessed` is that it is a coverage number, and it means nothing diff --git a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs index c191ad0e9..777ee381e 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/StepAsASentenceTest.cs @@ -59,7 +59,7 @@ public void EveryRuleWrittenAsDataIsNamedInProse() { var names = MatchedRules.All.SelectMany(set => set.Rules).Select(rule => rule.Name) .Distinct(StringComparer.Ordinal).ToList(); - Assert.Equal(303, names.Count); + Assert.Equal(306, names.Count); Assert.All(names, name => Assert.True(Explanation.IsProse(name), $"'{name}' is a rule name that does not read as a phrase in English"));