Repository navigation
RewriteRules.Common does not terminate: a three-cycle on -x * 1/2 #1056
Description
Activity
- added a commit that references this issue
on Aug 25, 2026 The three arms are identified, and the normalisation is not one of them.
Applying
CommonwithoutInnerSimplifiedbetween passes reproduces the cycle unchanged, so the
normalisation is a bystander here — every step is a pureCommonrewrite:1: -1/2 * x Mulf(-1/2, x) -> raw Mulf(-1, Divf(x, 2)) 2: -x / 2 Mulf(-1, Divf(x, 2)) -> raw Divf(Mulf(-1, x), 2) 3: -x / 2 Divf(Mulf(-1, x), 2) -> raw Mulf(-1/2, x)Each rewrite was attributed by asking every addressable rule in
RewriteRules.Common.Ruleswhich
one reproduces the observed output — which is what the arm-level registry is for, and is the only
reason this can be named rather than guessed at:step arm rule -1/2 * x→-(x / 2)CommonRules:237Mulf(Rational(var mOne, var den), var any1) => -(any1 / den)-(x / 2)→(-1 * x) / 2CommonRules:88Mulf(var any1, Divf(var any2, var any3)) => any1 * any2 / any3(-1 * x) / 2→-1/2 * xCommonRules:82Divf(Mulf(Number const1, var any1), Number const2) => const1 / const2 * any1Reading the arm order in the source would have got this wrong:
CommonRules:19is
Divf(Mulf(Number const1, var any1), var any2) => const1 * (any1 / any2), sits far above
CommonRules:82, and matches the third shape — it is simply not the arm that fires. That was worth
finding out by measurement rather than by reading.The orientation is not undetermined; it is specified and unimplemented.
Docs/Contributing/CanonicalForm.md
§4 givesMulf's canonical form as "flat, ordered, numeric factors folded into one leading factor",
which makesMulf(-1/2, x)the canonical member of the three andCommonRules:237the arm pointing
away from it. So the question is not which of the three is the destination — the specification
already answers that — but whetherCommonmay stop offering the quotient form at all, given that
237 and its three neighbours (234–238) exist so thatx / 2is printed rather than1/2 * x.That is a printed-output change across a wide surface rather than a rule fix, which is why this
stays open rather than being closed by a patch.- added a commit that references this issue
on Aug 31, 2026
RewriteRules.Commoniterated on-x * 1/2never reaches a fixed point, with or without thenormalisation between passes. Found by a new test that puts #746 tier 2's "termination checked by
tooling rather than asserted by authors" into the build rather than into a workspace harness.
The cycle
Printed forms are not enough to see it — two of the three trees print the same string — so this is
the shape:
So the cycle proper is
three distinct trees printing as two distinct strings. Each step is
Common.ApplyOnce(...)followedby
.InnerSimplified, which is howSimplificatorruns the set.ApplyOnceis deterministic —-x / 2parsed fresh always rewrites to-1/2 * x. The apparentnon-determinism in a printed trace is only the two trees at steps 2 and 3 sharing a string.
What it does and does not break
Simplifydoes not hang: it bounds its own iteration, and"-x * 1/2".Simplify()is-1/2 * xin about 40 ms. So this is not a user-visible defect today.It matters because tier 2 makes rule sets first-class data that a caller may apply on its own, and
Commonis not a terminating rewrite system on its own. Two rules disagree about which ofc * xand(c * x) / dis the destination, and nothing records that the orientation is a choice.Why it was not found before
work/rulecheckhas measured termination for a while and reportsPowerandNumericNeatassettling only in composition. Its corpus has no unary shape applied to a compound expression, so
-x * 1/2is not in it. The corpus was the limit, not the check.Not fixed here
Choosing an orientation changes the output shape of a set that runs on nearly every simplification,
and
CanonicalOrderExactand the normalisation already interact in ways that have been surprisingbefore. That is a deliberate decision rather than a patch, so this is filed rather than fixed.
The new test names
Commonin a list of known non-terminating sets and asserts the list in bothdirections, so a set that starts cycling fails and a set that stops cycling has to leave the list.