From 5a6a84025db7b9f34154bdb56d89def6c9a18407 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 7 Sep 2026 15:53:42 +0000 Subject: [PATCH] A graph transformation stops when its answer has, not only when the graph has #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. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Core/Transformations/Saturation.cs | 13 ++++- .../Transformation.Catalogue.cs | 51 ++++++++++++++++--- 2 files changed, 57 insertions(+), 7 deletions(-) diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 130ad9657..9f20e526f 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -109,8 +109,18 @@ private static readonly Lazy> safeRules /// witness, never the answer: what the caller finally extracts is the caller's own /// business, and is where a cheapest-form and a canonical-form caller differ. /// + /// + /// A caller's own stop, asked after every pass that merged something; + /// ends the run without the graph's fixed point having been reached. A caller that + /// extracts an answer passes "the extraction has not changed for two passes": that is + /// the fixed point which matters to it, and it comes where the graph's own may never — + /// on a rational coefficient beside a variable, the regrouping rules add a fresh e-node + /// to the root's class on every pass while its cheapest member stopped changing on the + /// third (#1200). + /// passes nothing: it needs a union, not an extraction. + /// internal static bool Run(EGraph graph, IReadOnlyList rules, - BudgetLedger ledger, Func witnessCost) + BudgetLedger ledger, Func witnessCost, Func? settled = null) { var chargedNodes = graph.NodeCount; bool ChargeGrowthSinceLastCall() @@ -220,6 +230,7 @@ bool TryTerm(out Entity value) if (!ledger.Spend()) break; graph.Rebuild(); if (!merged) saturated = true; + else if (settled is not null && settled()) break; } return saturated; } diff --git a/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs b/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs index 81fc2fc01..af6c1d136 100644 --- a/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs +++ b/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs @@ -470,10 +470,17 @@ public static Transformation EqualitySaturation(WorkBudget budget, CostModel cos /// What this is not. Not a canonical form for the language — no such thing /// exists here, since zero-equivalence is undecidable, and /// Docs/Contributing/CanonicalForm.md states that boundary. It is a canonical form - /// modulo these rules and this budget: equal trees mean the rules proved the two - /// expressions equal, different trees mean they did not, and a budget that ran out is - /// reported rather than hidden. Nothing in the library calls this — like - /// it is offered, not applied. + /// modulo these rules, this budget, and the answer having settled: equal trees mean + /// the rules proved the two expressions equal, different trees mean they did not, and a + /// budget that ran out is reported rather than hidden. The run stops once the least + /// member of the input's class has survived two passes unchanged, which is the fixed + /// point that matters to an extraction and comes where the graph's own may never — on + /// a rational coefficient beside a variable the regrouping rules add a member on every + /// pass for as long as they are allowed (#1200), + /// and the answer was settled on the third. Measured on the corpus and on those inputs, + /// no answer moved and the nine of them went from two seconds to milliseconds. Nothing + /// in the library calls this — like it is offered, not + /// applied. /// /// /// @@ -673,10 +680,31 @@ internal EqualitySaturationTransformation(WorkBudget budget, CostModel costModel graph.Rebuild(); var ledger = BudgetLedger.For(Name, budget); - Saturation.Run(graph, SafeRules, ledger, costModel.Cost); + // Stop once the answer has: after two passes in which the cheapest member of the + // root's class did not change, further merging can only add members this + // extraction would not choose. That is the fixed point a caller who extracts + // cares about, and on #1200's inputs it comes on the third pass where the + // graph's own never does. Measured on the corpus, no answer moves. + Entity? last = null; + var unchanged = 0; + bool Settled() + { + var now = graph.Extract(root, costModel.Cost); + unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0; + last = now; + return unchanged >= SettledPasses; + } + Saturation.Run(graph, SafeRules, ledger, costModel.Cost, Settled); ledger.Report(); return graph.Extract(root, costModel.Cost) ?? input; } + + /// + /// How many consecutive passes the extracted answer must survive unchanged before + /// the run stops on the answer rather than on the graph. Two, not one: a pass can + /// leave the cheapest member alone while adding what the next pass will improve on. + /// + private const int SettledPasses = 2; } /// @@ -711,7 +739,18 @@ internal GraphCanonicalizationTransformation(WorkBudget budget, RewriteRuleGrowt graph.Rebuild(); var ledger = BudgetLedger.For(Name, budget); - Saturation.Run(graph, rules, ledger, CostModel.Default.Cost); + // The same stop as EqualitySaturationTransformation's, on the least member + // rather than the cheapest, since that is what this extracts. + Entity? last = null; + var unchanged = 0; + bool Settled() + { + var now = graph.ExtractLeast(root, EntityOrder.Canonical); + unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0; + last = now; + return unchanged >= 2; + } + Saturation.Run(graph, rules, ledger, CostModel.Default.Cost, Settled); ledger.Report(); // The least member, not the cheapest: a cost model ties, and a tie would make the