A bounded pattern is walked by index, not enumerated (#1079) by Rafael-SOWNet · Pull Request #1080 · asc-community/AngouriMath

Rafael-SOWNet · 2026-08-26T17:57:02Z

Closes #1079.

MatchedRule.TryApply had two paths: IsDeterministic → one match, no allocation;
anything else → Match, a chain of iterator state machines one per pattern node, built
at every node of the tree a rewrite pass visits.

Between them sits a case that is neither and is common: a Commutative<T> node of
deterministic children offers the written order and the swapped one and nothing else.
Two candidates, known before it is asked, paid for with the whole iterator chain.

That cost is what made #1076 write six orientations out where two commutative rules would
have done — SolveMediumHard went 165.05 MB → 171.37 MB, +3.8%, past the kernel gate's
3% allocation band.

What this adds

MatchPattern.ChoiceCount — how many candidates at most, or Unbounded.
MatchPattern.TryMatchChoice(expr, bindings, n, out result) — the nth candidate, no iterator.

A node's count is the product over its children, doubled when commutative. Gathered is
Unbounded — how many ways k parts sit among n operands is a property of the
expression, not of the pattern — and anything containing one is unbounded with it.

The index is a mixed radix over the children with the first as the most significant
digit, because MatchInOrder makes it the outermost loop. Order is part of the
contract, not a detail: TryApply takes the first candidate that also satisfies the
rule's when, so two implementations that agree on the set of matches and differ on
which comes first are two different rewriters.

The count is an upper bound, not a count — a child whose name is already bound offers
one candidate or none depending on what it is asked to match, which is not known until it
is asked. An index that does not exist answers false and is skipped, exactly as an
enumeration omits it.

What holds it together

BoundedMatchingAgreesWithEnumeration: every rule in MatchedRules against the corpus
already there, asserting count, order and bindings, plus an assertion that at least
one pattern really did match more than one way — otherwise it is the deterministic test
again under another name.

DeterministicMatchingTest's set list was five names, written when there were five, and
still five while MatchedRules grew past twenty — so the test whose subject is "every
rule" was looking at a tenth of them. It reads the class now, which is why both tests
cover more than they did.

Measured

On master, with no new rule set — the sets already converted carry commutative patterns,
so the saving is there to collect before anything else is exchanged:

	`SolveMediumHard`, allocated
master (`d9b175f3`)	165,054,016 B
this branch	163,400,736 B — −1.00%

SimplifyEasy is 129,648 B on both, to the byte.

Full suite: 8630 passed, 0 failed.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd

`MatchedRule.TryApply` had two paths: a pattern that `IsDeterministic` is asked for a single match and allocates nothing, and anything else is enumerated through `Match`, which is a chain of iterator state machines, one per pattern node, built at every node of the tree a pass visits. Between the two sits a case that is neither and is common. A `Commutative<T>` node of deterministic children offers the written order and the swapped one and nothing else -- two candidates, known before it is asked. Enumerating those two costs the whole iterator chain, and on a set that runs on every pass it is measurable: `RewriteRules.Power` as data with two commutative rules took `SolveMediumHard` from 165.05 MB to 171.37 MB, +3.8%, past the kernel gate's 3% band, and had to be written out as six node patterns to land (#1076). So a pattern now says how many candidates it can offer at most -- `ChoiceCount`, or `Unbounded` where it cannot say -- and can be asked for the nth of them without an iterator. A node's count is the product over its children, doubled when commutative; `Gathered` is unbounded, because how many ways k parts sit among n operands is a property of the expression rather than of the pattern, and anything containing one is unbounded with it. The index is a mixed radix over the children with the first the most significant digit, because `MatchInOrder` makes it the outermost loop -- so indexing yields the candidates in the order enumeration yields them, which matters: `TryApply` takes the first that satisfies the rule's `when`, so two implementations agreeing on the set of matches and differing on the order are two different rewriters. The count is an upper bound rather than a count, since a child whose name is already bound offers one candidate or none depending on what it is asked to match; an index that does not exist answers false and is skipped, exactly as an enumeration omits it. `BoundedMatchingAgreesWithEnumeration` holds the two implementations together over every rule in `MatchedRules` and the corpus already there, asserting count, order and bindings, and asserting that at least one pattern did match more than one way -- or it would be the deterministic test again under another name. Measured on master, with no new rule set: `SolveMediumHard` 165,054,016 B to 163,400,736 B, -1.00%. The sets already converted carry commutative patterns, so the saving is there to collect before anything else is exchanged. The set list in `DeterministicMatchingTest` was five names, written when there were five and still five while `MatchedRules` grew past twenty -- so the test whose subject is "every rule" was looking at a tenth of them. It reads the class now. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd

…e most guarded `Patterns.PowerRules` is the biggest `switch` in the transformation layer and the one carrying the most conditions: five separate issues -- #752, #801, #802, #902 and #721 -- each put a branch-cut guard on one rewrite in it. Written as data, its thirty-five arms are thirty rules, and every one of those guards is *asked of the same helper it was written in* rather than restated here. A branch cut copied into a second file is how the two copies come to disagree, and one of these has already been wrong in both directions at once. Two rules needed something a `Bindings` cannot carry. `log_b(b) = 1` holds wherever the node is defined at all, so it takes the overload handed the matched node and reads the node's own `DomainCondition`; and the radical reduction asks `ReduceRadical` in both its `when` and its replacement, because whether it applies and what it produces are one computation. Six `switch` arms collapse into two commutative patterns -- a power times its own base, and a power times a product containing its base -- which fire exactly where the pair and the quadruple did, since the `switch` writes every orientation out. **That collapse is affordable only because of #1080.** A commutative pattern is not `IsDeterministic`, so before bounded matching it enumerated its two candidates through an iterator state machine per pattern node, at every node of every pass. The kernel gate failed this branch on allocation for exactly that: `SolveHard` +4.4% and `SolveMediumHard` +5.0%, reproduced locally as 165,054,016 B to 171,367,976 B. Writing the six arms out fixed it at the cost of the collapse; walking the candidates by index fixes it without, and the same two rules now measure 164,959,936 B against master's 163,425,360 B, +0.94% and inside the band. `SimplifyEasy` is 129,648 B either way, to the byte. Two arms bind their operands as `Number` rather than as `Entity`, so `1 - c` folds to a literal in the `switch` where `Entity` arithmetic would build a `Minusf`. The agreement run over 3,464 generated expressions found both; the data form casts and folds the same way. This is the whole value of running the two forms over generated expressions rather than over cases someone thought of. `EveryDataRuleIsClassifiedAsWritten` takes a name's classification as distinct rather than merely distinct-by-pair: `Power` and `Factorization` deliberately carry the same guarded `a^b * c^b`, and one name standing for two classifications would have listed the rule twice below rather than failed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd

…e most guarded (#1076) `Patterns.PowerRules` is the biggest `switch` in the transformation layer and the one carrying the most conditions: five separate issues -- #752, #801, #802, #902 and #721 -- each put a branch-cut guard on one rewrite in it. Written as data, its thirty-five arms are thirty rules, and every one of those guards is *asked of the same helper it was written in* rather than restated here. A branch cut copied into a second file is how the two copies come to disagree, and one of these has already been wrong in both directions at once. Two rules needed something a `Bindings` cannot carry. `log_b(b) = 1` holds wherever the node is defined at all, so it takes the overload handed the matched node and reads the node's own `DomainCondition`; and the radical reduction asks `ReduceRadical` in both its `when` and its replacement, because whether it applies and what it produces are one computation. Six `switch` arms collapse into two commutative patterns -- a power times its own base, and a power times a product containing its base -- which fire exactly where the pair and the quadruple did, since the `switch` writes every orientation out. **That collapse is affordable only because of #1080.** A commutative pattern is not `IsDeterministic`, so before bounded matching it enumerated its two candidates through an iterator state machine per pattern node, at every node of every pass. The kernel gate failed this branch on allocation for exactly that: `SolveHard` +4.4% and `SolveMediumHard` +5.0%, reproduced locally as 165,054,016 B to 171,367,976 B. Writing the six arms out fixed it at the cost of the collapse; walking the candidates by index fixes it without, and the same two rules now measure 164,959,936 B against master's 163,425,360 B, +0.94% and inside the band. `SimplifyEasy` is 129,648 B either way, to the byte. Two arms bind their operands as `Number` rather than as `Entity`, so `1 - c` folds to a literal in the `switch` where `Entity` arithmetic would build a `Minusf`. The agreement run over 3,464 generated expressions found both; the data form casts and folds the same way. This is the whole value of running the two forms over generated expressions rather than over cases someone thought of. `EveryDataRuleIsClassifiedAsWritten` takes a name's classification as distinct rather than merely distinct-by-pair: `Power` and `Factorization` deliberately carry the same guarded `a^b * c^b`, and one name standing for two classifications would have listed the rule twice below rather than failed. Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

…last set `Patterns.CommonRules` is the largest `switch` in the transformation layer and the one the exchange was always going to be judged on: a hundred arms, and the great majority of them one shape written out in every orientation its operands can take. A `switch` has to write all of them; a commutative pattern says them at once. So `x + a*x`, `x + x*a`, `a*x + x` and `x*a + x` are four arms and one rule. None of that collapsing is a guess about what the arms cover. Every orientation gathered here is one the `switch` writes out, and `MatchedRulesAgreeWithTheSwitchTest` runs both forms over 3,487 generated expressions with an empty `firesWhereTheSwitchDoesNot` -- so a pattern that reached one shape more than its arms did would fail rather than pass quietly. Where the `switch` writes only one orientation, the rule is a node pattern and stays one. Order is load-bearing here more than in any set so far. `a * a` becoming `a ^ 2` sits in the middle of the file and would swallow half of what is above it if it moved up; the rules are in the arms' order and the agreement run is what says that is enough. Ten rules bind their operands as `Number` rather than as `Entity`, so `c1 * c2` folds to a literal in the `switch` where `Entity` arithmetic would build a node. The agreement run found all sixteen affected expressions at once, `1 * y + -y` among them, which is what running two forms over generated inputs is for and what no hand-written case list would have done. `Rational(var one, var den) when one == 1 && den != 1` is now `IsWholeReciprocal` and `DenominatorOf` in `Patterns.Common.cs`, asked by both forms rather than restated here. **Measured, and the set is now cheaper than the `switch` it replaces**: `SimplifyEasy` 93,115 ns against master's 97,048 ns, -4.1%, with allocation identical at 128,100 B and `ParseEasy` and `SolveEasy` unmoved. That took two changes underneath it. Written first, this set cost **+34.6%** -- 128,995 ns to 173,659 ns -- because sixty-two rules were asked at every node against a `switch`'s single jump; #1085 indexes a set's rules by the root type each pattern requires and took `SimplifyEasy` down 36% on master alone. And its twenty commutative patterns cost 169,708,912 B of `SolveMediumHard` against 165,054,016 B before #1080, because a commutative pattern could not take the single-match path. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd

…last set (#1083) `Patterns.CommonRules` is the largest `switch` in the transformation layer and the one the exchange was always going to be judged on: a hundred arms, and the great majority of them one shape written out in every orientation its operands can take. A `switch` has to write all of them; a commutative pattern says them at once. So `x + a*x`, `x + x*a`, `a*x + x` and `x*a + x` are four arms and one rule. None of that collapsing is a guess about what the arms cover. Every orientation gathered here is one the `switch` writes out, and `MatchedRulesAgreeWithTheSwitchTest` runs both forms over 3,487 generated expressions with an empty `firesWhereTheSwitchDoesNot` -- so a pattern that reached one shape more than its arms did would fail rather than pass quietly. Where the `switch` writes only one orientation, the rule is a node pattern and stays one. Order is load-bearing here more than in any set so far. `a * a` becoming `a ^ 2` sits in the middle of the file and would swallow half of what is above it if it moved up; the rules are in the arms' order and the agreement run is what says that is enough. Ten rules bind their operands as `Number` rather than as `Entity`, so `c1 * c2` folds to a literal in the `switch` where `Entity` arithmetic would build a node. The agreement run found all sixteen affected expressions at once, `1 * y + -y` among them, which is what running two forms over generated inputs is for and what no hand-written case list would have done. `Rational(var one, var den) when one == 1 && den != 1` is now `IsWholeReciprocal` and `DenominatorOf` in `Patterns.Common.cs`, asked by both forms rather than restated here. **Measured, and the set is now cheaper than the `switch` it replaces**: `SimplifyEasy` 93,115 ns against master's 97,048 ns, -4.1%, with allocation identical at 128,100 B and `ParseEasy` and `SolveEasy` unmoved. That took two changes underneath it. Written first, this set cost **+34.6%** -- 128,995 ns to 173,659 ns -- because sixty-two rules were asked at every node against a `switch`'s single jump; #1085 indexes a set's rules by the root type each pattern requires and took `SimplifyEasy` down 36% on master alone. And its twenty commutative patterns cost 169,708,912 B of `SolveMediumHard` against 165,054,016 B before #1080, because a commutative pattern could not take the single-match path. Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

… was (#1086) `MatchedRules.Sort` records why it is expressed and not wired: paying matcher dispatch on the normalisation cost +48% of `SimplifyEasy`, which the kernel gate reported as 4.14x. That figure was measured, and it was a statement about the matcher of the day. The matcher has changed twice since -- bounded matching (#1080) and rules indexed by node type (#1085) -- and the same wiring now measures **+13.3%**: 97,048 ns to 109,968 ns on the repository's own benchmark, allocation +0.28% and inside the band. The decision does not move. Thirteen percent of the flagship benchmark for no capability is still no. What moves is the reason, and what it is a reason *about*. It is not dispatch across the rules any more. Every rule in this set is typed -- `Any<Sumf>`, `Any<Mulf>` -- so the index tries one or two at a node rather than seven. What is left is the layer: a rule is a match that binds a name and a delegate that reads it back, where a `switch` arm is a type test and a call. Everywhere else that layer buys something -- a pattern that says what the rewrite is, reversible, addressable. Here every rule is a type test and a call *already*, so there is nothing for it to buy. That is a better boundary than "the normalisation is too hot", and it is about what a rule is rather than about where it runs. It also has to be re-measured whenever the matcher changes, which is now written down, because this is the second measurement and the first one had been read as settled. Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Rafael-SOWNet merged commit 2c082da into master Aug 26, 2026
31 checks passed

Rafael-SOWNet deleted the feat/bounded-choice-matching-1079 branch August 26, 2026 18:14

Rafael-SOWNet mentioned this pull request Aug 26, 2026

A hundred arms become sixty-two rules: Common is data, the last set (#746) #1083

Merged

Rafael-SOWNet mentioned this pull request Aug 26, 2026

Thirty-five arms become thirty: Power is data (#746) #1076

Merged

Rafael-SOWNet mentioned this pull request Aug 26, 2026

The reason the canonical orders stay a switch is a third of what it was #1086

Merged

Rafael-SOWNet mentioned this pull request Aug 26, 2026

Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746

Open

Navigation Menu

Uh oh!

A bounded pattern is walked by index, not enumerated (#1079) - #1080

A bounded pattern is walked by index, not enumerated (#1079)#1080
Rafael-SOWNet merged 1 commit into
masterfrom
feat/bounded-choice-matching-1079

Rafael-SOWNet commented Aug 26, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

Rafael-SOWNet commented Aug 26, 2026

What this adds

What holds it together

Measured

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant