Skip to content

Commit e45413c

Browse files
A graph transformation stops when its answer has, not only when the graph has (#1206)
#1200's inputs -- a rational coefficient beside a variable, x / x * -x, x ^ 2 / x -- run away at the safe ceiling: the quotient-regrouping rules recombine members across classes, so every pass adds fresh e-nodes to the root's class for as long as the budget allows. Traced on x ^ 2 / x, the root extracts x from the third pass on and never stops gaining members. A caller who extracts an answer was paying the whole budget, two seconds, for an answer it had in milliseconds. Saturation.Run takes a caller's own stop, asked after every pass that merged something, and the two transformations that extract -- EqualitySaturation, the cheapest member, and CanonicalizationOverGraph, the least -- pass "the extraction has not changed for two passes". Two rather than one, because a pass can leave the chosen member alone while adding what the next pass improves on. ProvesEqual passes nothing: it needs a union, not an extraction, and keeps saturating. Measured on the corpus gate's forty problems, the nine inputs of #1200 and the five pinned ordinary ones, through both public transformations: every answer identical, and the run of all of them 13,495 ms to 320 ms -- x / x * -x 1,869 to 10 ms, x ^ 2 / x 2,010 to 3 ms, 2 ^ (-1) / sqrt(1/2) 998 to 2 ms. The remark on CanonicalizationOverGraph says what its canonical form is now modulo: these rules, this budget, and the answer having settled. What this does not do is make the rules confluent on that family; the bare graph still runs away and ConstantFoldTest still says so. #1200 stays open as the question about the rules, with its practical cost gone. Part of #746. Full suite 9610 passed, 0 failed. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
1 parent ed38186 commit e45413c

2 files changed

Lines changed: 57 additions & 7 deletions

File tree

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

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,8 +109,18 @@ private static readonly Lazy<IReadOnlyList<MatchedRule>> safeRules
109109
/// <i>witness</i>, never the answer: what the caller finally extracts is the caller's own
110110
/// business, and is where a cheapest-form and a canonical-form caller differ.
111111
/// </param>
112+
/// <param name="settled">
113+
/// A caller's own stop, asked after every pass that merged something; <see langword="true"/>
114+
/// ends the run without the graph's fixed point having been reached. A caller that
115+
/// extracts an answer passes "the extraction has not changed for two passes": that is
116+
/// the fixed point which matters to it, and it comes where the graph's own may never —
117+
/// on a rational coefficient beside a variable, the regrouping rules add a fresh e-node
118+
/// to the root's class on every pass while its cheapest member stopped changing on the
119+
/// third (<a href="https://github.com/asc-community/AngouriMath/issues/1200">#1200</a>).
120+
/// <see cref="ProvesEqual"/> passes nothing: it needs a union, not an extraction.
121+
/// </param>
112122
internal static bool Run(EGraph graph, IReadOnlyList<MatchedRule> rules,
113-
BudgetLedger ledger, Func<Entity, double> witnessCost)
123+
BudgetLedger ledger, Func<Entity, double> witnessCost, Func<bool>? settled = null)
114124
{
115125
var chargedNodes = graph.NodeCount;
116126
bool ChargeGrowthSinceLastCall()
@@ -220,6 +230,7 @@ bool TryTerm(out Entity value)
220230
if (!ledger.Spend()) break;
221231
graph.Rebuild();
222232
if (!merged) saturated = true;
233+
else if (settled is not null && settled()) break;
223234
}
224235
return saturated;
225236
}

‎Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs‎

Lines changed: 45 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -470,10 +470,17 @@ public static Transformation EqualitySaturation(WorkBudget budget, CostModel cos
470470
/// <b>What this is not.</b> Not a canonical form <i>for the language</i> — no such thing
471471
/// exists here, since zero-equivalence is undecidable, and
472472
/// <c>Docs/Contributing/CanonicalForm.md</c> states that boundary. It is a canonical form
473-
/// <i>modulo these rules and this budget</i>: equal trees mean the rules proved the two
474-
/// expressions equal, different trees mean they did not, and a budget that ran out is
475-
/// reported rather than hidden. Nothing in the library calls this — like
476-
/// <see cref="Canonicalization"/> it is offered, not applied.
473+
/// <i>modulo these rules, this budget, and the answer having settled</i>: equal trees mean
474+
/// the rules proved the two expressions equal, different trees mean they did not, and a
475+
/// budget that ran out is reported rather than hidden. The run stops once the least
476+
/// member of the input's class has survived two passes unchanged, which is the fixed
477+
/// point that matters to an extraction and comes where the graph's own may never — on
478+
/// a rational coefficient beside a variable the regrouping rules add a member on every
479+
/// pass for as long as they are allowed (<a href="https://github.com/asc-community/AngouriMath/issues/1200">#1200</a>),
480+
/// and the answer was settled on the third. Measured on the corpus and on those inputs,
481+
/// no answer moved and the nine of them went from two seconds to milliseconds. Nothing
482+
/// in the library calls this — like <see cref="Canonicalization"/> it is offered, not
483+
/// applied.
477484
/// </para>
478485
/// </remarks>
479486
/// <remarks>
@@ -673,10 +680,31 @@ internal EqualitySaturationTransformation(WorkBudget budget, CostModel costModel
673680
graph.Rebuild();
674681

675682
var ledger = BudgetLedger.For(Name, budget);
676-
Saturation.Run(graph, SafeRules, ledger, costModel.Cost);
683+
// Stop once the answer has: after two passes in which the cheapest member of the
684+
// root's class did not change, further merging can only add members this
685+
// extraction would not choose. That is the fixed point a caller who extracts
686+
// cares about, and on #1200's inputs it comes on the third pass where the
687+
// graph's own never does. Measured on the corpus, no answer moves.
688+
Entity? last = null;
689+
var unchanged = 0;
690+
bool Settled()
691+
{
692+
var now = graph.Extract(root, costModel.Cost);
693+
unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0;
694+
last = now;
695+
return unchanged >= SettledPasses;
696+
}
697+
Saturation.Run(graph, SafeRules, ledger, costModel.Cost, Settled);
677698
ledger.Report();
678699
return graph.Extract(root, costModel.Cost) ?? input;
679700
}
701+
702+
/// <summary>
703+
/// How many consecutive passes the extracted answer must survive unchanged before
704+
/// the run stops on the answer rather than on the graph. Two, not one: a pass can
705+
/// leave the cheapest member alone while adding what the next pass will improve on.
706+
/// </summary>
707+
private const int SettledPasses = 2;
680708
}
681709

682710
/// <summary>
@@ -711,7 +739,18 @@ internal GraphCanonicalizationTransformation(WorkBudget budget, RewriteRuleGrowt
711739
graph.Rebuild();
712740

713741
var ledger = BudgetLedger.For(Name, budget);
714-
Saturation.Run(graph, rules, ledger, CostModel.Default.Cost);
742+
// The same stop as EqualitySaturationTransformation's, on the least member
743+
// rather than the cheapest, since that is what this extracts.
744+
Entity? last = null;
745+
var unchanged = 0;
746+
bool Settled()
747+
{
748+
var now = graph.ExtractLeast(root, EntityOrder.Canonical);
749+
unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0;
750+
last = now;
751+
return unchanged >= 2;
752+
}
753+
Saturation.Run(graph, rules, ledger, CostModel.Default.Cost, Settled);
715754
ledger.Report();
716755

717756
// The least member, not the cheapest: a cost model ties, and a tie would make the

0 commit comments

Comments
 (0)