Equivalence Preserving Rewrite Optimization¶

Rewrite something into a cheaper, clearer, faster, safer, or more usable form only after proving or testing that the declared behavior stays equivalent.

Why this archetype exists¶

Many systems need to change form without changing what they mean or promise. A program can be refactored, a query can be replanned, a proof obligation can be rewritten, a policy clause can be clarified, and a workflow can be reordered. In each case, the improvement is real only if the new form remains equivalent under the relation that matters.

This archetype captures the design pattern for using equivalence deliberately. It does not merely say “rewrite it.” It requires a preservation gate before optimization: define what equivalence means, verify that candidates preserve it, and only then select the form that is faster, cheaper, clearer, safer, easier to prove, or easier to maintain.

Structural pattern¶

The core move is a two-stage selection process.

First, the work defines an equivalence relation. For software this might be public behavior and compatibility. For mathematics it may be logical truth or algebraic equality. For policy it may be unchanged rights, duties, exceptions, and appeal paths. For workflow it may be the same eligibility outcome plus the same audit and failure semantics.

Second, the work defines a separate cost criterion. A candidate rewrite is allowed to win on performance, maintainability, proof burden, clarity, resource use, or portability only after it has passed the preservation gate. This separation is what keeps optimization from quietly becoming behavior change.

Key components¶

Component	Description
Equivalence Relation Contract ↗	The equivalence relation says what must remain the same. It should include the visible contract, not just the obvious output. Timing, ordering, side effects, permissions, logging, error behavior, precision, and appeal rights may all be part of the relation in the right context.
Rewrite Rule Set ↗	Rewrite rules are the allowed transformations. They can be formal identities, compiler passes, refactoring rules, query transformations, workflow reorderings, or policy drafting conventions. Each rule needs preconditions so that it is not applied outside the context where it preserves equivalence.
Invariant Preservation Oracle ↗	The oracle is the evidence source: proof, type check, test suite, differential comparison, property-based test, metamorphic relation, expert review, or regression suite. The oracle does not need to be perfectly formal in every domain, but it must match the stakes and the observable boundary.
Orthogonal Cost Criterion ↗	The optimization criterion is separate from equivalence. Speed, memory use, maintainability, clarity, auditability, proof difficulty, and resource cost are common examples. The criterion should be explicit enough that a candidate cannot win by weakening the behavior it is supposed to preserve.
Rewrite Trace and Provenance ↗	A rewrite is more trustworthy when reviewers can reconstruct it. The trace records the source form, applied rules, assumptions, evidence, cost measurements, selected candidate, and owner. It supports rollback, audit, and future debugging.

Common mechanisms¶

Compiler optimization passes, query plan rewriters, algebraic simplification rulebooks, normal-form reductions, property-based equivalence tests, golden-output regression tests, benchmark harnesses, and semantics-preserving refactoring workflows are mechanisms. They instantiate the archetype, but none is the archetype by itself.

Mechanism choice depends on risk. Formal domains can use proof and rewrite-system checks. Software domains often combine regression tests, property-based tests, compatibility contracts, and benchmarks. Policy or governance domains may require expert review, crosswalks, appeal-path preservation, and decision records.

Parameters and dimensions¶

Important design dimensions include the strength of the equivalence relation, the breadth of observable behavior, the size of the candidate rewrite space, the reliability of the preservation oracle, the cost criterion being optimized, the reversibility of the rewrite, and the cost of semantic drift.

A narrow equivalence relation makes optimization easier but risks hidden change. A broad relation is safer but harder to verify. A powerful rewrite system can find better candidates but may need confluence, termination, or priority checks. A cheap benchmark may speed up selection but miss real-world workload differences.

Invariants to preserve¶

The equivalence relation must stay fixed during selection. Rewrite preconditions must be checked before applying a rule. Cost ranking must happen only after preservation is established. Evidence must stay attached to the accepted rewrite. Hidden behavior changes must be labeled as redesign, approximation, or relation revision rather than smuggled into the rewrite.

Neighbor distinctions¶

Equivalence Normalization chooses consistent representative forms for uniform treatment. This archetype is broader and cost-directed: multiple equivalent forms may remain viable, and the chosen form is selected for operational reasons.

Equivalence Class Consolidation groups different entities under shared treatment. This archetype rewrites one object, expression, plan, rule, or representation into another form.

Equivalence-Relation Refinement and Coarsening changes the sameness criterion. This archetype treats the criterion as the guardrail and optimizes inside it.

Correspondence Validation checks whether a replacement preserves behavior in an overlap domain. This archetype actively searches or selects among equivalent rewrites for operational advantage.

Bounded Approximation permits controlled error. This archetype does not unless the work is explicitly reframed.

Examples¶

A database query optimizer reorders joins to reduce execution time while preserving result semantics. A compiler transforms an expression into a lower-cost instruction sequence under language semantics. A software team refactors internals while preserving API behavior and regression outcomes. A policy team rewrites clauses for clarity while preserving rights, duties, exceptions, and appeals. A formal verification tool rewrites proof obligations into solver-friendly normal form while preserving truth.

Non-examples¶

Dropping rare cases for speed is not equivalence-preserving rewrite optimization; it is approximation or redesign. Merging duplicate records is not this archetype; it is class consolidation. Normalizing names to one canonical spelling is usually equivalence normalization. General cleanup without a behavior-preservation oracle is technical-debt work, not this archetype.

