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

CHANGELOG.md

@@ -1,5 +1,76 @@
 # Changelog
 
+## 0.9.0 (unreleased)
+
+A new simplify kernel. `simplify` is now a best-first cancellation SEARCH instead of a fixed
+cancellation order; masking (numeric literals -> `<constant>`) is separated from the
+equivalence loop so representation is no longer entangled with rewriting; and the constant-fold
+fallback is brought under the same finite-a.e. certificate the rules and cancellation already
+enforce.
+
+### Added
+- **Cancellation search** (`Engine::simplify_search`). `simplify` no longer commits to one
+  cancellation order. Cancel is non-confluent -- taking candidate A can destroy candidate B,
+  and which choice ends shortest depends on what the ruleset can fold -- so the kernel now
+  SEARCHES a small move graph instead of guessing. State = an expression; the moves are a flat
+  choice set (apply the rules pass, or cancel any one qualifying candidate); the answer is the
+  shortest state visited. Every state is a.e.-equivalent to the input and the input is state
+  zero, so a result can never be longer than its own input. Best-first by
+  length with a visited-set, pre-filled with the greedy result so a truncated budget can never
+  do worse than the plain fixpoint. The node budget (`SIMPLIPY_SEARCH_BUDGET`, default 24;
+  0 restores the plain greedy fixpoint and its speed exactly) bounds a rare heavy tail -- the
+  median expression expands 2 nodes and 53% have no cancellation candidate at all, but the p99
+  is ~186. The default is the measured elbow of the returns curve on the 64k v23.0 prior: below
+  24 an extra microsecond buys ~14 output tokens, above it ~2.7, and by 256 only 0.7. On that
+  corpus the search shortens ~2860/1000/350 expressions (2-1/3-2/4-3) that no previous version
+  could reach, at ~2.3x the simplify wall time; raise the budget for offline corpus
+  canonicalisation, lower it for latency.
+- **Symmetric `neg`/`inv` cancellation** (BEHAVIOUR CHANGE). The cancellation unit already
+  EMITTED the class inverses but never CONSUMED them: a leaf under its own class inverse was
+  shielded, so `x * inv(x)` and `x + neg(x)` did not cancel through the inverse. Each inverse is
+  now region-continuing in its own class (`neg` additive, `inv` multiplicative), symmetric with
+  the emit path, and there is exactly one region shape -- the asymmetry is not preserved behind
+  a flag. Consequence on sparse rule sets: a handful of expressions come out ONE token longer
+  than in 0.7.x, because the old opaque treatment happened to leave a sign arrangement those
+  rule sets can re-fold and the connected treatment does not (6 of 65536 on the 2-1/3-2-class
+  `3-2` set; none on `4-3` or richer, and never longer than the input). Cancelling through the
+  class inverse is worth far more than it costs: the same corpus gets 1005 expressions SHORTER
+  on `3-2` and 350 on `4-3`.
+- **Soundness `Mode` (`simplify(expr, mode=Mode.SOUND)`).** A single ordinal soundness axis,
+  exposed as `simplipy.Mode`. `Mode.SOUND` (the default) is equivalence-preserving and
+  idempotent -- the deployed inference/scoring path, byte-identical to the historical default.
+  `Mode.LOSSY` trades soundness for recall: every rule placeholder binds any subtree (the
+  `!`-sort finite-a.e. certificate is skipped) AND the constant-fold's finiteness gate is
+  relaxed, so a non-finite-a.e. subtree such as `<constant>/0` collapses to `<constant>` too.
+  `Mode.LOSSY` is for training-corpus canonicalisation ONLY -- the training data is generated
+  FROM the simplified form (target == data) -- and must never run on an inference or scoring
+  path. The decided full ordering is `EXACT <= SOUND <= AE <= LOSSY`; only `SOUND` and `LOSSY`
+  are implemented.
+
+### Changed
+- **BREAKING: masking is separated from `simplify`.** Masking numeric literals to the generic
+  `<constant>` placeholder is a REPRESENTATION step for downstream models that cannot consume
+  literals, not an equivalence-preserving rewrite. `simplify` no longer masks; it is now the
+  equivalence loop only (search + sort to a fixpoint), sound and idempotent by construction. The
+  `mask_elementary_literals` parameter of `simplify` is removed; 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. Entangling masking with
+  the search fixpoint was also the sole cause of the former non-idempotence: masking mints a free
+  `<constant>` from a structural literal (`x - x -> 0 -> <constant>`), and re-searching could
+  fold that constant into a denominator, dropping the reachable `C = 0` the input required.
+
+### Fixed
+- **Constant folding respects the finiteness certificate.** 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).
+  This was the one search edge that skipped the finiteness certification the rule matcher and the
+  cancellation already enforce. The fold now consults the same value-set analysis and collapses to
+  `<constant>` only when the subtree has a positive-measure finite part, 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)`).
+
 ## 0.8.0 (unreleased)
 
 Makes the public package produce the BEST rule sets from one command: mining now natively

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "simplipy-core"
-version = "0.8.0"              # kept in lockstep with the Python package version (pyproject.toml)
+version = "0.9.0"              # kept in lockstep with the Python package version (pyproject.toml)
 edition = "2021"
 rust-version = "1.83"          # MSRV floor of the resolved tree (pyo3 0.29 requires Rust >= 1.83)
 description = "Rust inline-phase backend for the SimpliPy prefix-expression simplifier (PyO3, the simplipy._core extension)"

docs/index.md

@@ -21,8 +21,9 @@ costs that dominate at scale. SimpliPy was created to remove those bottlenecks:
 
 - **Prefix-first representation** – Expressions stay as token lists the entire
 	time, so there's no repeated parsing or AST allocation.
-- **Deterministic pipelines** – Rule application, operand sorting, and literal
-	masking always produce the same layout, which keeps downstream caches warm.
+- **Deterministic pipelines** – Rule application, operand sorting, and the separate
+	literal-masking step (`mask`) always produce the same layout, which keeps downstream
+	caches warm.
 - **ML-pipeline integration** – Outputs stay in the prefix token space consumed
 	by the `symbolic-data` layer (and through it by Flash-ANSR training) without
 	any conversion step, making it practical to simplify millions of candidates
@@ -55,55 +56,65 @@ of magnitude faster than SymPy, while producing near-identical simplification ra
 ## Simplification Pipeline (Pseudo-Algorithm)
 
 ```text
