Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions BREAKING-CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,8 @@ read first.
| | the same on `x + x`, and `x + x * y` | `x + x`, `x * y + x` — left as written | `2 * x`, `(1 + y) * x` |
| **Silent** | `RewriteRules.Common.Rules[i].Growth`, for sixteen rules | `Unknown` | `Collects` for fourteen, `Rearranges` and `Expands` for the reciprocal-factor pair |
| **Silent** | what `RewriteRuleGrowth.Collects` promises | fewer nodes for every input | never more, and fewer for some — every rule that was `Collects` still is |
| | `Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(2 / x) ^ 3 * x")`, and its like with a power of the denominator | `(2 * 1 / x) ^ 3 * x` — left as written | `8 * x ^ (-2)`; `(2 / x) ^ 3 * x ^ 2` is `8 * 1 / x` |
| **Silent** | `RewriteRules.Power.Rules[i].Growth` for nine rules, and `Factorization`'s for four | `Unknown` | `Collects` |

### A cancelled quotient says its operand is defined, not only non-zero

Expand Down Expand Up @@ -900,6 +902,30 @@ and answers exactly as before on every input below.
| `RewriteRules.All` by growth | 97 / 45 / 30 / 152 | 111 / 46 / 31 / 136 |
| what `RewriteRuleGrowth.Collects` promises | fewer nodes for every input | never more, and fewer for some |

### `Power` and `Factorization` declare the rest of the collecting family

The entry above named the relatives of the `1 − |a|` shape in `Power` and `Factorization` as next.
Nine rules of `Power` — `a ^ n * a`, `a / a ^ n`, `a ^ n / a`, `a ^ n * (a * rest)`,
`(c / a) ^ d * a`, `(c / a) ^ d * a ^ e`, `a / b / b`, `a / b ^ n / b`, `a / b / b ^ n` — and four of
`Factorization` — `k + k * q`, `k + k`, `k - k * q`, `k * q - k` — declare `Collects`, each on its
own count; three more of `Power` stay `Unknown` with the reason written beside the rule. The safe
ceiling admits 170 of 324 rules where it admitted 157.

On ordinary input little moves, and for a measured reason: `x ^ 2 * x` reaches `x ^ (2 + 1)` over
the graph, which is no smaller at a leaf, and no safe rule folds the exponent, so the input is kept;
and `Factorization`'s four have twins in `Common` that were declared in the entry above, so
`a + a * b` was already `(1 + b) * a`. What does move is the power of a reciprocal beside its own
denominator, whose exponents fold as the replacement is built.

| | Was | Is |
|---|---|---|
| `Transformation.CanonicalizationOverGraph(budget).ApplyOrKeep("(2 / x) ^ 3 * x")` | `(2 * 1 / x) ^ 3 * x` — left as written | `8 * x ^ (-2)` |
| the same on `(2 / x) ^ 3 * x ^ 2` | `(2 * 1 / x) ^ 3 * x ^ 2` | `8 * 1 / x` |
| the same on `x ^ 2 * x`, `x / x ^ 2`, `x ^ 2 / x`, `x / y / y`, `a + a * b`, `a + a` | `x ^ 2 * x`, `1 / x ^ 2 * x`, `1 / x * x ^ 2`, `(1 / y) ^ 2 * x`, `(1 + b) * a`, `2 * a` | the same |
| `RewriteRules.Power.Rules` by growth — collects / rearranges / expands / unknown | 13 / 6 / 1 / 13 | 22 / 6 / 1 / 4 |
| `RewriteRules.Factorization.Rules` by growth | 4 / 0 / 2 / 5 | 8 / 0 / 2 / 1 |
| `RewriteRules.All` by growth | 111 / 46 / 31 / 136 | 124 / 46 / 31 / 123 |

## 2.4.0 — since 2.3.0

Released 2026-08-28. These entries sat under “Unreleased” while 2.4.0 was tagged and
Expand Down
73 changes: 60 additions & 13 deletions Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1450,15 +1450,21 @@ is var (divided, remainder)
MatchPattern.Commutative<Mulf>(MatchPattern.Any("k"), MatchPattern.Any("q"))),
bound => bound["k"] * (1 + bound["q"]),
Soundness.Sound,
description: "k + k*q = k*(1 + q)"),
description: "k + k*q = k*(1 + q)",
// The shared term is matched twice and written once, and the 1 is one node more:
// the delta is 1 - |k|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

