Formal proofs that structural congruence laws preserve bisimilarity using Relative Pushouts (RPOs).
Status: Design Documentation Last Updated: 2025-12-17
This document formalizes how each structural congruence law preserves behavioral equivalence (bisimilarity) using the Relative Pushout (RPO) framework from Wells & Stay's "Behavior in Higher-Order Languages". The key insight is that congruence laws can be proven sound by showing they preserve the LTS (Labeled Transition System) structure up to bisimulation.
The derived transition system computes transitions via IPOs (Idempotent Pushouts):
Γ ⊢ t⃗ →[c] d⟨⟨r⃗⟩⟩
where c is the minimal context (label) enabling the rewrite.
Theorem: For each structural congruence law $P \equiv Q$, we prove:
P \approx Q$ (P and Q are bisimilar)C[P] \approx C[Q]$ (congruence property)Proof Strategy: For each law, we:
(P, Q)Statement: $P | 0 \equiv P$
Claim: For all processes P, $P | 0 \approx P$.
Bisimulation Relation:
R = {(P | 0, P) | P ∈ Proc} ∪ {(P, P) | P ∈ Proc}
Proof that R is a bisimulation:
Let $(P | 0, P) \in R$. We must show:
P | 0 \to [\alpha ] Q'$, then $P \to [\alpha ] Q''$ for some Q'' with $(Q', Q'') \in R$P \to [\alpha ] Q''$, then $P | 0 \to [\alpha ] Q'$ for some Q' with $(Q', Q'') \in R$Case 1: $P | 0 \to [\alpha ] Q'$
By the semantics of parallel composition, transitions from P | 0 arise from:
P \to [\alpha ] P'$, then $P | 0 \to [\alpha ] P' | 0$0 has no actions0 has no transitionsSo if $P | 0 \to [\alpha ] Q'$, then Q' = P' | 0 for some P' with $P \to [\alpha ] P'$.
We have $(P' | 0, P') \in R$ by definition. ✓
Case 2: $P \to [\alpha ] P'$
Then $P | 0 \to [\alpha ] P' | 0$ by PAR-L rule.
We have $(P' | 0, P') \in R$ by definition. ✓
Conclusion: R is a bisimulation, so $P | 0 \approx P. \blacksquare$
The Nil identity law corresponds to a unit law in the RPO framework:
0) is the unit object for parallel compositionP | 0 factors through P with identity contextsNil identity is transparent (Definition 14) because:
C[P | 0] →[c̄] C' iff C[P] →[c̄] C'Statement: $P | Q \equiv Q | P$
Claim: For all processes P, Q: $P | Q \approx Q | P$.
Bisimulation Relation:
R = {(P | Q, Q | P) | P, Q ∈ Proc} ∪ Id
Proof that R is a bisimulation:
Let $(P | Q, Q | P) \in R$. We show the bisimulation conditions.
Transitions from P | Q:
P-transition: If $P \to [\alpha ] P'$, then $P | Q \to [\alpha ] P' | Q$
Q | P \to [\alpha ] Q | P'$(P' | Q, Q | P') \in R$ ✓Q-transition: If $Q \to [\alpha ] Q'$, then $P | Q \to [\alpha ] P | Q'$
Q | P \to [\alpha ] Q' | P$(P | Q', Q' | P) \in R$ ✓Synchronization $(\tau )$: If P and Q can communicate:
P \to [x̄\langle v\rangle] P'$ and Q →[x(v)] Q' gives $P | Q \to [\tau ] P' | Q'$Q | P \to [\tau ] Q' | P'$(P' | Q', Q' | P') \in R$ ✓Conclusion: R is a bisimulation, so $P | Q \approx Q | P. \blacksquare$
Commutativity corresponds to the symmetry of the tensor product in the RPO category:
P | Q match those from Q | PTo ensure termination when used as a simplification rule, apply the canonical ordering guard:
fn guard(&self, term: &Proc, _facts: &AnalysisFacts) -> bool {
if let Proc::Par(p, q) = term {
canonical_order(p) > canonical_order(q)
} else {
false
}
}
This ensures the rule only fires in one direction, toward canonical form.
Statement: $(P | Q) | R \equiv P | (Q | R)$
Claim: For all processes P, Q, R: $(P | Q) | R \approx P | (Q | R)$.
Bisimulation Relation:
R = {((P | Q) | R, P | (Q | R)) | P, Q, R ∈ Proc} ∪ Id
Proof Sketch:
Transitions from (P | Q) | R arise from P, Q, or R independently, or from pairwise synchronizations. The same transitions exist for P | (Q | R):
From (P | Q) | R | From P | (Q | R) | Matching |
|---|---|---|
$P \to [\alpha ] P'$ gives (P' | Q) | R | $P \to [\alpha ] P'$ gives P' | (Q | R) | ✓ |
$Q \to [\alpha ] Q'$ gives (P | Q') | R | $Q \to [\alpha ] Q'$ gives P | (Q' | R) | ✓ |
$R \to [\alpha ] R'$ gives (P | Q) | R' | $R \to [\alpha ] R'$ gives P | (Q | R') | ✓ |
| P,Q sync: τ-transition | P,Q sync: same τ-transition | ✓ |
| P,R sync: τ-transition | P,R sync: same τ-transition | ✓ |
| Q,R sync: τ-transition | Q,R sync: same τ-transition | ✓ |
Conclusion: R is a bisimulation, so $(P | Q) | R \approx P | (Q | R). \blacksquare$
Associativity corresponds to the associativity of the tensor product:
(P | Q) | R to a list [P, Q, R] then rebuilding preserves semanticsStatement: $\text{new} x.(P | Q) \equiv (\text{new} x.P) | Q$ when $x \notin \text{FV}(Q)$
Claim: When $x \notin \text{FV}(Q)$: $\text{new} x.(P | Q) \approx (\text{new} x.P) | Q$.
Bisimulation Relation:
R = {(new x.(P | Q), (new x.P) | Q) | x ∉ FV(Q)} ∪ (bisimilarity closure)
Key Insight: Since $x \notin \text{FV}(Q)$, Q cannot interact with P on channel x. Therefore:
Proof Sketch:
new x.P can still perform x̄(n) transitionsConstraint: The free-variable check $x \notin \text{FV}(Q)$ is essential for soundness.
Counterexample without constraint: If $x \in \text{FV}(Q)$:
new x.(x!v | x?y.R) can synchronize internally (τ-transition)(new x.x!v) | x?y.R exposes x in Q, changing behaviorConclusion: With the constraint, R is a bisimulation. $\blacksquare$
Scope extrusion relates to scope coherence in the RPO framework:
x \notin$ FV(Q)Scope extrusion is transparent when the constraint holds:
x \notin \text{FV}(Q)$, Q's contexts don't involve xStatement: $\text{new} x.\text{new} x.P \equiv \text{new} x.P$
Claim: $\text{new} x.\text{new} x.P \approx \text{new} x.P$.
Bisimulation Relation:
R = {(new x.new x.P, new x.P) | P ∈ Proc} ∪ Id
Proof Sketch:
The inner new x creates a fresh channel that shadows the outer new x. Since both bindings produce the same scoping effect (all occurrences of x in P are bound), the semantics are identical:
Conclusion: R is a bisimulation, so $\text{new} x.\text{new} x.P \approx \text{new} x.P. \blacksquare$
This law applies when the same variable name is used for nested scopes. With alpha-normalization, this pattern may not arise naturally, but it can appear from macro expansion or program transformation.
Statement: $\text{new} x.P \equiv P$ when $x \notin \text{FV}(P)$
Claim: When $x \notin \text{FV}(P)$: $\text{new} x.P \approx P$.
Bisimulation Relation:
R = {(new x.P, P) | x ∉ FV(P)} ∪ Id
Proof that R is a bisimulation:
Since $x \notin \text{FV}(P)$, P cannot perform any action involving x. Therefore:
Any transition from P: $P \to [\alpha ] P'$
\text{new} x.P \to [\alpha ] \text{new} x.P'$ (where $\alpha$ doesn't involve x, since $x \notin$ FV(P))x \notin \text{FV}(P')$ (which follows from $x \notin \text{FV}(P)$), then $(\text{new} x.P', P') \in R$ ✓Any transition from new x.P: Must come from P
x \notin$ FV(P), no bound outputs on xnew x.P correspond directly to P's transitionsConclusion: R is a bisimulation, so $\text{new} x.P \approx P$ when $x \notin \text{FV}(P). \blacksquare$
Dead scope elimination corresponds to the unit law for scope:
x \notin$ FV(P)| Law | Statement | Condition | Bisimilarity |
|---|---|---|---|
| Nil Identity | $P \| 0 \equiv P$ | - | ✓ Proven |
| Commutativity | $P \| Q \equiv Q \| P$ | - | ✓ Proven |
| Associativity | $(P \| Q) \| R \equiv P \| (Q \| R)$ | - | ✓ Proven |
| Scope Extrusion | $\text{new} x.(P \| Q) \equiv (\text{new} x.P) \| Q$ | $x \notin \text{FV}(Q)$ | ✓ Proven |
| Scope Fusion | $\text{new} x.\text{new} x.P \equiv \text{new} x.P$ | - | ✓ Proven |
| Dead Scope | $\text{new} x.P \equiv P$ | $x \notin \text{FV}(P)$ | ✓ Proven |
Statement: If $P_{0} \equiv P_{1} \equiv ... \equiv P_{n}$ by applying congruence laws, then $P_{0} \approx P_{n}$.
Proof: By induction on n.
Base case (n=0): $P_{0} \approx P_{0}$ by reflexivity.
Inductive case: Assume $P_{0} \approx P_{k}$. Since $P_{k} \equiv P_{k+1}$ by one congruence law, we have $P_{k} \approx P_{k+1}$ by the proofs above. By transitivity of bisimilarity, $P_{0} \approx P_{k+1}. \blacksquare$
If a program P is simplified to Q using only structural congruence laws (with their guards satisfied), then $P \approx Q$ - the simplified program is behaviorally equivalent to the original.
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 |