Skip to content

0.9.0: tree-search simplify kernel + representation/equivalence separation + certified constant folding#40

Merged
psaegert merged 16 commits into
mainfrom
release/0.9.0
Jul 24, 2026
Merged

0.9.0: tree-search simplify kernel + representation/equivalence separation + certified constant folding#40
psaegert merged 16 commits into
mainfrom
release/0.9.0

Conversation

@psaegert

Copy link
Copy Markdown
Owner

0.9.0 — new simplify kernel + representation/equivalence separation + certified constant folding

Bundles the tree-search simplify kernel with two soundness changes to the kernel. simplify is now sound and idempotent by construction, with all of its rewrite edges (rules, cancellation, constant-fold) under the same finite-a.e. certificate.

What's in it

Tree-search cancellation kernel (already on release/cancel-search)

  • simplify no longer commits to one cancellation order — it runs a best-first search over a small move graph (apply the rules pass, or cancel any one qualifying candidate) and returns the shortest state visited. Every state is a.e.-equivalent to the input, so a result can never be longer than its input.
  • Symmetric neg/inv cancellation: each class inverse is now region-continuing in its own class (behaviour change; net large reduction, a handful of 3-2-class expressions come out one token longer).
  • simplify(..., wildcard_all=…): an opt-in apply-time aggressive mode (default off; do not use on an inference/scoring path).

Representation vs equivalence (BREAKING)

  • Masking (numeric literals → <constant>) is a representation step for downstream models that cannot consume literals, not an equivalence-preserving rewrite. It is no longer performed by simplify.
  • simplify drops the mask_elementary_literals parameter. Use the new terminal Engine.mask() (relabel literals + one sort, no re-simplify) on simplify's output when placeholders are needed, and do not re-simplify a masked expression.
  • This also removes the former non-idempotence at the root: masking inside the search fixpoint could mint a free <constant> from a structural literal (x - x → 0 → <constant>) and refold it into a denominator, dropping the reachable C = 0 the input required.

Certified constant folding (FIXED)

  • The constant-fold fallback collapsed any subtree whose operands are all <constant> or finite literals to a free <constant>, on a syntactic test that assumed finite operands compose to a finite result. That is false at a pole: <constant> / 0 is ±inf/nan for every constant, so a structural zero reaching a denominator could be folded to a finite free constant — unsound (it revives a structurally zeroed term).
  • The fold now consults the same value-set analysis the rule matcher uses, collapsing to <constant> only when the subtree has a positive-measure finite part. It keeps unbounded-but-finite-a.e. folds (1/C, tan C, cosh(C+5)) and refuses non-finite-a.e. ones (C/0, C·inv(0)).

Migration

  • Replace simplify(x, mask_elementary_literals=True) with mask(simplify(x)).
  • simplify(x, mask_elementary_literals=False) is just simplify(x).
  • Never re-simplify a masked expression.

Verification

  • 71 Rust + 279 Python tests pass.
  • 64k v23.0 prior (4-3): idempotence 0/65536; median |simp|/|orig| unchanged; 105.9 µs/expr (no regression). 16 rows change under the fold fix — all degenerate structural-zero inputs, now sound.

Note for the maintainer

The CHANGELOG currently carries two (unreleased) sections: 0.9.0 (this work) and 0.8.0 (native sort promotion + the verify API, which merged to main via #39 but was never tagged). Fold 0.8.0 into 0.9.0 or tag both at release time as you prefer.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w

psaegert and others added 16 commits July 24, 2026 03:13
…g an order

Cancellation is non-confluent: taking candidate A can destroy candidate B, and
which choice ends shortest depends on what the ruleset can fold afterwards. The
kernel previously committed to one order (root-most candidate, fixed
cancel->rules alternation, endpoint-vs-input length guard) and silently lost
whenever that order was wrong.

- `Engine::simplify_search`: state = an expression; the moves are a FLAT choice
  set (apply the rules pass, or cancel any one qualifying candidate, under
  either neg/inv region shape); the answer is the shortest state ever VISITED.
  Best-first by length over the DAG with a visited-set. Because every state is
  a.e.-equivalent to the input and the input is state zero, a result can never
  exceed its input, and the greedy seed makes it never worse than the previous
  fixpoint under any budget.
- Node budget `SIMPLIPY_SEARCH_BUDGET` (default 64, 0 = old greedy fixpoint)
  bounds a rare heavy tail: median 2 expansions, 53% of expressions have no
  cancellation candidate, p99 ~186.
- Symmetric neg/inv cancellation: the unit emitted the class inverses but never
  consumed them, shielding a leaf under its own class inverse.
- `simplify(..., wildcard_all=True)`: opt-in, default-off aggressive apply-time
  mode (every placeholder binds any subtree, `!` certificate skipped).
  Documented as unsound-by-construction; not for inference/scoring paths.

64k v23.0 prior vs the previous engine: 0 rows longer in any of the 6 configs;
2867/1008/351 safe rows shorter for 2-1/3-2/4-3 (net -14086/-5910/-2060 tokens)
at ~3x simplify wall time. Frozen dev_7-3 references regenerated: 7 and 6 rows
shorter, 0 longer. 71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
The opaque neg/inv region shape entered the search as an extra move dimension,
doubling the branching at every expansion to buy ~4 rows of extra shortening
and close 6 regressions on 3-2_safe. Wrong placement: what the opaque shape is
worth is exactly the pre-0.8.0 engine's TRAJECTORY, not arbitrary opaque
interleavings, so it belongs in the seed.

Same guarantee (0 rows longer than the previous engine in all 6 configs of the
64k v23.0 prior), at no measurable cost:

  4-3_safe, budget 64 : 142.3 -> 130.6 us/expr  (transparent-only: 129.1)
  4-3_safe, budget 256: 263.7 -> 203.4 us/expr

FIX along the way: the seed was gated on the INPUT containing neg/inv, which is
wrong -- cancel EMITS the class inverses, so an expression with none can acquire
one mid-trajectory and the shapes diverge from there. idx 2189 of the prior has
no neg in its input and a neg in the shorter answer; the gate skipped the seed
exactly where it was needed, leaving 3 of the 6 regressions unfixed. Gate removed.

Frozen dev_7-3 references unchanged by this commit. 71 Rust + 279 Python green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
Reverts the opaque region shape in every form: not a policy, not a move, not a
seed. Treating the class inverses as opaque was the original defect (the unit
emitted them but never consumed them), so the pre-0.8.0 outputs that depended
on that asymmetry are deliberately NOT preserved. collect_multiplicities and
cancel_terms lose their shape parameter; simplify_search loses its second seed.

Cost of the honesty, 64k v23.0 prior: 6 of 65536 expressions on the sparse 3-2
rule set come out ONE token longer than 0.7.x (still <= input in every case),
where the opaque treatment happened to leave a sign arrangement that sparse set
can re-fold. None on 4-3 or richer. Against that: 1005 expressions SHORTER on
3-2 and 350 on 4-3 than any previous release could produce.

Also the fastest variant measured -- dropping the shape branch takes 4-3_safe
from 130.6 to 124.7 us/expr at budget 64 (opaque-as-moves was 142.3).

CHANGELOG: the "never longer than a previous release" claim is removed, since
it is no longer true; the behaviour change is documented instead.

Frozen dev_7-3 references unchanged. 71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…feel

Two things were set on reasoning rather than data. Both now measured on the
full 64k v23.0 prior (4-3, the deployed rule set).

GREEDY PRE-FILL of `best` -- keep it, it is strictly dominant. Costs ~5% wall
time, and pre-filled@32 beats un-pre-filled@64 on BOTH axes (99.7 vs 119.7
us/expr, and fewer output tokens). Without it, budget 8 leaves 551 expressions
worse than the greedy result alone; with it, 2. The experiment toggle used to
establish this is removed again -- it is not a knob anyone needs.

NODE BUDGET 64 -> 24. 24 is the smallest budget at which no expression comes
out longer than the previous release, and it sits at the elbow of the returns
curve:

  budget    8    12    16    24    32    64   256
  us/expr 65.8  74.7  80.4  91.0  99.7 125.6 190.1
  tokens/extra-us  24.8  18.1   8.6   2.9   2.6   0.7

64 cost 38% more wall time than 24 for 120 tokens out of 1.5M (0.008%).

Frozen dev_7-3 references regenerated at the new default: one row is one token
longer than at budget 64, which is the budget trade-off behaving as designed.
71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…e per candidate

The search's branching operator re-ran collect_multiplicities for every
candidate plus once to count them: b+1 tree collections per expansion where 1
suffices. cancel_successors now collects once and reuses the tree across the
per-candidate emit walks.

  4-3_safe @ budget 24: 91.0 -> 79.1 us/expr  (-13%)
  2-1_safe @ budget 24: 79.1 -> 53.6 us/expr  (-32%)

Also TRIED AND DROPPED, both measured on the full 64k v23.0 prior (4-3):
prioritising the frontier by the promise of the move that produced a state.
The diagnosis behind it is real -- cancel is usually length-neutral or +1 (it
emits a hyper/inverse prefix and leaves neutrals for the rules pass to fold),
so a heap keyed on raw length pushes the productive grow-then-fold path to the
back, which is exactly why an un-pre-filled search does badly on a small
budget. But neither fix pays:

  tie-break by candidate kind : ~15 tokens per 1.5M for +2.8% time
  score by post-rules length  : 1509437 tok @ 77.1 us  (one-ply lookahead)
  plain length key            : 1509365 tok @ 76.0 us  <- wins at matched time

Computing a better priority costs more than spending the same time expanding
more nodes. The greedy pre-fill remains the cheap fix for the same problem.

71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…nt and the pre-fill

Commits to the search model completely and deletes what predated it.

REMOVED, and this is the point: the greedy pre-fill of `best`, and with it the
entire `simplify_trajectory` fixpoint, which existed for nothing else. The
pre-fill was an unmotivated heuristic bolted onto a principled formulation, and
at matched wall-clock it buys nothing -- un-pre-filled at budget 32 is 1509383
tokens / 78.5 us against pre-filled at budget 24 with 1509365 / 79.1. Its only
real effect was forcing a second cancel->rules code path to exist.

I earlier called the pre-fill "strictly dominant". That was a misreading of my
own table: un-pre-filled@64 had FEWER tokens than pre-filled@32, not more.

Also removed: the longer-result guard (unreachable -- the root is `best`'s
initial value and mask/sort are length-neutral, so the answer is <= the input by
construction; verified across the whole 64k prior, zero outputs exceed input),
and `SimplifyCtx::cancel_memo` (only the deleted fixpoint used it; the search's
`visited` set already dedupes nodes).

Vocabulary switched throughout to node / root / children / edge / expand /
visited / frontier / budget. No "fixpoint", "trajectory" or "policy" left in
cancel.rs, and only the constant-fold helper's own local usage in simplify.rs.

Default budget 24 -> 48, the elbow of the un-pre-filled curve:

  budget      24    32    40    48    64    96   192   384
  us/expr   73.7  78.5  84.1  88.3  97.0 109.3 131.5 156.5
  tok/extra-us    13.5   9.8   7.1   3.4   2.2   1.4   0.3

64k v23.0 prior at the new default: 4-3 89.8 us/expr, 340 expressions shorter
than the previous engine, net -2007 tokens. 11 rows come out longer than the
pre-branch engine (0 with the pre-fill) -- accepted: the search wins on total
output while losing on individual rows, and no output ever exceeds its input.

71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
Deleting the fixpoint left `cancel_only`/`cancel_terms_unit` described as "the
kernel's own cancel step". There is no such thing any more: the search branches
over every cancellation candidate rather than privileging one, so the unit entry
and the kernel answer different questions and must not be read as equivalent.
Both tests renamed to pin the UNIT's contract instead of a false equivalence
(cancel_unit_selects_the_root_most_candidate / test_cancel_only_applies_one_
cancellation).

Also drops two dangling references to things this branch deleted: the
`has_annihilation` / `annihilation_only` selection filter, and
benchmarks/diff_cancel.py (absent from the repo, so it gated nothing).

71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…e_budget

Three changes, all following from taking the tree-search model literally.

IDEMPOTENCE (a real defect, found by the new invariant test). `simplify` was
not idempotent: calling it twice gave a SHORTER answer on 0.87% of the 64k
v23.0 prior, worth 979 tokens on 4-3 -- about half of what the search itself
buys. Two causes, both structural:
  * `best` is adopted when a node is GENERATED but the budget can stop before
    that node is EXPANDED, so the answer could sit one move from something
    shorter -> the search is now re-rooted at its own answer until stable;
  * masking literals and sorting operands are NOT cosmetic post-processing.
    They rewrite tokens and reorder operands, which changes which rules match,
    so a canonicalised answer can be simplifiable again -> they moved INSIDE
    the loop. This was the residual cause after the re-rooting alone.
Both are length-neutral and idempotent and every round but the last strictly
shortens, so the loop terminates. Costs +22% wall time and buys ~1000 tokens
on 4-3 -- 52 tokens per extra microsecond, an order of magnitude better than
raising the budget (3-7).

max_iter -> node_budget (BREAKING, and SIMPLIPY_SEARCH_BUDGET is gone with it).
max_iter counted iterations of a fixpoint that no longer exists, and the knob
that does matter had been hiding in an environment variable, which is no way to
expose a library parameter. The separate depth cap is deleted as provably
redundant: depth <= expansions <= budget, so a cap at or above the budget can
never bind, and measurement showed reachable depth saturating at 20 anyway.

The frozen 400-row answer sheet is replaced by an INVARIANT test (and the two
reference JSONs deleted). Pinning exact outputs of a bounded search was the
wrong shape of test -- it had to be regenerated on every tuning change and
failed confusingly at a non-default budget. It now asserts what is actually
contractual and holds at ANY budget: never longer than input, idempotent,
deterministic, monotone in budget, and most rows change. It caught the
idempotence defect on its first run.

64k v23.0 prior vs 0.7.x: 15231/6382/3007 tokens shorter (2-1/3-2/4-3);
zero non-idempotent rows, zero outputs longer than their input.
71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
Sorting IS a legitimate edge -- length-neutral, semantically identity on
commutative operands, and it changes which rules match. Tried and measured on
the 64k v23.0 prior (4-3).

It raises the reachable CEILING: with sorting confined to the pipeline loop the
corpus saturates at 1508224 tokens however large the budget grows, while
sorting as an edge reaches 1508057. But it is not efficient, because a sort
pass is then paid at every expansion:

    ~124us  budget-only 1508255 (b96)  vs  sort-edge 1508656 (b12)
    ~150us  budget-only 1508229 (b192) vs  sort-edge 1508301 (b24)
    ~174us  budget-only 1508224 (b384) vs  sort-edge 1508158 (b32)  <- crossover
    ~205us  budget-only saturated      vs  sort-edge 1508057 (b48)

Below ~170us/expr the budget wins outright; sorting only pays once the
budget-only curve has flattened. At the shipped operating point (~106us) it
costs ~2x for 241 tokens in 1.5M. The cheap way to get the same rule-unlocking
effect is what the kernel already does: sort BETWEEN pipeline rounds, a handful
of times, rather than at every node.

71 Rust + 279 Python tests green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
I had documented 0 as a kill switch that "returns the expression unsimplified".
Wrong, and materially so: 0 disables the SEARCH only -- literal masking and
operand sorting still run, so `* 2 2` comes back as `* <constant> <constant>`.
Turning literals into free constants changes what the expression means, so a
caller relying on that wording to get their input back would be misled.

Corrected in the kernel doc, the Python docstring, and the CHANGELOG.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
… the constant-fold

Two soundness changes to the simplify kernel.

Representation vs equivalence (BREAKING). Masking (numeric literals -> `<constant>`)
is a representation step for a downstream model that cannot consume literals, not an
equivalence-preserving rewrite. Entangling it with the search fixpoint was unsound: masking
mints a free `<constant>` from a structural literal (`x-x -> 0 -> <constant>`), and
re-searching that folds the fresh constant into a denominator, losing the reachable `C=0`
and turning an identically-zero term non-zeroable. It was also the sole cause of the former
non-idempotence. `simplify` is now the equivalence loop only (search + sort to a fixpoint),
sound and idempotent by construction; masking is carved out into a separate terminal
`Engine.mask()` (relabel literals + one sort, no re-simplify), which callers apply to
`simplify`'s output when placeholders are needed. `simplify` drops the
`mask_elementary_literals` parameter.

Certified constant folding (FIXED). The constant-fold fallback collapsed any subtree whose
operands are all `<constant>` or finite literals to a free `<constant>`, on a purely
syntactic test that assumed finite operands compose to a finite result. False at a pole:
`<constant>/0` is +-inf/nan for every constant, so folding it to a finite free constant both
drops the reachable non-finite value and fabricates finite ones (it revived a structurally
zeroed term). This was the one search edge that skipped the finiteness certification the rule
matcher (`match_pattern_with_cert`) and the cancellation (its group-axiom leaf gate) already
carry. The fold now consults the same value-set analysis and collapses to `<constant>` only
when the subtree has a positive-measure finite part (`interval::value_set` over R,
`has_fin && !fin_null`) -- keeping unbounded-but-finite-a.e. folds (`1/C`, `tan C`,
`cosh(C+5)`) and refusing non-finite-a.e. ones (`C/0`, `C*inv(0)`).

Verified on the 64k v23.0 prior (4-3): idempotence 0/65536; median |simp|/|orig| unchanged;
105.9us/expr (no regression); 16 rows change (all degenerate structural-zero inputs, now
sound). 71 Rust + 279 Python tests pass.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
New simplify kernel release: the cancellation search + symmetric neg/inv cancellation +
apply-time wildcard_all mode (moved to their own 0.9.0 section), plus this branch's
representation/equivalence separation (masking carved out of simplify into Engine.mask;
simplify drops mask_elementary_literals -- BREAKING) and the certified constant-fold fix.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…card_all boolean

Replaces the public `wildcard_all: bool` parameter of `simplify` with `mode: Mode = Mode.SOUND`
(the decided ordinal soundness axis; `simplipy.Mode`). `Mode.SOUND` is today's default, sound
and idempotent (inference/scoring). `Mode.LOSSY` trades soundness for recall for training-corpus
canonicalisation ONLY.

LOSSY now relaxes BOTH certificates, not just the rule matcher's: it already made every rule
placeholder bind any subtree (skipping the `!`-sort finite-a.e. certificate), and it now also
relaxes the constant-fold's finiteness gate (`try_fold_constants` folds unconditionally under
`ctx.wildcard_all`), so a non-finite-a.e. subtree such as `<constant>/0` collapses to
`<constant>` too. This is safe for training because the data is generated FROM the simplified
form (target == data), and it makes the two relaxations symmetric. SOUND is byte-identical to
before (the gate is untouched when wildcard_all is false).