// k + k -> 2k
new MatchedRule(
"a-term-added-to-itself-doubles",
MatchPattern.Node<Sumf>(MatchPattern.Any("k"), MatchPattern.Any("k")),
bound => 2 * bound["k"],
Soundness.Sound,
description: "k + k = 2k"),
description: "k + k = 2k",
// The term is matched twice and written once, and the 2 is one node more: the
// delta is 1 - |k|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

// k*p - k*q -> k*(p - q). The outer node is a difference and stays one.
new MatchedRule(
Expand All @@ -1480,7 +1486,10 @@ is var (divided, remainder)
MatchPattern.Commutative<Mulf>(MatchPattern.Any("k"), MatchPattern.Any("q"))),
bound => bound["k"] * (1 - bound["q"]),
Soundness.Sound,
description: "k - k*q = k*(1 - q)"),
description: "k - k*q = k*(1 - q)",
// The shared term is matched twice and written once, and the 1 is one node more:
// the delta is 1 - |k|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

// k*q - k -> k*(q - 1)
new MatchedRule(
Expand All @@ -1490,7 +1499,10 @@ is var (divided, remainder)
MatchPattern.Any("k")),
bound => bound["k"] * (bound["q"] - 1),
Soundness.Sound,
description: "k*q - k = k*(q - 1)"),
description: "k*q - k = k*(q - 1)",
// The shared term is matched twice and written once, and the 1 is one node more:
// the delta is 1 - |k|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

// k - k -> 0
new MatchedRule(
Expand Down Expand Up @@ -2767,7 +2779,10 @@ is var (divided, remainder)
MatchPattern.Any("a")),
bound => new Powf(bound["a"], bound["n"] + 1),
Soundness.SoundUnderAssumptions,
description: "a ^ n * a = a ^ (n + 1)"),
description: "a ^ n * a = a ^ (n + 1)",
// The base is matched twice and written once, and the 1 added to the exponent is
// one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"two-powers-of-one-base-multiply-by-adding-exponents",
Expand Down Expand Up @@ -2900,7 +2915,11 @@ is var (divided, remainder)
MatchPattern.Node<Powf>(MatchPattern.Any("a"), MatchPattern.Any("n"))),
bound => new Powf(bound["a"], 1 - bound["n"]),
Soundness.SoundUnderAssumptions,
description: "a / a ^ n = a ^ (1 - n)"),
description: "a / a ^ n = a ^ (1 - n)",
// The base is matched twice and written once, and the 1 the exponent is taken
// from is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink
// beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"a-power-over-its-own-base-lowers-the-exponent",
Expand All @@ -2909,7 +2928,10 @@ is var (divided, remainder)
MatchPattern.Any("a")),
bound => new Powf(bound["a"], bound["n"] - 1),
Soundness.SoundUnderAssumptions,
description: "a ^ n / a = a ^ (n - 1)"),
description: "a ^ n / a = a ^ (n - 1)",
// The base is matched twice and written once, and the 1 taken from the exponent
// is one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"a-number-raised-to-a-logarithm-of-itself-is-the-antilogarithm",
Expand Down Expand Up @@ -2957,7 +2979,10 @@ is var (divided, remainder)
MatchPattern.Commutative<Mulf>(MatchPattern.Any("a"), MatchPattern.Any("rest"))),
bound => new Powf(bound["a"], bound["n"] + 1) * bound["rest"],
Soundness.SoundUnderAssumptions,
description: "a ^ n * (a * rest) = a ^ (n + 1) * rest"),
description: "a ^ n * (a * rest) = a ^ (n + 1) * rest",
// The base is matched twice and written once, and the 1 added to the exponent is
// one node more: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

