Skip to content

Commit 72676b0

Browse files
The growth ceiling is the scheduling policy, and the runaway is bounded to trig (#1194)
#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. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
1 parent 102f728 commit 72676b0

3 files changed

Lines changed: 183 additions & 0 deletions

File tree

‎Sources/AngouriMath/Core/Transformations/Saturation.cs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,16 @@ internal static class Saturation
6565
/// classified may fire at all. Naming that as the widest setting makes it a request a
6666
/// caller has to make on purpose, which is the most this can honestly do about it.
6767
/// </para>
68+
/// <para>
69+
/// <b>And the ceiling is the scheduling policy, not a stand-in for one.</b> When both
70+
/// directions of an inverse pair are declared, <c>RulesUpTo(Rearranges)</c> keeps the
71+
/// collecting one and withholds the expanding one, mechanically, for every such pair.
72+
/// <c>sin(2x)</c> and <c>2 sin x cos x</c> run away at the widest ceiling and saturate at
73+
/// the safe one because <c>ExpandMultipleAngle</c> declares
74+
/// <see cref="RewriteRuleGrowth.Expands"/>. Growth is the direction marker. A pair whose
75+
/// expanding direction is unjudged is the one case this cannot protect, and that is what
76+
/// declaring a growth for a rule is for. <c>RunawayBreadthTest</c> holds this.
77+
/// </para>
6878
/// </remarks>
6979
internal static IReadOnlyList<MatchedRule> RulesUpTo(RewriteRuleGrowth widest)
7080
=> MatchedRules.All

‎Sources/AngouriMath/Docs/Contributing/InversePairTable.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,18 @@ What this is and is not:
141141
held by `SaturationAblationTest` in both directions. It is also the measured answer to what
142142
#746 tier 2 called "a scheduling policy for `Expands`/`Unknown` rules": on this input the
143143
runaway is not a tier, it is one pair.
144+
145+
And the pair is bounded. The two `Common` coefficient rules are confluent on plain arithmetic —
146+
`2 * x * y`, `(1/2) * x` and `2 * (x * y) / 3` saturate in a handful of nodes at the widest
147+
ceiling, with the trigonometric sets present and with all of them removed — so making them
148+
confluent is not a branch. The runaway is the sine family (`sin(2x)`, `sin(x) cos(x)`, `sin(3x)`,
149+
`sin(2x) cos(2x)`; not `cos(2x)`), and it does not exist without the trigonometric sets.
150+
**The growth ceiling already withholds one direction of it.** `ExpandMultipleAngle`'s rules are
151+
declared `Expands`, so `Saturation.SafeRules` — `RulesUpTo(Rearranges)` — fires only the
152+
collecting direction, and every member of the family saturates there. Growth is the direction
153+
marker and the ceiling is the scheduling policy, for every pair whose two directions are
154+
declared; a pair whose expanding direction is unjudged is the one case it cannot protect. Held by
155+
`RunawayBreadthTest`.
144156
- **It needs no reversibility mechanism at all**, which is the whole of what makes it available
145157
today: it is behaviour observed at the top of the pipeline, not a property computed about a rule.
146158
- **It answers the question equality saturation actually asks.** The consumer in the opening quote
Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
//
2+
// Copyright (c) 2019-2026 Angouri.
3+
// AngouriMath is licensed under MIT.
4+
// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.
5+
// Website: https://am.angouri.org.
6+
//
7+
8+
using System;
9+
using System.Collections.Generic;
10+
using System.Linq;
11+
using AngouriMath.Core;
12+
using AngouriMath.Core.Budgets;
13+
using AngouriMath.Core.Transformations;
14+
using AngouriMath.Core.Transformations.Matching;
15+
using AngouriMath.Extensions;
16+
using Xunit;
17+
18+
namespace AngouriMath.Tests.Core.Transformations
19+
{
20+
/// <summary>
21+
/// How broad the saturation runaway is, and where it is not. <see cref="SaturationAblationTest"/>
22+
/// names the four rules behind one input; this holds the facts that decide what to do about
23+
/// them, so that a branch already measured dead cannot be re-proposed.
24+
/// </summary>
25+
/// <remarks>
26+
/// <para>
27+
/// Two branches were on the table for the inverse pair <c>sin(2x)</c> / <c>2 sin x cos x</c>:
28+
/// withhold one direction from saturation, or make the two <c>Common</c> coefficient rules
29+
/// confluent so the graph could absorb the pair. The second assumed those rules were the
30+
/// problem. <b>They are not.</b> On plain arithmetic — <c>2 * x * y</c>, <c>(1/2) * x</c>,
31+
/// <c>2 * (x * y) / 3</c> — the widest ceiling saturates in a handful of nodes, with every
32+
/// trigonometric set present and with all of them removed. The coefficient rules were
33+
/// load-bearing in the runaway only because they supplied the respellings the trigonometric
34+
/// pair fed on.
35+
/// </para>
36+
/// <para>
37+
/// <b>The runaway is a family, and it is bounded to the trigonometric sets.</b> Every sine
38+
/// input reachable from a product loops at the widest ceiling — <c>sin(2x)</c>,
39+
/// <c>sin(x) cos(x)</c>, <c>sin(3x)</c>, <c>sin(2x) cos(2x)</c> — and <c>cos(2x)</c> does not.
40+
/// With the five trigonometric sets removed, the exemplar <c>sin(2x) + cos(2x)</c> saturates
41+
/// at seven nodes.
42+
/// </para>
43+
/// <para>
44+
/// <b>And the safe ceiling already withholds the expanding direction.</b>
45+
/// <c>ExpandMultipleAngle</c>'s rules are declared <see cref="RewriteRuleGrowth.Expands"/>,
46+
/// and <see cref="Saturation.SafeRules"/> is <c>RulesUpTo(Rearranges)</c>, so at that ceiling
47+
/// only the collecting direction fires and every member of the family saturates. That is the
48+
/// measured answer to <a href="https://github.com/asc-community/AngouriMath/issues/746">#746</a>
49+
/// tier 2's "scheduling policy" item: the growth ceiling <i>is</i> the policy. When both
50+
/// directions of an inverse pair are declared, it keeps the collecting one and withholds the
51+
/// expanding one, mechanically, for every such pair — and it can only protect pairs whose
52+
/// directions are declared, which is what declaring growth for a code-built rule is for.
53+
/// </para>
54+
/// </remarks>
55+
[Trait("Area", "Core")]
56+
public sealed class RunawayBreadthTest
57+
{
58+
private static readonly WorkBudget Quick = new() { Steps = 3_000, Time = TimeSpan.FromSeconds(1) };
59+
60+
private static readonly string[] TrigonometricSets =
61+
{
62+
"Trigonometric", "ExpandMultipleAngle", "ExpandTrigonometric",
63+
"CollapseTrigonometricFunctions", "NormalTrigonometricForm",
64+
};
65+
66+
private static IReadOnlyList<MatchedRule> Rules(RewriteRuleGrowth ceiling, Func<MatchedRuleSet, bool> keep) =>
67+
MatchedRules.All
68+
.Where(keep)
69+
.SelectMany(set => set.Rules)
70+
.Where(rule => rule.Soundness is Soundness.Sound or Soundness.SoundUnderAssumptions)
71+
.Where(rule => rule.Growth <= ceiling)
72+
.ToList();
73+
74+
private static (bool Saturated, int Nodes, string Extracted) Saturate(string source, IReadOnlyList<MatchedRule> rules)
75+
{
76+
var graph = new EGraph();
77+
var root = graph.AddEntity(source.ToEntity());
78+
var ledger = BudgetLedger.For(nameof(RunawayBreadthTest), Quick);
79+
var saturated = Saturation.Run(graph, rules, ledger, node => node.Complexity);
80+
return (saturated, graph.NodeCount, graph.Extract(root, node => node.Complexity)?.Stringize() ?? "(nothing)");
81+
}
82+
83+
private static readonly (string Input, string Extracts)[] PlainArithmetic =
84+
{
85+
("2 * x * y", "2 * x * y"),
86+
("(1/2) * x", "x / 2"),
87+
("2 * (x * y) / 3", "2/3 * x * y"),
88+
};
89+
90+
[Fact]
91+
public void TheCoefficientRulesAreConfluentOnPlainArithmetic()
92+
{
93+
var failures = new List<string>();
94+
foreach (var (input, extracts) in PlainArithmetic)
95+
foreach (var (label, rules) in new[]
96+
{
97+
("all sets", Rules(RewriteRuleGrowth.Unknown, _ => true)),
98+
("no trigonometric sets", Rules(RewriteRuleGrowth.Unknown, set => !TrigonometricSets.Contains(set.Name))),
99+
})
100+
{
101+
var (saturated, nodes, extracted) = Saturate(input, rules);
102+
if (!saturated || extracted != extracts)
103+
failures.Add($"{input} with {label}: saturated={saturated} nodes={nodes} => {extracted}");
104+
}
105+
106+
Assert.True(failures.Count == 0,
107+
"the coefficient rules no longer settle on plain arithmetic — making them confluent "
108+
+ "stopped being a phantom branch:\n" + string.Join("\n", failures));
109+
}
110+
111+
private static readonly string[] Family =
112+
{ "sin(2 * x)", "sin(x) * cos(x)", "sin(3 * x)", "sin(2 * x) * cos(2 * x)" };
113+
114+
[Fact]
115+
public void TheWidestCeilingRunsAwayOnTheWholeFamilyAndNotOnCosine()
116+
{
117+
var all = Rules(RewriteRuleGrowth.Unknown, _ => true);
118+
var settled = Family.Where(input => Saturate(input, all).Saturated).ToList();
119+
Assert.True(settled.Count == 0,
120+
"these members of the family saturate at the widest ceiling now; delete them from "
121+
+ "the list rather than leave them: " + string.Join(", ", settled));
122+
123+
var cosine = Saturate("cos(2 * x)", all);
124+
Assert.True(cosine.Saturated,
125+
$"cos(2 * x) runs away at the widest ceiling now ({cosine.Nodes} nodes); the family "
126+
+ "has grown a cosine side and the remark above is wrong about the asymmetry");
127+
}
128+
129+
[Fact]
130+
public void TheFamilyIsBoundedToTheTrigonometricSets()
131+
{
132+
var noTrig = Rules(RewriteRuleGrowth.Unknown, set => !TrigonometricSets.Contains(set.Name));
133+
var (saturated, nodes, _) = Saturate("sin(2 * x) + cos(2 * x)", noTrig);
134+
Assert.True(saturated,
135+
$"the exemplar runs away ({nodes} nodes) with every trigonometric set removed, so the "
136+
+ "runaway is no longer bounded to them");
137+
}
138+
139+
/// <summary>
140+
/// The claim that makes the ceiling the policy. Asserted, not inferred: at
141+
/// <see cref="RewriteRuleGrowth.Rearranges"/> the expanding direction is withheld and every
142+
/// member of the family must settle.
143+
/// </summary>
144+
[Fact]
145+
public void TheSafeCeilingSaturatesTheWholeFamily()
146+
{
147+
var safe = Rules(RewriteRuleGrowth.Rearranges, _ => true);
148+
var runsAway = new List<string>();
149+
foreach (var input in Family.Append("sin(2 * x) + cos(2 * x)"))
150+
{
151+
var (saturated, nodes, extracted) = Saturate(input, safe);
152+
if (!saturated) runsAway.Add($"{input}: {nodes} nodes => {extracted}");
153+
}
154+
155+
Assert.True(runsAway.Count == 0,
156+
"these run away at the safe ceiling, so the growth ceiling is not withholding the "
157+
+ "expanding direction and is not the policy the remark says it is:\n"
158+
+ string.Join("\n", runsAway));
159+
}
160+
}
161+
}

0 commit comments

Comments
 (0)