Repository navigation
Add a way to collect intermediate pattern replacements when simplifying #28
Description
Activity
Currently only the entities can be get but not the patterns used.
There's Entity.Alternate which returns some possible forms of the initial expression.
Or you mean step-by-step simplification?step-by-step simplification?
Yes
No point of adding it, to be honest. The way simplification works is not the one we are taught in schools so it would be garbage for the user. It's very unobvious and complicated
Okay
We're unexpectedly evolving 🦆🦆🦆
Reacted by YunsReacted by Hadrian Tang#819 implements this at rule-set granularity, and deliberately stops short of what the example above asks for.
using var recording = RewriteRecording.Start(); var simplified = ((Entity)"a / (b / c)").Simplify(); foreach (var step in recording.Steps) Console.WriteLine(step); // Common: a / (b / c) -> a * c / b
A step carries the rule set that fired, the subexpression it matched, what replaced it, and the relation and soundness tier that set declares.
Where it falls short of the example. The output above names
any1 / (any2 / any3) -> any1 * any3 / any2— an individual rewrite. Every rewrite in this library is acaseof oneswitch, which the compiler turns into a type test and a jump; making each case individually addressable would replace one dispatch per node with one delegate call per rule per node, on the hottest path there is. That wants the design document #746 item 50 asks for, and it is not something to do incidentally. Until then a step names the set, not the case.Two other honest limits, both in the type's documentation:
- The step is the subexpression, not a snapshot of the whole expression. A pass walks bottom-up and rewrites nodes as it goes, so there is no moment at which a partly-rewritten whole expression exists to photograph —
Output[0],Output[1]above would have to be constructed rather than observed. - These are the rewrites, not everything
Simplifydid. It also expands, factorises, divides polynomials, minimises boolean expressions and then chooses among candidates by a complexity metric. The steps are every rewrite that fired across every candidate generated, including the ones that lost — so they are not a route from the input to the answer returned. That route is the derivation object in Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746's v5.0 tier and needs the candidate search attributable too.
Leaving this open rather than closing it, since what it asks for is the finer grain.
- The step is the subexpression, not a snapshot of the whole expression. A pass walks bottom-up and rewrites nodes as it goes, so there is no moment at which a partly-rewritten whole expression exists to photograph —
Correcting my comment above. I gave a performance reason for stopping at rule-set granularity:
Every rewrite in this library is a
caseof oneswitch, which the compiler turns into a type test and a jump; making each case individually addressable would replace one dispatch per node with one delegate call per rule per node, on the hottest path there is.I never measured that, and it is wrong. #825 has the measurement — on the 259-node expression
DotnetBenchmarkuses forSimplifyHard, identical output and allocation across shapes:shape 15 rules 35 rules switch, as written today0.0054 ms 0.0025 ms flat list of rule delegates 0.0086 ms — bucketed by node type 0.0022 ms 0.0024 ms Rules bucketed by the node type they match are faster than the switch at fifteen rules and indistinguishable at thirty-five — because a switch over enough distinct node types is compiled into that same type dispatch anyway. Only the naive flat list is slower, and that is the one shape nobody would build.
So the reason this issue is still open is not that the grain it asks for is unaffordable. It is that transcribing forty
switcharms by hand into forty objects is forty chances to change a pattern silently, which is an argument for a source generator over the existing bodies, not for leaving the rewrites unnamed.The claim is withdrawn from the source and the contributor docs in #826, and #825 is the design document for doing it properly.
#951 landed the grain this issue asks for: a step now names the individual rewrite, not just the set. The example at the top is answered literally — running
a / (b / c)through a recording onmasterat2d128f3cproducesCommon/Divf(var any1, Divf(var any2, var any3)): 1 / (1 / c) -> 1 * c / 1which is the
any1 / (any2 / any3) -> any1 * any3 / any2the issue wrote out by hand.But I am not closing this, because measuring the same example says the derivation is still not readable. Of 259 recorded steps, 13 name a rule and 246 do not:
steps set Rules.Count237 CanonicalOrder0 3 CommonDenominator0 3 CanonicalOrderCountingConstants0 3 CommonDenominatorCountingConstants0 All four are among the fourteen sets whose rewrites are not a
switchover the expression, so there are no arms to generate from and nothing to name.CanonicalOrderalone is 91% of the steps.Two separate things follow, and I think only the first is this issue's.
1. The fourteen non-
switchsets are the remaining gap. They are already the binding constraint for #746 item 51 — the e-graph cannot schedule what cannot declare a direction — and this shows they are the binding constraint for #28 as well, on its own example. Same work unblocks both.2. A readable derivation needs the sort's steps collapsed, not named. Even if
CanonicalOrdercould name every rewrite, 237 of them for oneSimplifyofa / (b / c)is not something a human reads. This is close to what @WhiteBlackGoose said in 2020:The way simplification works is not the one we are taught in schools so it would be garbage for the user.
That objection was about the content of the steps and it has aged well, but the measurement points somewhere narrower than "no point adding it": the mechanism is fine and the useful steps are already legible — it is the normalisation passes that swamp them. Filtering a recording to the steps that name a rule leaves four lines for this expression, and those four are readable.
So a plausible shape for the rest of this issue is a recording that reports normalisation as one collapsed step rather than 237, with the named rewrites in between. Raising it here rather than opening an issue, since it is a question about what the feature is for.
- added a commit that references this issue
on Aug 17, 2026 - added a commit that references this issue
on Aug 23, 2026
Add a way to collect intermediate pattern replacements when simplifying.
e.g.
Input: x^(-1)/(y/z)
Output[0]: x^(-1)*z/y // any1 / (any2 / any3) -> any1 * any3 / any2
Output[1]: 1/x*z/y // Powf.PHang(any1, Num(-1)) -> 1 / any1
...