// Taking a factor out from under a root needs that factor positive, or the root to be
// a whole power. https://github.com/asc-community/AngouriMath/issues/752
Expand Down Expand Up @@ -3001,7 +3026,11 @@ is var (divided, remainder)
bound => new Powf(bound["c"], bound["d"])
* new Powf(bound["a"], 1 - (Number)bound["d"]),
Soundness.SoundUnderAssumptions,
description: "(c / a) ^ d * a = c ^ d * a ^ (1 - d), for numeric c and d"),
description: "(c / a) ^ d * a = c ^ d * a ^ (1 - d), for numeric c and d",
// The two numbers are leaves and 1 - d folds to one; the base is matched twice
// and written once, and the second power is one node more than the quotient it
// replaces: the delta is 1 - |a|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"a-power-of-a-numeric-reciprocal-times-a-power-of-its-own-denominator-subtracts-the-exponents",
Expand All @@ -3013,7 +3042,10 @@ is var (divided, remainder)
bound => new Powf(bound["c"], bound["d"])
* new Powf(bound["a"], (Number)bound["e"] - (Number)bound["d"]),
Soundness.SoundUnderAssumptions,
description: "(c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), for numeric c, d and e"),
description: "(c / a) ^ d * a ^ e = c ^ d * a ^ (e - d), for numeric c, d and e",
// The three numbers are leaves and e - d folds to one; the base is matched twice
// and written once, and the quotient goes: the delta is -1 - |a|, at most -2.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"dividing-twice-by-one-thing-squares-it",
Expand All @@ -3022,7 +3054,10 @@ is var (divided, remainder)
MatchPattern.Any("b")),
bound => bound["a"] / new Powf(bound["b"], 2),
Soundness.SoundUnderAssumptions,
description: "a / b / b = a / b ^ 2"),
description: "a / b / b = a / b ^ 2",
// The divisor is matched twice and written once, and the exponent is one node
// more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"dividing-by-a-power-and-then-by-its-base-raises-the-exponent",
Expand All @@ -3033,7 +3068,10 @@ is var (divided, remainder)
MatchPattern.Any("b")),
bound => bound["a"] / new Powf(bound["b"], bound["n"] + 1),
Soundness.SoundUnderAssumptions,
description: "a / b ^ n / b = a / b ^ (n + 1)"),
description: "a / b ^ n / b = a / b ^ (n + 1)",
// The divisor is matched twice and written once, and the 1 added to the exponent
// is one node more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"dividing-by-a-thing-and-then-by-a-power-of-it-raises-the-exponent",
Expand All @@ -3042,7 +3080,10 @@ is var (divided, remainder)
MatchPattern.Node<Powf>(MatchPattern.Any("b"), MatchPattern.Any("n"))),
bound => bound["a"] / new Powf(bound["b"], bound["n"] + 1),
Soundness.SoundUnderAssumptions,
description: "a / b / b ^ n = a / b ^ (n + 1)"),
description: "a / b / b ^ n = a / b ^ (n + 1)",
// The divisor is matched twice and written once, and the 1 added to the exponent
// is one node more: the delta is 1 - |b|, nothing at a leaf and a shrink beyond it.
growth: RewriteRuleGrowth.Collects),

new MatchedRule(
"dividing-by-two-powers-of-one-base-adds-the-exponents",
Expand Down Expand Up @@ -3092,6 +3133,8 @@ is var (divided, remainder)
MatchPattern.Node<Logf>(MatchPattern.Any("a"), MatchPattern.Any("a")),
(node, bound) => new Providedf(1, ((Logf)node).DomainCondition),
Soundness.SoundUnderAssumptions,
// Left Unknown: the condition attached is the node's own domain condition, whose
// size nothing here bounds.
description: "log(a, a) = 1, where log(a, a) is defined"),

// ln(1/b) = -ln(b) is false on the negative reals: at b = -0.63 the two differ by the
Expand Down Expand Up @@ -3174,6 +3217,8 @@ is var (divided, remainder)
Soundness.Sound,
when: bound => Functions.Patterns.ReduceRadical(
(Integer)bound["radicand"], (Rational)bound["power"]) is not null,
// Left Unknown: the helper answers a whole times a root, two nodes more than the
// pattern, or a whole alone, two fewer.
description: "sqrt(8) = 2 * sqrt(2), and its like for a positive whole radicand"),

// The rule above takes a whole power out from under one root; this takes a root out
Expand All @@ -3192,6 +3237,8 @@ is var (divided, remainder)
bound => Functions.Patterns.DenestRadical(bound["radicand"])!,
Soundness.Sound,
when: bound => Functions.Patterns.DenestRadical(bound["radicand"]) is not null,
// Left Unknown: the helper computes the answer, and the radicands it denests take
// more shapes than one count covers.
description: "sqrt(5 + 2*sqrt(6)) = sqrt(2) + sqrt(3)"));

