Formal proofs that simplification phases compose transparently, preserving behavioral equivalence.
Status: Design Documentation Last Updated: 2025-12-17
This document establishes that the 4-layer simplification architecture preserves semantics through transparency - the property that each phase's transformations don't introduce observable differences. We connect this to Wells & Stay's transparency definition (Definition 14) to ensure weak bisimilarity is a congruence.
A context c is transparent if for every non-reactive use, there exists a unique c̄ such that:
c(t) →[c̄] d(t)
In other words, a transparent context doesn't "absorb" transitions - it passes them through predictably.
Definition: A simplification rule r: P ↦ Q is transparent if:
C[P] \approx C[Q]$The simplification transpiler has 4 layers:
┌────────────────────────────────────────────┐
│ Layer 1: Analysis (Ascent-based) │ ← Read-only
│ Layer 2: Rule Application (MORK) │ ← Transform
│ Layer 3: Strategy Selection │ ← Control
│ Layer 4: Verification (MeTTaIL) │ ← Read-only
└────────────────────────────────────────────┘
Claim: The Analysis phase is trivially transparent.
Proof: The analysis phase is read-only:
Therefore, P_out = P_in, and $P_\text{in} \approx P_\text{out}$ trivially.
Transparency: Trivially satisfied since no transformation occurs. $\blacksquare$
Claim: The Rule Application phase is transparent when each rule preserves bisimilarity.
Proof Structure:
Each rule r: pattern → template is proven bisimilarity-preserving in 09-rpo-congruence-proofs.md. The key properties:
Individual rule transparency: For rule r with $P \equiv Q$:
P \approx Q$ (bisimilarity, proven via RPO)C[P] \approx C[Q]$ (congruence)Sequential composition: If $P \approx Q$ and $Q \approx R$, then $P \approx R$ by transitivity
Rule application order: The strategy layer ensures termination, but any valid ordering preserves bisimilarity
Formal Statement:
Let apply_rules(P) be the result of exhaustively applying rules in the Rule Application phase. If every rule r_i satisfies $P \approx r_i(P)$ when applicable, then:
P ≈ apply_rules(P)
Proof: By induction on the number of rule applications. Each step preserves bisimilarity, and transitivity gives the final result. $\blacksquare$
Claim: The Strategy Selection phase is transparent.
Proof: The strategy layer controls rule ordering but does not modify the program directly:
The strategy layer is a meta-level controller:
The strategy layer affects when transformations happen, not what they are.
Transparency: Satisfied because it's a control layer, not a transformation layer. $\blacksquare$
Claim: The Verification phase is trivially transparent.
Proof: The verification phase is read-only:
The verification phase does not modify the program. It either:
In both cases, the output is behaviorally equivalent to some valid program state.
Transparency: Trivially satisfied since no transformation occurs. $\blacksquare$
Statement: The complete simplification pipeline is transparent:
P ≈ simplify(P)
where simplify is the composition of all 4 layers.
Proof:
Let P₀ be the input program. Define:
P₁ = Analysis(P₀) = P₀ (read-only)P₂ = RuleApplication(P₁) (transformative)P₃ = Strategy(P₂) = P₂ (control-only, output equals P₂)P₄ = Verification(P₃) (either P₃ or rollback to P₀)Case 1: Verification accepts P₃
P_{0} \approx P_{1}$ (trivial, same program)P_{1} \approx P_{2}$ (Layer 2 transparency)P_{2} \approx P_{3}$ (trivial, same program)P_{3} \approx P_{4}$ (trivial, same program)P_{0} \approx P_{4}$ ✓Case 2: Verification rejects P₃
P_{0} \approx P_{0}$ trivially ✓Conclusion: $P_{0} \approx \text{simplify}(P_{0})$ in all cases. $\blacksquare$
A context g is IPO uniform if transitions factor predictably through sublists. Formally, for derived transitions:
Γ ⊢ t⃗ →[c] d⟨⟨r⃗⟩⟩
The factorization through subcontexts is consistent.
Claim: Structural congruence rules satisfy IPO uniformity.
Evidence:
Nil Identity (P | 0 → P):
[- | 0]$Commutativity (P | Q → Q | P):
Associativity ((P | Q) | R → P | (Q | R)):
Scope Extrusion (new x.(P | Q) → (new x.P) | Q when $x \notin \text{FV}(Q)$):
If every context is either reactive or IPO uniform, then weak bisimilarity is a congruence.
The ρ-calculus (and Rholang) satisfies this condition:
\text{out}(n,-) | \text{in}(n,\lambda x.-)$ (communication pairs)For non-reactive contexts, we've shown:
Conclusion: Weak bisimilarity is a congruence for Rholang, ensuring that behaviorally equivalent programs remain equivalent in all contexts.
P \approx r(P)$ onceP \approx Q$, then $C[P] \approx C[Q]$ for all C/// Transparent simplification result
pub struct TransparentSimplification<P> {
/// Original program
pub original: P,
/// Simplified program
pub simplified: P,
/// Evidence of transparency
pub evidence: TransparencyEvidence,
}
#[derive(Clone, Debug)]
pub enum TransparencyEvidence {
/// No transformation occurred
Identity,
/// Single rule application with bisimilarity proof
SingleRule {
rule_name: String,
bisim_proof: BisimulationWitness,
},
/// Composition of transparent transformations
Composition(Vec<TransparencyEvidence>),
/// Verified by bisimulation check
BisimulationVerified(BisimulationWitness),
}
impl<P> TransparentSimplification<P> {
/// Assert that simplification preserves behavior
pub fn is_valid(&self) -> bool {
matches!(
&self.evidence,
TransparencyEvidence::Identity
| TransparencyEvidence::SingleRule { .. }
| TransparencyEvidence::Composition(_)
| TransparencyEvidence::BisimulationVerified(_)
)
}
}
Transparency enables compositional testing:
#[test]
fn test_rule_transparency() {
// Generate random process
let proc = arbitrary_process();
// Apply rule
let simplified = apply_nil_identity(&proc);
// Verify bisimilarity
assert!(check_bisimilar(&proc, &simplified));
}
#[test]
fn test_phase_transparency() {
let proc = arbitrary_process();
// Apply full simplification
let result = simplify_full(&proc);
// Must be bisimilar
assert!(check_bisimilar(&proc, &result.simplified));
// Evidence must be valid
assert!(result.evidence.is_valid());
}
For rules r₁, r₂, ..., rₙ applied in sequence:
P ≈ r₁(P) ≈ r₂(r₁(P)) ≈ ... ≈ rₙ(...r₁(P)...)
Proof: By induction on n, using transitivity of $\approx .$
If rules r₁ and r₂ are independent (act on disjoint parts of the AST), then:
r₁(r₂(P)) ≈ r₂(r₁(P))
This enables parallel rule application when rules don't interfere.
For rules involving lambda-abstracted continuations (e.g., $\text{in}(x, \lambda y.P)$):
(\lambda x.P) v \approx P[v/x]$ preserves bisimilarity\lambda x.P x \approx P$ when $x \notin \text{FV}(P)$These higher-order rules are also transparent when applied correctly:
Following Definition 1 (Behavior Paper), meta-contexts $\langle -\rangle : T \to T$ are generated by:
- \times X$ (product on the left)[X \to -]$ (exponential)Transparency of higher-order rules follows from the fibered structure:
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 |