Common Mechanisms¶

Algebraic Simplification Rulebook
Benchmark Harness
Compiler Optimization Pass
Golden-Output Regression Test
Metamorphic Test Suite
Normal-Form Reduction
Peephole Optimization
Property-Based Equivalence Test
Query Plan Rewriter
Rewrite System with Confluence Tests
Rewrite Trace Log
Semantics-Preserving Refactoring

Compression statement¶

Equivalence-Preserving Rewrite Optimization applies when an object can take multiple forms that are equivalent under a named relation but differ operationally. The intervention makes the equivalence relation explicit, defines observable behavior and side-effect boundaries, generates or selects candidate rewrites, verifies preservation, ranks accepted candidates by an orthogonal cost criterion, and records the rewrite trace so the new form can be audited, rolled back, or compared with the old one.

Canonical formula: Given object x, equivalence relation ~, admissible rewrite relation R, and cost C, choose y such that x R* y, x ~ y, and C(y) is preferable among verified candidates; never optimize C by weakening ~.

Abstractions this archetype builds on — directly (a source ingredient) or as a related pattern. Links follow the typed catalog namespace.

Built directly on (7)

Equivalence Relation: Groups elements into equivalence classes.
Equivalence-Preserving Rewriting: Transforming an object into a behaviourally equivalent but operationally different form under an explicit equivalence relation, then selecting among rewrites by an orthogonal cost criterion.
Invariance: Properties unchanged under transformation.
Optimization: Finds best solution under constraints.
Refactoring: Change internal structure while preserving observable behavior.
Representation: Model complex ideas.
Transformation: A rule-governed mapping that restructures an input into a different output, holding certain invariants fixed while altering others.

Also references 20 related abstractions

Algorithm: Step-by-step problem-solving procedure.
Bijectivity: A correspondence that is exactly one-to-one and onto — no collisions, no gaps — so it is reversible and the two collections have equal size and information content.
Boundedness: Values remain within limits.
Canonical Form: A unique distinguished representative per equivalence class lets equivalence be tested by identity of representatives.
Complexity (Time/Space): Resource scaling with input size.
Constraint: Limits possibilities to guide outcomes.
Contraposition: Run an implication backward: from the absence of the consequence, infer the absence of the cause.
Correspondence Principle: New theories match old limits.
Data Integrity: Accuracy and consistency preserved.
Formal System: Symbols, formation rules, axioms, and inference rules closed under mechanical derivation.

▸ Show 10 more

Variants¶

Narrower or domain-specific specializations that share this archetype's core structure. Recognized variants are established; candidate variants are provisional.

Semantics-Preserving Refactoring · domain variant · recognized

Rewrite internal software structure while preserving externally observable behavior and improving maintainability, modularity, testability, or risk.

Distinct from parent: The parent is cross-domain; this variant focuses on software and process refactoring with technical-debt and regression-test machinery.
Use when: The public contract, tests, or observable behavior should remain unchanged; The internal representation creates complexity, duplication, coupling, or maintenance risk; Improvement is judged by maintainability, clarity, performance, or evolution cost rather than by new functionality.
Typical domains: software engineering, data pipeline design, API evolution
Common mechanisms: semantics preserving refactoring, golden output regression test, property based equivalence test, rewrite trace log

Algebraic Rewrite Optimization · mechanism family variant · recognized

Use valid algebraic, logical, symbolic, or rule-based identities to transform expressions into equivalent forms that are easier to compute, prove, inspect, or compare.

Distinct from parent: The parent includes organizational, software, and representation rewrites; this variant emphasizes formal expression transformation.
Use when: The object has formal rewrite rules with known preconditions; Different equivalent expressions have different operational costs or proof difficulty; The system needs a traceable sequence of rule applications rather than informal simplification.
Typical domains: mathematics, formal methods, compiler design, logic
Common mechanisms: algebraic simplification rulebook, rewrite system with confluence tests, normal form reduction, peephole optimization

Cost-Based Query or Plan Rewriting · domain variant · recognized

Generate equivalent execution plans, query forms, or workflow plans, then select the one with better estimated resource cost while preserving result semantics.

Distinct from parent: Narrower than the parent because it focuses on executable plans and resource estimates.
Use when: A declarative query, plan, or workflow can be executed through multiple equivalent paths; The selected path should improve time, memory, cost, throughput, or resource contention; Result equivalence must be established before cost ranking is trusted.
Typical domains: database systems, operations planning, workflow automation
Common mechanisms: query plan rewriter, benchmark harness, rewrite trace log

Contrapositive Rewrite for Proof · implementation variant · candidate

Rewrite an implication into an equivalent contrapositive when the rewritten form is easier to prove, test, or operationalize.

Distinct from parent: Narrower because the rewrite class is a logical implication transformation.
Use when: The logical system licenses the contrapositive rewrite; The contrapositive form is easier to establish than the forward implication; The rewrite is used for proof or verification rather than for practical rule-out evidence alone.
Typical domains: mathematics, formal verification, policy logic review
Common mechanisms: algebraic simplification rulebook, property based equivalence test

Near names: Behavior-Preserving Rewrite Optimization, Semantics-Preserving Transformation, Invariant-Preserving Rewrite, Equivalent Form Optimization, Cost-Directed Rewriting, Semantics-Preserving Refactoring, Normal-Form Reduction, Peephole Optimization.