Only `SOUND` (1) and `LOSSY` (3) are exposed; `EXACT` (0) and `AE` (2) are reserved rungs of the
decided `EXACT <= SOUND <= AE <= LOSSY` ordering, unimplemented. The Rust core keeps its
`wildcard_all` bool (the mechanism); the Python API translates `mode == Mode.LOSSY`.

71 Rust + 283 Python tests pass.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…nt with rules and fold

`Mode.LOSSY` already relaxed the rule matcher's `!`-certificate and the constant-fold's
finiteness gate; cancellation was the one edge still enforcing its soundness gate in LOSSY. Now
all three relax together: under `wildcard_all`, every leaf registers in BOTH connection classes
(the group-axiom gate is dropped), so `0/0 -> 1`, `inf/inf -> 1`, `inf - inf -> 0` cancel
structurally. SOUND is untouched -- the relaxation is behind the `wildcard_all` branch, and the
diagnostic `cancel_only` entry stays sound. Threads `wildcard_all` through `cancel_successors`
and `collect_multiplicities`; `children_of` passes `ctx.wildcard_all`.

71 Rust + 283 Python tests pass (TestMode now also pins the cancellation relaxation).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…ess Modes

index.md's Simplification Pipeline showed mask_literals running INSIDE simplify (stale since the
0.9.0 carve-out) and used the old max_iter/cancel->rules-fixpoint framing. Rewritten to the
search -> sort equivalence loop with masking as a separate terminal mask() step, and the mermaid
updated to match. Added a Soundness Modes section (SOUND vs LOSSY, examples, and how/why
flash-ansr uses LOSSY for training-data generation (target==data) and SOUND for inference/scoring).
Quickstart gains a mask() and a Mode.LOSSY example. Verified the existing quickstart outputs still
hold on 0.9.0.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…est tuple)

`cargo fmt --check` is a CI gate (rustfmt/clippy/test/deny). Pure formatting, no logic change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
@psaegert
psaegert merged commit 6acfd5b into main Jul 24, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant