From ea2e6c0e2d87b120636088f35c281d40e2b624f0 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 6 Sep 2026 23:13:06 +0000 Subject: [PATCH] The growth ceiling is the scheduling policy, and the runaway is bounded to trig #1193 named the four rules behind sin(2x) + cos(2x) running away at the widest ceiling and left the decision open: withhold one direction of the inverse pair, or make the two Common coefficient rules confluent so the graph could absorb it. Measuring how broad the runaway is settles both, and the facts are pinned so neither branch can be re-proposed from the symptom. The coefficient rules are confluent on plain arithmetic. 2 * x * y, (1/2) * x and 2 * (x * y) / 3 saturate at the widest ceiling in a handful of nodes, with every trigonometric set present and with all five removed, and extract 2 * x * y, x / 2 and 2/3 * x * y. They were load-bearing in the runaway only because they supplied the respellings the trigonometric pair fed on; making them confluent is not a branch. The runaway is a family and it is bounded to the trigonometric sets. sin(2x), sin(x) cos(x), sin(3x) and sin(2x) cos(2x) all run away at the widest ceiling, cos(2x) does not, and with Trigonometric, ExpandMultipleAngle, ExpandTrigonometric, CollapseTrigonometricFunctions and NormalTrigonometricForm removed the exemplar saturates at seven nodes. And the safe ceiling already withholds the expanding direction. ExpandMultipleAngle's rules are declared Expands, so RulesUpTo(Rearranges) fires only the collecting one and every member of the family saturates there. That was inferred from the declarations when #1193 went in; RunawayBreadthTest asserts it now. Growth is the direction marker and the ceiling is the scheduling policy, mechanically, for every pair whose two directions are declared -- a pair whose expanding direction is unjudged is the one case it cannot protect, which is what declaring a growth for a rule is for. The RulesUpTo remark and InversePairTable.md say so. Four tests, 300 ms between them, bounded by the same 3,000-step ceiling as the ablation. Each failure message says which way the fact moved and what to do about it. Part of #746. Full suite 9578 passed, 0 failed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Core/Transformations/Saturation.cs | 10 ++ .../Docs/Contributing/InversePairTable.md | 12 ++ .../Transformations/RunawayBreadthTest.cs | 161 ++++++++++++++++++ 3 files changed, 183 insertions(+) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/RunawayBreadthTest.cs diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 2d47d69bc..19c32a060 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -65,6 +65,16 @@ internal static class Saturation /// classified may fire at all. Naming that as the widest setting makes it a request a /// caller has to make on purpose, which is the most this can honestly do about it. /// + /// + /// And the ceiling is the scheduling policy, not a stand-in for one. When both + /// directions of an inverse pair are declared, RulesUpTo(Rearranges) keeps the + /// collecting one and withholds the expanding one, mechanically, for every such pair. + /// sin(2x) and 2 sin x cos x run away at the widest ceiling and saturate at + /// the safe one because ExpandMultipleAngle declares + /// . Growth is the direction marker. A pair whose + /// expanding direction is unjudged is the one case this cannot protect, and that is what + /// declaring a growth for a rule is for. RunawayBreadthTest holds this. + /// /// internal static IReadOnlyList RulesUpTo(RewriteRuleGrowth widest) => MatchedRules.All diff --git a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md index dddbc91d2..bd9c62914 100644 --- a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md +++ b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md @@ -141,6 +141,18 @@ What this is and is not: held by `SaturationAblationTest` in both directions. It is also the measured answer to what #746 tier 2 called "a scheduling policy for `Expands`/`Unknown` rules": on this input the runaway is not a tier, it is one pair. + + And the pair is bounded. The two `Common` coefficient rules are confluent on plain arithmetic — + `2 * x * y`, `(1/2) * x` and `2 * (x * y) / 3` saturate in a handful of nodes at the widest + ceiling, with the trigonometric sets present and with all of them removed — so making them + confluent is not a branch. The runaway is the sine family (`sin(2x)`, `sin(x) cos(x)`, `sin(3x)`, + `sin(2x) cos(2x)`; not `cos(2x)`), and it does not exist without the trigonometric sets. + **The growth ceiling already withholds one direction of it.** `ExpandMultipleAngle`'s rules are + declared `Expands`, so `Saturation.SafeRules` — `RulesUpTo(Rearranges)` — fires only the + collecting direction, and every member of the family saturates there. Growth is the direction + marker and the ceiling is the scheduling policy, for every pair whose two directions are + declared; a pair whose expanding direction is unjudged is the one case it cannot protect. Held by + `RunawayBreadthTest`. - **It needs no reversibility mechanism at all**, which is the whole of what makes it available today: it is behaviour observed at the top of the pipeline, not a property computed about a rule. - **It answers the question equality saturation actually asks.** The consumer in the opening quote diff --git a/Sources/Tests/UnitTests/Core/Transformations/RunawayBreadthTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RunawayBreadthTest.cs new file mode 100644 index 000000000..78844c81c --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RunawayBreadthTest.cs @@ -0,0 +1,161 @@ +// +// 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; +using System.Collections.Generic; +using System.Linq; +using AngouriMath.Core; +using AngouriMath.Core.Budgets; +using AngouriMath.Core.Transformations; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// How broad the saturation runaway is, and where it is not. + /// names the four rules behind one input; this holds the facts that decide what to do about + /// them, so that a branch already measured dead cannot be re-proposed. + /// + /// + /// + /// Two branches were on the table for the inverse pair sin(2x) / 2 sin x cos x: + /// withhold one direction from saturation, or make the two Common coefficient rules + /// confluent so the graph could absorb the pair. The second assumed those rules were the + /// problem. They are not. On plain arithmetic — 2 * x * y, (1/2) * x, + /// 2 * (x * y) / 3 — the widest ceiling saturates in a handful of nodes, with every + /// trigonometric set present and with all of them removed. The coefficient rules were + /// load-bearing in the runaway only because they supplied the respellings the trigonometric + /// pair fed on. + /// + /// + /// The runaway is a family, and it is bounded to the trigonometric sets. Every sine + /// input reachable from a product loops at the widest ceiling — sin(2x), + /// sin(x) cos(x), sin(3x), sin(2x) cos(2x) — and cos(2x) does not. + /// With the five trigonometric sets removed, the exemplar sin(2x) + cos(2x) saturates + /// at seven nodes. + /// + /// + /// And the safe ceiling already withholds the expanding direction. + /// ExpandMultipleAngle's rules are declared , + /// and is RulesUpTo(Rearranges), so at that ceiling + /// only the collecting direction fires and every member of the family saturates. That is the + /// measured answer to #746 + /// tier 2's "scheduling policy" item: the growth ceiling is the policy. When both + /// directions of an inverse pair are declared, it keeps the collecting one and withholds the + /// expanding one, mechanically, for every such pair — and it can only protect pairs whose + /// directions are declared, which is what declaring growth for a code-built rule is for. + /// + /// + [Trait("Area", "Core")] + public sealed class RunawayBreadthTest + { + private static readonly WorkBudget Quick = new() { Steps = 3_000, Time = TimeSpan.FromSeconds(1) }; + + private static readonly string[] TrigonometricSets = + { + "Trigonometric", "ExpandMultipleAngle", "ExpandTrigonometric", + "CollapseTrigonometricFunctions", "NormalTrigonometricForm", + }; + + private static IReadOnlyList Rules(RewriteRuleGrowth ceiling, Func keep) => + MatchedRules.All + .Where(keep) + .SelectMany(set => set.Rules) + .Where(rule => rule.Soundness is Soundness.Sound or Soundness.SoundUnderAssumptions) + .Where(rule => rule.Growth <= ceiling) + .ToList(); + + private static (bool Saturated, int Nodes, string Extracted) Saturate(string source, IReadOnlyList rules) + { + var graph = new EGraph(); + var root = graph.AddEntity(source.ToEntity()); + var ledger = BudgetLedger.For(nameof(RunawayBreadthTest), Quick); + var saturated = Saturation.Run(graph, rules, ledger, node => node.Complexity); + return (saturated, graph.NodeCount, graph.Extract(root, node => node.Complexity)?.Stringize() ?? "(nothing)"); + } + + private static readonly (string Input, string Extracts)[] PlainArithmetic = + { + ("2 * x * y", "2 * x * y"), + ("(1/2) * x", "x / 2"), + ("2 * (x * y) / 3", "2/3 * x * y"), + }; + + [Fact] + public void TheCoefficientRulesAreConfluentOnPlainArithmetic() + { + var failures = new List(); + foreach (var (input, extracts) in PlainArithmetic) + foreach (var (label, rules) in new[] + { + ("all sets", Rules(RewriteRuleGrowth.Unknown, _ => true)), + ("no trigonometric sets", Rules(RewriteRuleGrowth.Unknown, set => !TrigonometricSets.Contains(set.Name))), + }) + { + var (saturated, nodes, extracted) = Saturate(input, rules); + if (!saturated || extracted != extracts) + failures.Add($"{input} with {label}: saturated={saturated} nodes={nodes} => {extracted}"); + } + + Assert.True(failures.Count == 0, + "the coefficient rules no longer settle on plain arithmetic — making them confluent " + + "stopped being a phantom branch:\n" + string.Join("\n", failures)); + } + + private static readonly string[] Family = + { "sin(2 * x)", "sin(x) * cos(x)", "sin(3 * x)", "sin(2 * x) * cos(2 * x)" }; + + [Fact] + public void TheWidestCeilingRunsAwayOnTheWholeFamilyAndNotOnCosine() + { + var all = Rules(RewriteRuleGrowth.Unknown, _ => true); + var settled = Family.Where(input => Saturate(input, all).Saturated).ToList(); + Assert.True(settled.Count == 0, + "these members of the family saturate at the widest ceiling now; delete them from " + + "the list rather than leave them: " + string.Join(", ", settled)); + + var cosine = Saturate("cos(2 * x)", all); + Assert.True(cosine.Saturated, + $"cos(2 * x) runs away at the widest ceiling now ({cosine.Nodes} nodes); the family " + + "has grown a cosine side and the remark above is wrong about the asymmetry"); + } + + [Fact] + public void TheFamilyIsBoundedToTheTrigonometricSets() + { + var noTrig = Rules(RewriteRuleGrowth.Unknown, set => !TrigonometricSets.Contains(set.Name)); + var (saturated, nodes, _) = Saturate("sin(2 * x) + cos(2 * x)", noTrig); + Assert.True(saturated, + $"the exemplar runs away ({nodes} nodes) with every trigonometric set removed, so the " + + "runaway is no longer bounded to them"); + } + + /// + /// The claim that makes the ceiling the policy. Asserted, not inferred: at + /// the expanding direction is withheld and every + /// member of the family must settle. + /// + [Fact] + public void TheSafeCeilingSaturatesTheWholeFamily() + { + var safe = Rules(RewriteRuleGrowth.Rearranges, _ => true); + var runsAway = new List(); + foreach (var input in Family.Append("sin(2 * x) + cos(2 * x)")) + { + var (saturated, nodes, extracted) = Saturate(input, safe); + if (!saturated) runsAway.Add($"{input}: {nodes} nodes => {extracted}"); + } + + Assert.True(runsAway.Count == 0, + "these run away at the safe ceiling, so the growth ceiling is not withholding the " + + "expanding direction and is not the policy the remark says it is:\n" + + string.Join("\n", runsAway)); + } + } +}