Repository navigation
A rational coefficient beside a variable never reaches a fixed point at the safe ceiling #1200
Description
Activity
The budget overshoot on these same inputs is #1199.
A correction, measured once extraction stopped being the cost (the fix for #1199 makes a whole-graph extraction a fixed point from the leaves up; the old top-down walk took 1.9 s on a 253-node graph, which is what made these look bounded). Same inputs, 200,000 steps / 30 s, safe ceiling:
input fixed point e-nodes wall x ^ 2 / xno 11,755 30.0 s x / x * -xno 12,563 30.0 s x / x * x * 1/2no 10,773 30.0 s 2 ^ (-1) / sqrt(1/2)no, step ceiling 1,565 3.7 s x * 1/2 * 2no, step ceiling 1,022 1.0 s 2 * x * 1/2,(2 - 0) * x * 1/2,1 / (1/2) * x * 1/2no, step ceiling 558–559 0.2–0.8 s So this is two families, not one stall: the three with an
x / xorx ^ 2 / xare genuine runaways at about 400 e-nodes a second, and the coefficient-only ones plateau at some 560 e-nodes and stop because the steps run out. "Bounded at 135–583 e-nodes after thirty seconds" above was the slow extraction, not the graph. Every one still extracts the right answer, and the budget is now honoured to the millisecond, so what bounds them is the budget and nothing intrinsic.ConstantFoldTestis corrected to say the same.The practical cost of this is gone with #1206, without pretending the rules are confluent. The two public transformations that extract an answer —
Transformation.EqualitySaturation(cheapest member) andTransformation.CanonicalizationOverGraph(least member) — now stop once the extraction has survived two passes unchanged, which on these inputs comes on the third pass where the graph's own fixed point never does. Measured through both, before and after, on the corpus gate's forty problems and the nine inputs above: every answer identical, and the run of all of them 13,495 ms → 320 ms —x / x * -x1,869 → 10 ms,x ^ 2 / x2,010 → 3 ms,2 ^ (-1) / sqrt(1/2)998 → 2 ms.Saturation.ProvesEqualkeeps saturating (it needs a union, not an extraction) and the bareSaturation.Runstill runs away on this family, whichConstantFoldTeststill pins.So this stays open as the question about the rules — a normal form for a coefficient's spellings inside the graph, or an orientation among the regrouping rules — but nothing a caller reaches waits on it any more.
At the safe ceiling (
RulesUpTo(Rearranges)), seven of the 3,630 shapes in the growth corpus neverreport a fixed point, and they are one family: a rational coefficient beside a variable.
Measured (build
98a9420c, after #1198)WorkBudget { Steps = 200_000, Time = 30 s }, one input per graph:2 * x * 1/2xx * 1/2 * 2x(2 - 0) * x * 1/2xx / x * -x-xx / x * x * 1/2x / 2x / x * x ^ (-2)x ^ (-2)1 / (1/2) * x * 1/2xx ^ 2 / xx2 ^ (-1) / sqrt(1/2)sqrt(1/2)So this is a stall, not a runaway: the graph barely grows with fifteen times the budget, and
every extraction is right.
ConstantFoldTest.ACoefficientBesideAVariableStallsRatherThanRunsAwaypins it in both directions — an entry that starts saturating is to be deleted, and one that grows
past a thousand e-nodes has stopped being a stall.
What it is
The spellings of a coefficient beside a variable —
1/2 * x,x / 2,x * 2 ^ (-1),2 ^ (-1) * x— are exchanged byRearrangesrules (a-reciprocal-rational-factor-is-a-division,a-reciprocal-power-is-a-quotient, the quotient and product regrouping rules ofCommon), and afresh spelling keeps appearing at the edge of what has been rewritten, so a pass never comes back
empty. Before #1198 the same rules ran away on constant-only input (
2 - 0 + 0 * 2, 54 cases),because with nothing folding a number the spellings were unbounded; folding rationals on
insertion bounded the family without closing it.
RunawayBreadthTesthad called these rules"confluent on plain arithmetic" from three inputs; it now says what was measured.
What would close it, not decided
Either a normal form for a rational coefficient inside the graph —
c * xwithca literal,folded on insertion the way a rational over rationals now is — or an orientation among the
spelling rules so that only one direction fires under saturation. The first is a mechanism; the
second is what the growth ceiling already does for expanding rules and would need a marker for
"rearranges, but one way". Neither is worth doing until something calls the graph on this shape;
Transformation.CanonicalizationOverGraphis offered, not applied.Found while measuring #746 tier 2 item 4 (PR #1198). Related: the budget overshoot on these
same inputs, filed separately.