-function simplify(expr, max_iter=5):
-    tokens = parse(expr)               # infix→prefix, or validate existing prefix
-
-    for _ in range(max_iter):          # fixpoint loop
-        tokens = cancel_terms(tokens)  # one additive/multiplicative cancellation per pass
-        tokens = apply_rules(tokens)   # indexed rewrite patterns, top-down, first match wins
-        if unchanged_vs_previous_pass:
-            break                      # converged
-
-    tokens = mask_literals(tokens)     # collapse trivial numerics to <constant> (before sort)
-    tokens = sort_operands(tokens)     # canonical order for commutative ops
-    return tokens if len(tokens) <= len(input) else input   # longer results are rejected
+function simplify(expr, node_budget=48, mode=SOUND):
+    tokens = parse(expr)                        # infix→prefix, or validate existing prefix
+
+    loop:                                       # the EQUIVALENCE loop: search → sort to a fixpoint
+        best   = search(tokens, node_budget, mode)  # best-first over the rewrite MOVE graph
+                                                     # (apply the rules pass, or cancel any one
+                                                     # candidate); answer = shortest state VISITED
+        sorted = sort_operands(best)            # canonical order for commutative operands
+        if sorted == tokens: break              # converged
+        tokens = sorted
+    return tokens                               # never longer than the input (the input is
+                                                # state zero), sound and idempotent by construction
 ```
 
-Masking runs before sorting (so the canonical operand order is computed on the masked
-tokens and the mask/sort pair is a fixpoint), both run once after the loop, and a
-result longer than the input is rejected in favor of the input. Since 0.6.0 the loop
-memoizes whole passes and rule-normal subtrees per call, so the convergence-confirming
-iteration and unchanged subexpressions cost hash lookups instead of re-scans — with
-byte-identical outputs.
+`simplify` is the **equivalence loop only**. Every move — cancellation, rule application, and
+the constant-fold fallback — preserves the function almost everywhere, so the result is sound,
+never longer than the input (the input is the first candidate), and idempotent by construction.
+The search replaces the old fixed cancel→rules order: cancellation is non-confluent (taking one
+candidate can destroy another), so the kernel searches a bounded move graph instead of guessing
+(`node_budget` caps how many nodes it expands; `SIMPLIPY_SEARCH_BUDGET` overrides the default).
+
+**Masking is not part of `simplify`.** Relabelling numeric literals to the generic `<constant>`
+placeholder is a *representation* step for a downstream model that cannot consume literals, not
+an equivalence-preserving rewrite. It is a separate terminal method — apply it to `simplify`'s
+output and never re-`simplify` the result:
+
+```python
+tokens = engine.mask(engine.simplify(expr))   # literals -> <constant>, then one sort
+```
+
+The `mode` argument selects the soundness/recall trade-off; see **Soundness Modes** below.
+Since 0.6.0 the loop memoizes whole passes and rule-normal subtrees per call, so the
+convergence-confirming iteration and unchanged subexpressions cost hash lookups, not re-scans.
 
 The same call as a flowchart, with the memo state each stage touches drawn as
 cylinders (dotted links are lookups/inserts, not data flow):
 
 ```mermaid
 flowchart TD
     IN["input tokens"] --> INTERN["intern to token ids"]
-    INTERN --> CANCEL
-    subgraph LOOP["fixpoint loop (up to max_iter passes)"]
-        CANCEL["cancel_terms"] --> RULES["apply_rules"]
-        RULES --> CONV{"changed vs<br/>previous pass?"}
-        CONV -- yes --> CANCEL
+    INTERN --> SEARCH
+    subgraph LOOP["equivalence loop (search → sort to a fixpoint)"]
+        SEARCH["best-first SEARCH over the move graph<br/>(apply rules · cancel any one candidate);<br/>answer = shortest state VISITED"] --> SORT["sort operands"]
+        SORT --> CONV{"changed vs<br/>previous round?"}
+        CONV -- yes --> SEARCH
     end
-    CONV -- "no (converged)" --> MASK["mask elementary literals"]
-    MASK --> SORT["sort operands"]
-    SORT --> GUARD{"result longer<br/>than input?"}
-    GUARD -- yes --> ORIG["return original input"]
-    GUARD -- no --> OUT["output tokens"]
+    CONV -- "no (converged)" --> OUT["output tokens<br/>(≤ input · sound · idempotent)"]
+    OUT -. "callers, when placeholders needed" .-> MASK["mask() — separate terminal step:<br/>literals → &lt;constant&gt;, one sort"]
 
-    subgraph WALK["inside apply_rules: per subtree, top-down"]
+    subgraph WALK["inside the rules move: per subtree, top-down"]
         EXACT["exact rule lookup"] -- miss --> PATT["pattern scan,<br/>first match wins"]
-        PATT -- "match completed" --> CERT["certify !-bindings"]
-        PATT -- "no match" --> REC["recurse into operands,<br/>re-check the rebuilt node"]
+        PATT -- "match completed" --> CERT["certify !-bindings<br/>(skipped in LOSSY)"]
+        PATT -- "no match" --> FOLD["constant-fold fallback<br/>(finiteness-gated; relaxed in LOSSY)"]
+        FOLD -- "no fold" --> REC["recurse into operands,<br/>re-check the rebuilt node"]
     end
-    RULES -.- WALK
+    SEARCH -.- WALK
 
     STORE[("token store:<br/>engine table +<br/>per-call overlay")] -.- INTERN
