NumericNeat applied to a fixed point on -x / (-y) never reaches one. It grows by exactly four
nodes every pass, indefinitely:
0 7 -x / (-y)
1 9 -1 * x / (-y)
2 15 -1 * 1 * x / (1 * y) * 1 * (-1)
3 19 -1 * 1 * 1 * x / (1 * y) * 1 * 1 * (-1)
4 23 -1 * 1 * 1 * 1 * x / (1 * y) * 1 * 1 * 1 * (-1)
...
Reproduced with Transformation.Rewriting(RewriteRules.NumericNeat).UntilStable(64), which reports
no answer — which is what its remarks say it is for: "an unbounded rewrite loop is the failure mode
this layer is supposed to make visible."
What is doing it
a-negative-factor-in-a-numerator-comes-out and a-negative-factor-in-a-denominator-comes-out.
Each takes a negative real factor out and writes the magnitude back in its place:
y / (-a * x) = -(y / (a * x))
When the factor is -1 the magnitude is 1, and the replacement puts it back as a literal 1 *
rather than folding it away. The two rules then undo each other around the accumulating factors, and
each pass leaves two more behind.
This is the same shape as #1056, where
a-numeric-quotient-of-a-numeric-multiple-collects-its-numbers and
a-negated-reciprocal-rational-factor-is-a-negated-division undid each other. That one was fixed by
having the collecting rule decline c = -1, with a comment saying why — "that is not a numeric
factor to collect but the sign, which the language spells as a product." The same reasoning applies
here: -1 is not a factor whose magnitude is worth writing out.
Severity: latent, not live
Simplify is unaffected. "-x / (-y)".Simplify() answers x / y in 68 ms, because the pipeline
is bounded and selects by size rather than running this set alone to a fixed point. Nothing a user
does today hits this.
It matters anyway for two reasons. A caller may reasonably reach for
Transformation.Rewriting(set).UntilStable(n) — the transformation layer exists to be used that way.
And equality saturation runs rule sets against a budget, so a set with no fixed point spends it.
Where it is recorded
RuleSetsDoNotCycleTest.EveryRegisteredSetSettlesOnTheSeeds pins this as the one known
set-and-expression pair that does not settle, so that a new one fails the test and this one
failing to appear also fails it — fixing it should delete the entry rather than leave a name behind
that no longer means anything.
What a fix would need to establish
Declining when the magnitude is 1 is the obvious move and matches #1056's precedent, but it
narrows two rules that are otherwise doing useful work, so it wants measuring rather than assuming:
which expressions currently reach a better form through the 1 * step, and does Simplify's
answer move for any of them. The BREAKING-CHANGES.md discipline applies if it does.
NumericNeatapplied to a fixed point on-x / (-y)never reaches one. It grows by exactly fournodes every pass, indefinitely:
Reproduced with
Transformation.Rewriting(RewriteRules.NumericNeat).UntilStable(64), which reportsno answer — which is what its remarks say it is for: "an unbounded rewrite loop is the failure mode
this layer is supposed to make visible."
What is doing it
a-negative-factor-in-a-numerator-comes-outanda-negative-factor-in-a-denominator-comes-out.Each takes a negative real factor out and writes the magnitude back in its place:
When the factor is
-1the magnitude is1, and the replacement puts it back as a literal1 *rather than folding it away. The two rules then undo each other around the accumulating factors, and
each pass leaves two more behind.
This is the same shape as #1056, where
a-numeric-quotient-of-a-numeric-multiple-collects-its-numbersanda-negated-reciprocal-rational-factor-is-a-negated-divisionundid each other. That one was fixed byhaving the collecting rule decline
c = -1, with a comment saying why — "that is not a numericfactor to collect but the sign, which the language spells as a product." The same reasoning applies
here:
-1is not a factor whose magnitude is worth writing out.Severity: latent, not live
Simplifyis unaffected."-x / (-y)".Simplify()answersx / yin 68 ms, because the pipelineis bounded and selects by size rather than running this set alone to a fixed point. Nothing a user
does today hits this.
It matters anyway for two reasons. A caller may reasonably reach for
Transformation.Rewriting(set).UntilStable(n)— the transformation layer exists to be used that way.And equality saturation runs rule sets against a budget, so a set with no fixed point spends it.
Where it is recorded
RuleSetsDoNotCycleTest.EveryRegisteredSetSettlesOnTheSeedspins this as the one knownset-and-expression pair that does not settle, so that a new one fails the test and this one
failing to appear also fails it — fixing it should delete the entry rather than leave a name behind
that no longer means anything.
What a fix would need to establish
Declining when the magnitude is
1is the obvious move and matches #1056's precedent, but itnarrows two rules that are otherwise doing useful work, so it wants measuring rather than assuming:
which expressions currently reach a better form through the
1 *step, and doesSimplify'sanswer move for any of them. The
BREAKING-CHANGES.mddiscipline applies if it does.