Algebraic Simplification Rulebook¶
Reference artifact / rule catalog — instantiates Equivalence-Preserving Rewrite Optimization
A curated catalog of rewrite identities, each paired with the preconditions under which it provably preserves meaning — the trusted source of which rewrites are allowed.
Before anything rewrites anything, someone has to say which rewrites are safe. The Algebraic Simplification Rulebook is that authority: a written catalog of identities — a·b → b·a, x·2ⁿ → x << n, √(x²) → |x| — each entry carrying not just the transformation but the precondition that makes it equivalence-preserving. It is deliberately passive machinery. It does not run, choose an order, measure a speed-up, or check that a particular rewrite came out right; it is the reference that the runners, reducers, and checkers cite. Its one job — and what separates it from every active sibling — is to be the single audited place where "this form equals that form, provided X" is written down, so that no rewrite anywhere gets applied on a hunch.
Example¶
A team building a symbolic-math ("computer algebra") feature needs a simplify() that shrinks user-entered expressions. The tempting shortcut is to hard-code identities inline, and the tempting bug is √(x²) → x, which is wrong for negative x. The Rulebook is where that mistake is prevented on paper before it reaches code. Its entry reads: pattern √(x²), rewrite |x|, precondition "all real x", preserved relation "equal as real-valued functions." A neighbouring entry, (x²−1)/(x−1) → x+1, carries the precondition x ≠ 1 — the original is undefined there, so the "simpler" form is only equivalent off that point.
The outcome isn't a faster program; it's a governable one. The simplify() engine draws only from catalogued entries, each rewrite it makes is traceable to an identity with a stated precondition, and a reviewer can audit the whole simplifier by auditing the Rulebook — not by reading every call site.
How it works¶
Each entry is stored declaratively as a small record: a pattern, its rewrite, the precondition under which the two are equal, and the equivalence they are equal under (equal as functions? equal modulo rounding? equal result set?). The set is tool-agnostic — the same catalogue can feed a simplifier, a normal-form reducer, or a human reviewer. What the Rulebook deliberately withholds is just as important: it says nothing about which rule to try first, whether the rules terminate, or whether applying them actually made anything cheaper. It supplies the vocabulary of legal moves; other mechanisms supply the strategy, the guarantees, and the measurement.
Tuning parameters¶
- Precondition strictness — how tightly each identity is guarded. Narrow guards (exclude every edge case) are safe but leave rewrites on the table; broad guards apply more widely but risk an identity that is false at some ignored point.
- Directionality — whether identities are bidirectional or oriented (always "toward simpler"). Orientation is what lets the catalogue drive normalization; bidirectionality keeps it a pure equivalence reference.
- Domain scope — which algebra the entry lives in.
a·b = b·ais true for numbers and false for matrices; the Rulebook must pin each identity to its domain or it will be misapplied across one. - Granularity — a few powerful rules versus many narrow ones. Coarse rules are easier to audit; fine rules compose more predictably.
- Provenance / trust tier — whether an entry is machine-checked, hand-proven, or heuristic, flagged so consumers can decline the unproven ones.
When it helps, and when it misleads¶
Its strength is governance: a single, reviewable source of truth for what counts as a safe rewrite, which kills the ad-hoc "that looks equal to me" transformations that quietly introduce drift. It is also reusable — one audited catalogue serves every rewriter downstream.
Its characteristic failure is an identity applied outside its precondition. The textbook case is reassociating floating-point sums: (a + b) + c and a + (b + c) are algebraically identical but not numerically identical, because IEEE-754 addition is not associative, so a rule that is valid over the reals silently changes results over floats.[n1] A subtler failure is semantic drift between the catalogue and the system: identities true in ideal mathematics can be false in the implementation's actual number type or evaluation model. And the classic misuse is running it backwards — reaching for an identity to justify a rewrite already made, without checking that its precondition holds. The discipline that guards against all three is the same: every entry carries its precondition and its preserved-equivalence explicitly, and the catalogue states the domain it does not cover.
How it implements the components¶
The Rulebook fills the archetype's rule-and-contract components — the ones a static reference can own:
rewrite_rule_set— it is the enumerated set of legal transformations, the menu every rewriter draws from.equivalence_relation_contract— each entry declares the equivalence it preserves and the precondition under which that holds; together the entries define what "equivalent" means in this domain.
It does not choose application order or certify that the rules terminate and converge (that is Normal-Form Reduction and Rewrite System with Confluence Tests), does not measure whether a rewrite paid off (Benchmark Harness), and does not verify that a specific rewrite preserved behaviour on real data (Golden-Output Regression Test, Metamorphic Test Suite).
Related¶
- Instantiates: Equivalence-Preserving Rewrite Optimization — the Rulebook supplies the legal-move vocabulary the whole pattern is built on.
- Sibling mechanisms: Compiler Optimization Pass · Normal-Form Reduction · Rewrite System with Confluence Tests · Peephole Optimization · Golden-Output Regression Test
Editorial Notes¶
Form Classification¶
Form family: Representation, Specification & Plan
Rationale: A curated catalog of rewrite identities, each paired with the preconditions under which it provably preserves meaning — the trusted source of which rewrites are allowed, making its operative form a non-executable information artifact that externalizes static or prospective structure.
Independent corroboration: The frozen evidence defines Algebraic Simplification Rulebook as 'A curated catalog of rewrite identities, each paired with the preconditions under which it provably preserves meaning — the trusted source of which rewrites are allowed', so its operative form is Representation, Specification & Plan.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Mathematics
Origin pattern: Single lineage
Present-day reach: Universal
Rationale: Equivalence-preserving identities and their preconditions originate in algebraic manipulation and formal mathematics.
Related originating lineages:
- Computer Science & Software Engineering — Term-rewriting systems and compilers encode such rulebooks for automated simplification.
Review resolution: Algebraic rewrite rules have a clear mathematical lineage and universal reach, while computer science formalizes their mechanized execution. That supports single lineage and no encyclopedia synthesis; broad applicability does not require convergent provenance.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
The Rulebook asserts equivalences; it does not by itself verify them against a running system. An identity can be flawless as mathematics and still be wrong for the implementation — a wrong number type, an overflow, an evaluation-order effect. So it is a necessary upstream authority, not a sufficient guarantee: pairing it with an equivalence oracle (Golden-Output Regression Test or Metamorphic Test Suite) is what catches a catalogued identity that the real system does not actually honour.
[n1] IEEE-754 floating-point addition is not associative: reassociating or reordering a sum is algebraically valid but can change the computed result. This is the standard illustration of an identity that holds in the abstract domain (the reals) and fails in the concrete one (floats), which is exactly why each Rulebook entry must pin down its domain. ↩