A multi-layer simplification/optimization transpiler that processes the output of the semantic corrector, following MeTTaIL's architectural patterns.
Status: Design Documentation Last Updated: 2025-12-06
The simplification transpiler is a post-correction source-to-source transformer that takes corrected programs and produces simplified, more readable output while preserving semantics. It integrates with the MeTTaIL correction pipeline as a final optimization pass.
Semantic Corrector Output (Corrected Proc)
↓
┌────────────────────────────────────────────┐
│ SIMPLIFICATION TRANSPILER │
│ │
│ Layer 1: Analysis Layer (Ascent-based) │
│ Layer 2: Rule Application Layer (MORK) │
│ Layer 3: Strategy Selection Layer │
│ Layer 4: Verification Layer (MeTTaIL) │
│ │
└────────────────────────────────────────────┘
↓
Simplified Source (Same Language)
transform_multi_multi_()The simplification transpiler uses bisimulation as the soundness criterion for optimizations:
| Property | Description |
|---|---|
| Soundness | If $P \approx Q$, replacing P with Q preserves all observable behaviors |
| Completeness | Bisimulation captures exactly the observable distinctions |
| Compositionality | Bisimilar subterms can be replaced in any context |
| Constraint | Strategy | Guarantee |
|---|---|---|
| Memory | Dead code elimination, scope minimization | $P \approx \text{simplify}(P)$ |
| Latency | Communication fusion, inlining | $P \approx \text{optimize}(P)$ |
| Parallelism | Scope extrusion, parallel fusion | $P \approx \text{parallelize}(P)$ |
Up-to techniques reduce verification complexity:
| Technique | Speedup |
|---|---|
| Up-to congruence | 4-100x |
| Up-to transitivity | $\mathcal{O}(1)$ amortized |
| Up-to context | 100-10,000x |
See 11-optimization-strategies.md and 12-up-to-verification.md for details.
| Technology | Role |
|---|---|
| MORK | Pattern/template rule application |
| PathMap | Memoization cache for simplified terms |
| Ascent | Datalog-based program analysis |
| MeTTaIL | Semantic predicate evaluation |
| MeTTaTron | Guard predicate execution |
| liblevenshtein | Pre-normalization of symbols |
| Rholang | Structural congruence laws |
Located in rules/:
algebraic.metta - Algebraic identity rulescontrol-flow.metta - Control flow simplificationtype-aware.metta - Type-directed rulesbeta-reduction.metta - Lambda calculus rulesrholang-congruence.metta - Rholang structural laws// 1. Receive corrected program from semantic corrector
let corrected_proc: Proc = semantic_corrector.correct(input)?;
// 2. Run analysis pass (Ascent-based)
let analysis = AnalysisLayer::new(&theory_def);
let facts = analysis.analyze(&corrected_proc);
// 3. Apply simplification rules (MORK-based)
let engine = SimplificationEngine::new(&facts);
let simplified = engine.simplify(corrected_proc);
// 4. Verify semantic preservation (MeTTaIL-based)
let verifier = VerificationLayer::new();
verifier.check(&corrected_proc, &simplified)?;
// 5. Return simplified source
Ok(simplified)
(simplification-rule
(id add-zero-right)
(category algebraic)
(phase LocalSimplification)
(pattern (Plus ?x (Num 0)))
(template ?x)
(termination-weight -1))
Rules are organized into phases that execute in order:
| Phase | Purpose | Example Rules |
|---|---|---|
LocalSimplification | Fast algebraic rewrites | x+0→x, x*1→x |
AnalysisDriven | Requires analysis facts | Dead code elimination |
StructuralNormalization | Canonical form | Rholang congruence |
TypeDirected | Requires type info | Redundant cast removal |
| Metric | Target |
|---|---|
| AST size reduction | 15-30% |
| Latency | <50ms for typical programs |
| Memory overhead | <10% additional |
See Performance Targets for detailed benchmarks.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |