Congruence Closure Duality

Abstract

Forward congruences have dual repairs, common fixed points, and an adjoint triple.

Theorem 1.1 (Dual canonical repairs of an equivalence relation).

$$\begin{array}{c}\forall Y:\mathrm{Type},F:Y\to Y,\\ \forall R:\mathrm{Setoid}(Y),\\ I(F,R)=R⟺\mathrm{IsForwardCongruence}(F,R)⟺C(F,R)=R,\\ I(F,R)\subseteq R\wedge R\subseteq C(F,R),\\ \mathrm{GaloisConnection}(closureRepair,inclusion)\wedge \mathrm{GaloisConnection}(inclusion,interiorRepair).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/CongruenceClosureDuality.dual_congruence_repair_laws (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equivalence relations on Y are ordered by relation inclusion. The predictive interior reuses the all-iterate congruence kernel, while the forgetting closure is the least stable setoid above its input.

The theorem proves contraction, monotonicity, and idempotence for the interior; extensivity, monotonicity, and idempotence for the closure; the common fixed-point characterization; both Galois connections; and the repair sandwich.

References

• Truth anchor: D5/S3/Observer/Separation/CongruenceClosureDuality.dual_congruence_repair_laws
• Dependency: D5/S3/Observer/Separation/CongruenceKernel