/// <summary>
Expand Down
4 changes: 2 additions & 2 deletions Sources/AngouriMath/Core/Transformations/Saturation.cs
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@ internal static class Saturation
/// ceiling should refuse — it means the rule's growth was not judged, because its
/// replacement is code rather than a written pattern, so admitting it accepts a rewrite
/// nobody measured. But it is where the rules are: of the 324 rules in
/// <see cref="MatchedRules"/>, <b>111 collect, 46 rearrange, 31 expand and 136 are
/// unjudged</b>. A ceiling that refuses the fourth value still refuses 42% of the library,
/// <see cref="MatchedRules"/>, <b>124 collect, 46 rearrange, 31 expand and 123 are
/// unjudged</b>. A ceiling that refuses the fourth value still refuses 38% of the library,
/// and what is left could not do much when this was written — over six expression pairs
/// equal only through a larger intermediate form, the
/// <see cref="RewriteRuleGrowth.Rearranges"/> ceiling proved two, and
Expand Down
9 changes: 5 additions & 4 deletions Sources/AngouriMath/Docs/Contributing/WritingARule.md
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,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 — **136** rules sit at `Unknown` — but declare it where you can justify it:
honest default — **123** 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,
Expand Down Expand Up @@ -181,9 +181,10 @@ corpus, and each is false:
Two more used to be listed here and are not. The repeated hole that pays a literal to be gathered —
`a * (a * b) = a ^ 2 * b`, `k + k = 2 * k` and their relatives, every one `1 - |a|` — was
undeclarable only while `Collects` was read as "always fewer"; it is the commonest collecting shape
there is, and `Collects` promises never larger. `Common`'s thirteen are declared, with the count in
each one's comment; the relatives in `Power` and `Factorization` — `a ^ n * a`, `a / b / b` and
theirs — are the next to declare, each on its own count. And the reciprocal-factor rules were said
there is, and `Collects` promises never larger. `Common`'s thirteen, `Power`'s eight and
`Factorization`'s four are declared, with the count in each one's comment — and the count is worth
doing, since `Power`'s ninth relative, `(c / a) ^ d * a ^ e`, turned out to be `-1 - |a|` outright
rather than one of the family. And the reciprocal-factor rules were said
to admit two spellings of one thing; `IsWholeReciprocal` is `entity is Rational(...)`, so it admits
the literal only, and the pair is exactly `Rearranges` and exactly `Expands`.

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ public void NoWrittenPatternIntroducesACondition()
/// before the graph is wired into anything.
/// </summary>
/// <remarks>
/// <c>SafeRules</c> is <c>RulesUpTo(Rearranges)</c>, 157 of 324 rules. The 136 sitting at
/// <c>SafeRules</c> is <c>RulesUpTo(Rearranges)</c>, 170 of 324 rules. The 123 sitting at
/// <c>Unknown</c> are excluded by design, since their growth was never judged — so the
/// ceiling that is safe to run finds little, and the ceiling that finds things admits
/// rewrites nobody measured. That trade is the open part of tier 2, and this pins where it
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -89,15 +89,15 @@ public void ReplacementAPatternOrCode()
"how many rules have a pattern on both sides");
Stated(33, rules.Count(rule => rule.Reversed is not null),
"how many two-sided rules have a direction");
Stated(136, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Unknown),
Stated(123, 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
// the figures it quoted had gone stale by a factor of four -- "26 collect, 17
// rearrange, 9 expand and 270 unjudged", measured before the growth declarations
// went in. The argument survived; the arithmetic did not. A number a remark reasons
// from belongs somewhere that fails when it moves.
Stated(111, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects),
Stated(124, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Collects),
"how many rules are declared Collects");
Stated(46, rules.Count(rule => rule.Growth is RewriteRuleGrowth.Rearranges),
"how many rules are declared Rearranges");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,12 @@ public sealed class RuleGrowthAgreesWithTheCorpusTest
// a sum or a difference of itself -- and the sign-times-absolute-value cancellation.
"x + x * y", "x + (x + y)", "x + (x - y)", "x - (y - x)", "(y - x) - x",
"sgn(x) * (y * x) / abs(x)",

// A power beside its own base, on either side of a product or a quotient, and a
// divisor repeated -- the collecting shapes of `Power` that the arithmetic grammar
// builds only with a power of a leaf.
"x ^ 2 * x", "x / x ^ 2", "x ^ 2 / x", "(2 / x) ^ 3 * x", "(2 / x) ^ 3 * x ^ 2",
"x / y / y", "x / y ^ 2 / y",
};

private static List<Entity> Corpus()
Expand Down
Loading