From f2043ac2d0a8bc4e1df3b528704080d8fcb3bef9 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 6 Sep 2026 21:00:31 +0000 Subject: [PATCH] The saturation runaway is one inverse pair across two sets, not a tier #746 tier 2's remaining item was phrased as "a scheduling policy for Expands/Unknown rules", on the observation that sin(2x) + cos(2x) reaches 254 e-nodes at the widest ceiling without saturating -- and extracts the input unchanged, so the blow-up finds nothing. Ablating every set in turn says the unjudged rules are not the cause as a class: remove any one of Common, ExpandMultipleAngle or Trigonometric and it saturates at about twenty nodes; remove CollapseMultipleFractions and it gets worse, 618, because that set was a brake. Ablating the rules of those three sets one at a time names four. ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle sin(2x) -> 2 sin x cos x Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-... sin x cos x -> sin(2x) / 2 Common / a-numeric-factor-floats-out-of-a-product-of-functions the 2 goes out Common / a-reciprocal-rational-factor-is-a-division the 1/2 becomes / 2 The first two are an exact inverse pair. An e-graph is supposed to absorb one -- both directions land in a class and it stops -- and this one is not absorbed because its two forms differ by a coefficient the two Common rules rearrange non-confluently, so every pass makes a fresh spelling rather than a merge. That is a precise thing, and it is the first cross-set inverse pair anything here has measured. InversePairTable.md says the single-set observation "never meets" a pair split across two sets, and saturation meets it because it runs every set at once; the document records the pair now, and says so. Pinned in both directions by SaturationAblationTest: the runaway is a known non-saturation, each of the four rules is asserted load-bearing for it, and no other rule of the three sets is -- so fixing the pair deletes entries rather than leaving names that mean nothing, and a fifth rule joining the cycle fails. The load-bearing list checks each name still exists in the registry, so a rename cannot leave it asserting about nothing. What this does not do is fix the pair. Which direction to withhold from saturation -- or whether to make the coefficient rules confluent so the graph can absorb it -- is the decision the table is for, and it is a smaller one than the item it replaces. Part of #746. Full suite 9574 passed, 0 failed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Docs/Contributing/InversePairTable.md | 17 +- .../Transformations/SaturationAblationTest.cs | 152 ++++++++++++++++++ 2 files changed, 168 insertions(+), 1 deletion(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs diff --git a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md index 6f0e631c5..dddbc91d2 100644 --- a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md +++ b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md @@ -125,7 +125,22 @@ section arguing that behaviour is a better source than derivation. What this is and is not: - **It is a lower bound, and a cheap one.** A pair that never fires on the corpus is invisible to it, - and a pair split across two sets never meets. It cannot enumerate the table. + and — for the single-set observation above — a pair split across two sets never meets. It cannot + enumerate the table. + + *Saturation meets the cross-set case, because it runs every set at once.* The first pair found + that way is `ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle` against + `Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine` — `sin(2x)` to + `2 sin x cos x` and straight back to `sin(2x) / 2`. On `sin(2x) + cos(2x)` at the widest ceiling + the graph reaches 254 e-nodes without saturating and extracts the input unchanged; remove either + direction and it saturates at about twenty. An e-graph is supposed to absorb an inverse pair, and + this one is not absorbed because its two forms differ by a coefficient that two `Common` rules — + `a-numeric-factor-floats-out-of-a-product-of-functions` and + `a-reciprocal-rational-factor-is-a-division` — rearrange non-confluently, so each pass produces a + fresh spelling rather than a merge. Found by ablation, one set and then one rule at a time, and + 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. - **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/SaturationAblationTest.cs b/Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs new file mode 100644 index 000000000..118088bc7 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs @@ -0,0 +1,152 @@ +// +// 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 +{ + /// + /// What makes saturation at the widest ceiling run away, found by taking rules out one at a + /// time rather than by reasoning about tiers. + /// + /// + /// + /// The blow-up is not the unjudged rules as a class. It is one inverse pair, split across + /// two sets. #746 + /// tier 2's open item was phrased as "a scheduling policy for Expands/Unknown + /// rules", on the observation that sin(2x) + cos(2x) reaches 254 e-nodes without + /// saturating under the Unknown ceiling. Ablating every set in turn: removing any one + /// of Common, ExpandMultipleAngle or Trigonometric makes it saturate at + /// about twenty nodes, and removing CollapseMultipleFractions makes it worse + /// (618 — that set was acting as a brake). Ablating the rules of those three sets in turn + /// names four: + /// + /// + /// ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle — sin(2x) to + /// 2 sin x cos x; + /// Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine — + /// sin x cos x to sin(2x) / 2, the exact inverse; + /// Common / a-numeric-factor-floats-out-of-a-product-of-functions and + /// Common / a-reciprocal-rational-factor-is-a-division — which keep respelling the + /// 2 · and / 2 between the two, so the two forms never land in one e-class and + /// every pass makes a fresh spelling instead of merging. + /// + /// + /// An e-graph is supposed to absorb an inverse pair — both directions land in one class and + /// it stops. This pair does not, because its two forms differ by a coefficient the + /// Common rules rearrange non-confluently. That is a precise thing, and it is the + /// first cross-set inverse pair anything here has measured: + /// Docs/Contributing/InversePairTable.md says single-set observation "never meets" a + /// pair split across two sets, and saturation meets it because it runs every set at once. + /// + /// + /// Pinned in both directions. The runaway is a known non-saturation, and each of the four + /// rules is asserted to be load-bearing for it — so fixing the pair deletes entries here + /// rather than leaving names that mean nothing, and a fifth rule joining the cycle fails. + /// + /// + [Trait("Area", "Core")] + public sealed class SaturationAblationTest + { + private const string Runaway = "sin(2 * x) + cos(2 * x)"; + + /// + /// Saturating at twenty nodes takes a few hundred steps; the runaway is past 250 nodes by + /// thirty thousand and keeps going. Three thousand steps separates the two cleanly, and + /// the step ceiling rather than the wall is what bounds a non-culprit ablation — there are + /// about a hundred of those, and at a three-second wall each they cost the suite five + /// minutes. The second is a backstop, not the bound. + /// + private static readonly WorkBudget Quick = new() { Steps = 3_000, Time = TimeSpan.FromSeconds(1) }; + + private static readonly (string Set, string Rule)[] LoadBearing = + { + ("Common", "a-numeric-factor-floats-out-of-a-product-of-functions"), + ("Common", "a-reciprocal-rational-factor-is-a-division"), + ("ExpandMultipleAngle", "sine-of-a-whole-multiple-of-an-angle"), + ("Trigonometric", "a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine"), + }; + + private static IReadOnlyList Widest(Func keep) => + MatchedRules.All + .SelectMany(set => set.Rules.Select(rule => (set, rule))) + .Where(pair => keep(pair.set, pair.rule)) + .Select(pair => pair.rule) + .Where(rule => rule.Soundness is Soundness.Sound or Soundness.SoundUnderAssumptions) + .ToList(); + + private static (bool Saturated, int Nodes) Saturate(string source, IReadOnlyList rules) + { + var graph = new EGraph(); + graph.AddEntity(source.ToEntity()); + var ledger = BudgetLedger.For(nameof(SaturationAblationTest), Quick); + var saturated = Saturation.Run(graph, rules, ledger, node => node.Complexity); + return (saturated, graph.NodeCount); + } + + [Fact] + public void TheWidestCeilingDoesNotSaturateOnTheKnownRunaway() + { + var (saturated, nodes) = Saturate(Runaway, Widest((_, _) => true)); + Assert.False(saturated, + $"{Runaway} saturates now, at {nodes} nodes. The inverse pair above has been " + + "resolved; delete this and the load-bearing list rather than leave them."); + } + + [Fact] + public void EachOfTheFourRulesIsLoadBearingForTheRunaway() + { + var stillRunsAway = new List(); + foreach (var (setName, ruleName) in LoadBearing) + { + var rules = Widest((set, rule) => !(set.Name == setName && rule.Name == ruleName)); + Assert.True(rules.Count == Widest((_, _) => true).Count - 1, + $"{setName}/{ruleName} is not a rule in the registry any more; the entry is stale"); + var (saturated, nodes) = Saturate(Runaway, rules); + if (!saturated) + stillRunsAway.Add($"{setName}/{ruleName} removed: still {nodes} nodes and unsaturated"); + } + + Assert.True(stillRunsAway.Count == 0, + "these entries are no longer load-bearing for the runaway and should be deleted:\n" + + string.Join("\n", stillRunsAway)); + } + + /// + /// And no rule outside those four is load-bearing on its own — the pair is the whole of + /// it. Ablating every other rule of the three implicated sets must leave the runaway + /// intact, so a fifth rule joining the cycle is a change this notices. + /// + [Fact] + public void NoOtherRuleOfTheImplicatedSetsIsLoadBearing() + { + var implicated = new[] { "Common", "ExpandMultipleAngle", "Trigonometric" }; + var newlyLoadBearing = new List(); + foreach (var set in MatchedRules.All.Where(s => implicated.Contains(s.Name))) + foreach (var rule in set.Rules) + { + if (LoadBearing.Contains((set.Name, rule.Name))) continue; + var rules = Widest((s, r) => !ReferenceEquals(r, rule)); + var (saturated, nodes) = Saturate(Runaway, rules); + if (saturated) + newlyLoadBearing.Add($"{set.Name}/{rule.Name}: removing it saturates at {nodes}"); + } + + Assert.True(newlyLoadBearing.Count == 0, + "these rules are now load-bearing for the runaway and belong in the list above:\n" + + string.Join("\n", newlyLoadBearing)); + } + } +}