-    PMEMO[("pass memos<br/>(cancel / rules)")] -.- CANCEL
-    PMEMO -.- RULES
+    PMEMO[("pass memos<br/>(cancel / rules)")] -.- SEARCH
     NF[("rule-normal<br/>subtree set")] -.- WALK
     CCACHE[("certificate caches:<br/>per-call + per-engine")] -.- CERT
 ```
@@ -114,6 +125,56 @@ corrected conversions, and real-semantics power evaluation. Byte-exact reproduct
 historical behavior (the dev_7-3 / v23.0 era) is served by installing `simplipy<=0.6.0`.
 
 
+## Soundness Modes
+
+`simplify(expr, mode=...)` selects a point on a single ordinal soundness axis, `simplipy.Mode`.
+Two rungs are implemented; `EXACT` and `AE` are reserved positions in the decided
+`EXACT ≤ SOUND ≤ AE ≤ LOSSY` ordering.
+
+- **`Mode.SOUND`** (the default) is equivalence-preserving and idempotent. Every rewrite edge
+  carries a soundness gate: rules only bind a composite subtree that a match-time certificate
+  proves defined-and-finite almost everywhere (the `!`-sort); cancellation only cancels leaves
+  where the group axioms hold; and the constant-fold collapses a subtree to a free `<constant>`
+  only when its value is finite on a positive-measure set of its constants. This is the mode to
+  use whenever the output is scored against data from an unknown function (inference, recovery
+  scoring, holdout matching).
+
+- **`Mode.LOSSY`** relaxes *all three* gates together — every rule placeholder binds any subtree
+  (`!`-certificate skipped), cancellation drops its group-axiom gate, and the constant-fold drops
+  its finiteness gate. It only ever binds *more*, so it recovers reductions the sound line leaves
+  on the table, at the cost of firing off the certified domain (pole/`inf`/`nan`-bearing
+  cofactors). It is **not** equivalence-preserving.
+
+```python
+from simplipy import Mode
+
+# <constant>/0 is ±inf/nan for every constant: SOUND keeps it, LOSSY folds it.
+engine.simplify(['/', '<constant>', '0'], mode=Mode.SOUND)   # -> ['/', '<constant>', '0']
+engine.simplify(['/', '<constant>', '0'], mode=Mode.LOSSY)   # -> ['<constant>']
+
+# A finite-a.e. subtree (pole at a single measure-zero constant) folds in BOTH modes:
+engine.simplify(['inv', '<constant>'])                       # -> ['<constant>']   (1/C)
+```
+
+**Why two modes, and how flash-ansr uses them.** The downstream trainer
+([flash-ansr](https://github.com/psaegert/flash-ansr), a transformer for symbolic regression)
+uses each mode on a different side of its pipeline:
+
+- **Training-data generation uses `Mode.LOSSY`.** A skeleton is lossy-simplified and the numeric
+  data is then generated *from that simplified form* — so the target the model learns and the data
+  it is trained on are the *same* expression (`target == data`). There is no external ground-truth
+  function for LOSSY to violate, so the aggressive reductions are safe here and they give the model
+  the shortest, most canonical target. (A structural `<constant>/0` that survives cancellation, for
+  instance, becomes a plain `<constant>`, which is what the generated data reflects.)
+
+- **Inference and recovery scoring use `Mode.SOUND`.** At test time the data comes from an unknown
+  true function; the predicted skeleton must be simplified *without* changing what it computes, or
+  the fit and the score would drift. Only the equivalence-preserving mode is safe there.
+
+That split is the whole reason both modes exist: LOSSY maximizes canonicalization where the
+simplified form *defines* the data, and SOUND guarantees equivalence where it must not.
+
+
 ## Key Components
 
 - **Parsing & normalization** – `SimpliPyEngine.parse` and
@@ -152,6 +213,14 @@ engine.simplify(['/', '<constant>', '*', '/', '*', 'x3', '<constant>', 'x3', 'lo
 # Simplify infix expressions
 engine.simplify('x3 * sin(<constant> + 1) / (x3 * x3)')
 # -> '<constant> / x3'
+
+# Mask numeric literals to <constant> AFTER simplifying (for models that need placeholders)
+engine.mask(engine.simplify(['+', 'x1', '3.14']))
+# -> ['+', '<constant>', 'x1']
+
+# Aggressive canonicalization for training targets (see Soundness Modes)
+from simplipy import Mode
+engine.simplify(['/', '<constant>', '0'], mode=Mode.LOSSY)   # -> ['<constant>']
 ```
 
 Available engines can be browsed and downloaded from Hugging Face.

examples/profile_simplify.rs

@@ -37,13 +37,13 @@ fn main() {
         .map(|l| l.split(' ').map(str::to_string).collect())
         .collect();
     for e in corpus.iter().take(200) {
-        eng.simplify(e, 5, None, true, true);
+        eng.simplify(e, 5, None, true, false);
     }
     let (a0, b0) = (ALLOCS.load(Relaxed), BYTES.load(Relaxed));
     let t0 = std::time::Instant::now();
     let mut sink = 0usize;
     for e in &corpus {
-        sink += eng.simplify(e, 5, None, true, true).len();
+        sink += eng.simplify(e, 5, None, true, false).len();
     }
     let dt = t0.elapsed();
     let (a1, b1) = (ALLOCS.load(Relaxed), BYTES.load(Relaxed));

pyproject.toml

@@ -6,7 +6,7 @@ authors = [
     ]
 readme = "README.md"
 requires-python = ">=3.11"
-version = "0.8.0"
+version = "0.9.0"
 license = "MIT"
 license-files = ["LICEN[CS]E*"]
 keywords = ["symbolic-regression", "simplification", "expression", "prefix", "rewriting", "rust"]