From e26203e01dc843dfb82cba130175682a99525889 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sat, 5 Sep 2026 10:36:08 +0000 Subject: [PATCH] A rule set that never settles over a whole tree is caught too The cycle check added with this file rewrites at the root, which is what makes its "a term came back" criterion mean something -- but it is also what it cannot see past. A full pass can move its rewrite to a different node each time and never repeat a term while still never settling. `UntilStable` already answers that question. It reports hitting its bound as no answer rather than as the last value reached, and its remarks say why: "an unbounded rewrite loop is the failure mode this layer is supposed to make visible, and handing back a value from the middle of one would hide exactly the case worth seeing." This is a caller taking it up on that, over every registered set and the same seeds. It finds one, and it is not a cycle. NumericNeat grows `-x / (-y)` by four nodes a pass for ever: -1 * 1 * 1 * ... * x / (1 * y) * 1 * 1 * ... * (-1) The rules that bring a negative factor out of a numerator and out of a denominator each write the magnitude back in its place, and when the factor is -1 the magnitude is 1, which goes back as a literal `1 *` rather than folding. The two then undo each other around the factors that accumulate. That is the shape of #1056 one file over, and #1056's fix was to decline c = -1 for the same reason -- the sign is not a factor whose magnitude is worth writing out. Simplify is not affected and answers `x / y`: the pipeline is bounded and picks by size rather than running this set alone to a fixed point. So it is latent, and it is filed as #1167 rather than fixed here, because declining at a magnitude of 1 narrows two rules that are otherwise doing useful work and wants measuring first. Pinned as the one known pair rather than counted, so that a new one fails and so does this one going away: a fix should delete the entry rather than leave a name that no longer means anything. Full suite 9555 passed, 0 failed. Part of #825. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Transformations/RuleSetsDoNotCycleTest.cs | 54 +++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleSetsDoNotCycleTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleSetsDoNotCycleTest.cs index bb0d4c976..e0272bd5f 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleSetsDoNotCycleTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleSetsDoNotCycleTest.cs @@ -112,6 +112,60 @@ public void NoRuleSetRewritesBackToATermItHasAlreadyProduced() + string.Join("\n", cycles.Distinct())); } + /// + /// The same question over a whole tree rather than at the root, which is the half the + /// loop above cannot answer: a full pass can move its rewrite to a different node each + /// time and never repeat a term while still never settling. + /// + /// + /// UntilStable reports hitting its bound as no answer rather than as the + /// last value reached, and its remarks say why — "an unbounded rewrite loop is the failure + /// mode this layer is supposed to make visible, and handing back a value from the middle + /// of one would hide exactly the case worth seeing". This is a caller taking it up on + /// that. + /// + [Fact] + public void EveryRegisteredSetSettlesOnTheSeeds() + { + // Named rather than counted, so that finding another one is a change to this list. + // NumericNeat grows `-x / (-y)` by four nodes a pass for ever: the rules that bring a + // negative factor out of a numerator and out of a denominator each leave the + // magnitude of -1 behind as a literal `1 *` factor instead of folding it, and then + // undo each other around it -- + // -1 * x / (-y) + // -1 * 1 * x / (1 * y) * 1 * (-1) + // -1 * 1 * 1 * x / (1 * y) * 1 * 1 * (-1) + // `Simplify` is not affected and answers `x / y`, because the pipeline is bounded and + // picks by size rather than running this set alone to a fixed point. It is a set with + // no fixed point on an ordinary input all the same. + // https://github.com/asc-community/AngouriMath/issues/1167 + var known = new[] { "NumericNeat: -x / (-y)" }; + + var unsettled = new List(); + + foreach (var set in RewriteRules.All) + { + var rewriting = Transformation.Rewriting(set).UntilStable(Steps); + foreach (var start in Corpus()) + { + TransformationResult result; + try { result = rewriting.Apply(start); } + catch { continue; /* a rule declining loudly is not this test's subject */ } + if (!result.Succeeded) + unsettled.Add($"{set.Name}: {start.Stringize()}"); + } + } + + var unexpected = unsettled.Distinct().Except(known).ToList(); + Assert.True(unexpected.Count == 0, + $"{unexpected.Count} set-and-expression pairs newly fail to reach a fixed point " + + $"in {Steps} passes:\n" + string.Join("\n", unexpected.Take(20))); + + // And the known one is still known: fixing it should delete it from the list rather + // than leave a name here that no longer means anything. + Assert.Equal(known, unsettled.Distinct().Intersect(known).ToArray()); + } + /// /// The loop above has to actually rewrite something, or it passes by never firing. Named /// as a count that moves rather than as "it works".