Setoid.Congruences.Presented.Decidable¶
Decidability of finitely presented congruences¶
This is the Setoid.Congruences.Presented.Decidable module of the Agda Universal Algebra Library.
Setoid.Congruences.Presented.Basic proved the reconstruction half of the decidable
layer: every decidable congruence on a finite carrier is ≑ to Cg of its
related-pairs list. This module proves the converse half, which is
Presentation decidability.1 On a finite finitary algebra, membership in the
congruence Cg (fromPairs ps) generated by a finite pair list ps is decidable, so
every finitely presented congruence upgrades to a DecCon.
Together the two halves show that, on finite finitary algebras, the finitely
presented congruences and the decidable congruences coincide up to ≑.
Unlike reconstruction, decidability genuinely needs both finiteness interfaces:
- the carrier data
FiniteAlgebra(Setoid.Algebras.Finite) and - the signature data
FiniteSignature(Setoid.Signatures.Finite),
because the closure must be computed under every basic operation, which requires searching the operation symbols and, for each, the finitely many tuples of each arity.
The algorithm¶
Candidate relations are represented computationally as Boolean matrices
indexed by the carrier enumeration: Matrix = Fin card → Fin card → Bool.
-
Seed. The seed sets entry
(i , j)whenenum i ≈ enum jor the pair is presented byps— both decidable, by_≟_andfromPairs?. -
Closure. One closure step sets
(i , j)when it was already set, or its transpose was set (symmetry), or somekhas(i , k)and(k , j)set (one-step transitivity), or some operation symbol applied to two componentwise-related index tuples has images≈-matching(enum i , enum j)(compatibility). Each disjunct is decidable, the last by searching the enumerated symbols and the enumerated tuplesallVecs. -
Iteration. The step is iterated
card ² + 1times, stopping early at the first fixpoint (iterFix). A non-fixpoint step strictly increases the number of set bits (matCount), which is bounded bycard ², so the fuel suffices and the resultclosureis a fixpoint of the step — the pigeonhole argument is carried by the small counting lemmasbit-*,rowCount-*,matCount-*below.
Soundness (closure-sound). Every set bit of the closure
witnesses a genuine derivation in the generation datatype Gen of
Setoid.Congruences.Generation — by induction over the iteration, each step
disjunct mapping to the corresponding rule of Gen.
Completeness (GenR⊆closureRel). Decoding the fixpoint matrix
along chosen enumeration indices yields a relation closureRel that
is a congruence containing the presented relation — reflexivity over ≈ comes from
the seeded diagonal, symmetry and transitivity from the fixpoint equation, and
compatibility from the fixpoint equation plus the surjectivity of the symbol and
arity enumerations. By the congruence generation theorem (Cg-least)
the generated congruence is therefore contained in closureRel.
Soundness and completeness together give the decision procedure
Cg-dec: to decide Gen (fromPairs ps) x y, test one bit of the
closure matrix. Cg-DecCon packages the result as a
DecCon at the working congruence level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ of
Setoid.Congruences.Finite.Basic.2
Counting set bits¶
The termination argument is a pigeonhole: a Boolean matrix over Fin m × Fin n
has at most m * n set bits, and each strictly growing step sets at least one
more. We develop the count from the single-bit case upward, so that every lemma
is a one-line combination of monotonicity facts about _+_.
-- The numeric value of one bit. bit : Bool → ℕ bit true = 1 bit false = 0 -- A bit is at most 1. bit-bound : (b : Bool) → bit b ≤ 1 bit-bound true = s≤s z≤n bit-bound false = z≤n -- Implication of bits is monotone in the value. bit-mono : {b c : Bool} → (T b → T c) → bit b ≤ bit c bit-mono {false} {false} _ = z≤n bit-mono {false} {true} _ = z≤n bit-mono {true} {false} bc = ⊥-elim (bc tt) bit-mono {true} {true} _ = s≤s z≤n -- A bit that flips from unset to set strictly increases in value. bit-strict : {b c : Bool} → ¬ T b → T c → bit b < bit c bit-strict {false} {true} _ _ = s≤s z≤n bit-strict {false} {false} _ () bit-strict {true} {_} ¬tb _ = ⊥-elim (¬tb tt) -- A distinct implied bit must flip from unset to set. bit-flip : {b c : Bool} → (T b → T c) → b ≢ c → (¬ T b) × T c bit-flip {false} {false} _ ne = ⊥-elim (ne refl) bit-flip {false} {true} _ _ = (λ z → z) , tt bit-flip {true} {false} bc _ = ⊥-elim (bc tt) bit-flip {true} {true} _ ne = ⊥-elim (ne refl)
- Two conversions between a decision's
doesbit and the decided proposition.3
-- A set decision bit yields its witness. does-out : {p : Level} {P : Type p} (d : Dec P) → T (does d) → P does-out (true because ofʸ w) _ = w does-out (false because _) () -- A witness sets the decision bit. does-in : {p : Level} {P : Type p} (d : Dec P) → P → T (does d) does-in (true because _) _ = tt does-in (false because ofⁿ ¬w) w = ¬w w
- The count of set bits in a Boolean row, with its bound, monotonicity, and strict growth on a flipped witness.
-- The number of set bits in a row. rowCount : {n : ℕ} → (Fin n → Bool) → ℕ rowCount {zero} g = 0 rowCount {suc n} g = bit (g zero) + rowCount (g ∘ suc) -- A row of length n has at most n set bits. rowCount-bound : {n : ℕ} (g : Fin n → Bool) → rowCount g ≤ n rowCount-bound {zero} g = z≤n rowCount-bound {suc n} g = +-mono-≤ (bit-bound (g zero)) (rowCount-bound (g ∘ suc)) -- Pointwise implication of rows is monotone in the count. rowCount-mono : {n : ℕ} {g h : Fin n → Bool} → (∀ i → T (g i) → T (h i)) → rowCount g ≤ rowCount h rowCount-mono {zero} gh = z≤n rowCount-mono {suc n} gh = +-mono-≤ (bit-mono (gh zero)) (rowCount-mono (λ i → gh (suc i))) -- Pointwise implication with a flipped witness strictly increases the count. rowCount-strict : {n : ℕ} {g h : Fin n → Bool} → (∀ i → T (g i) → T (h i)) → (i₀ : Fin n) → ¬ T (g i₀) → T (h i₀) → rowCount g < rowCount h rowCount-strict gh zero ¬g₀ h₀ = +-mono-<-≤ (bit-strict ¬g₀ h₀) (rowCount-mono (λ i → gh (suc i))) rowCount-strict gh (suc i₀) ¬gᵢ hᵢ = +-mono-≤-< (bit-mono (gh zero)) (rowCount-strict (λ i → gh (suc i)) i₀ ¬gᵢ hᵢ)
- The same three facts for a matrix, summing the row counts.
-- The number of set bits in a matrix. matCount : {m n : ℕ} → (Fin m → Fin n → Bool) → ℕ matCount {zero} M = 0 matCount {suc m} M = rowCount (M zero) + matCount (M ∘ suc) -- An m × n matrix has at most m * n set bits. matCount-bound : {m n : ℕ} (M : Fin m → Fin n → Bool) → matCount M ≤ m * n matCount-bound {zero} M = z≤n matCount-bound {suc m} M = +-mono-≤ (rowCount-bound (M zero)) (matCount-bound (M ∘ suc)) -- Pointwise implication of matrices is monotone in the count. matCount-mono : {m n : ℕ} {M N : Fin m → Fin n → Bool} → (∀ i j → T (M i j) → T (N i j)) → matCount M ≤ matCount N matCount-mono {zero} MN = z≤n matCount-mono {suc m} MN = +-mono-≤ (rowCount-mono (MN zero)) (matCount-mono (λ i → MN (suc i))) -- Pointwise implication with a flipped witness strictly increases the count. matCount-strict : {m n : ℕ} {M N : Fin m → Fin n → Bool} → (∀ i j → T (M i j) → T (N i j)) → (i₀ : Fin m) (j₀ : Fin n) → ¬ T (M i₀ j₀) → T (N i₀ j₀) → matCount M < matCount N matCount-strict MN zero j₀ ¬m₀ n₀ = +-mono-<-≤ (rowCount-strict (MN zero) j₀ ¬m₀ n₀) (matCount-mono (λ i → MN (suc i))) matCount-strict MN (suc i₀) j₀ ¬mᵢ nᵢ = +-mono-≤-< (rowCount-mono (MN zero)) (matCount-strict (λ i → MN (suc i)) i₀ j₀ ¬mᵢ nᵢ)
Enumerating index tuples¶
The compatibility component of the closure step searches all pairs of arity tuples of
carrier indices. A tuple of length k over Fin n is represented as a
Vec, and allVecs n k lists all n ^ k of them;
∈-allVecs is the completeness of that enumeration, which the
compatibility proof uses to inject a concrete tuple into the search space.
-- All length-k vectors over Fin n. allVecs : (n k : ℕ) → List (Vec (Fin n) k) allVecs n zero = [] ∷ [] allVecs n (suc k) = concatMap (λ i → map (i ∷_) (allVecs n k)) (allFin n) -- Every length-k vector over Fin n occurs in allVecs n k. ∈-allVecs : {n k : ℕ} (v : Vec (Fin n) k) → v ∈ allVecs n k ∈-allVecs [] = here refl ∈-allVecs {n} {suc k} (i ∷ v) = ∈-concat⁺′ (∈-map⁺ (i ∷_) (∈-allVecs v)) (∈-map⁺ (λ x → map (x ∷_) (allVecs n k)) (∈-allFin i))
The closure computation¶
Fix a finite finitary algebra — an algebra 𝑨 with carrier-finiteness data 𝑭 and
signature-finiteness data 𝑺 — and a pair list ps. Throughout, R abbreviates
the presented relation fromPairs ps and GenR the relation of the congruence it
generates.
module _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρ} (𝑭 : FiniteAlgebra 𝑨) (𝑺 : FiniteSignature 𝑆) (ps : List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ])) where open FiniteAlgebra 𝑭 using ( _≟_ ; card ; enum ; enum-sur ) open FiniteSignature 𝑺 using ( opCard ; opEnum ; opEnum-sur ; arCard ; arEnum ; arIdx ; arEnum-arIdx ) open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) private -- The presented relation and its decision procedure. R : BinaryRel 𝕌[ 𝑨 ] (α ⊔ ρ) R = fromPairs {𝑨 = 𝑨} ps R? : ∀ x y → Dec (R x y) R? = fromPairs? {𝑨 = 𝑨} _≟_ ps -- The relation of the congruence generated by the presented relation. GenR : BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) GenR = Gen {𝑨 = 𝑨} R -- A chosen enumeration index for each carrier element, and its correctness. idx : 𝕌[ 𝑨 ] → Fin card idx x = enum-sur x .proj₁ idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x idx-≈ x = enum-sur x .proj₂ -- Candidate relations, represented as Boolean matrices over the enumeration. Matrix : Type Matrix = Fin card → Fin card → Bool -- The total number of matrix entries: the pigeonhole bound. entries : ℕ entries = card * card
The seed. Entry (i , j) starts set when the enumerated pair is ≈-equal
or presented.
-- The ways an entry can be set initially. BaseHit : Fin card → Fin card → Type (α ⊔ ρ) BaseHit i j = (enum i ≈ enum j) ⊎ R (enum i) (enum j) baseHit? : ∀ i j → Dec (BaseHit i j) baseHit? i j = (enum i ≟ enum j) ⊎-dec R? (enum i) (enum j) -- The seed matrix. (Private: it is internal machinery of the closure -- computation, and the name `seed` is the certificate-schema vocabulary of -- Setoid.Congruences.Certificates.Schema, with which it would clash in the -- Setoid.Congruences barrel.) private seed : Matrix seed i j = does (baseHit? i j) -- Reading a seed bit back as its proposition, and conversely. seed-out : ∀ {i j} → T (seed i j) → BaseHit i j seed-out {i} {j} = does-out (baseHit? i j) seed-in : ∀ {i j} → BaseHit i j → T (seed i j) seed-in {i} {j} = does-in (baseHit? i j)
The step. The auxiliary notions first: componentwise relatedness of two index tuples, the decoding of an index tuple to a carrier tuple, and the compatibility hit at one enumerated operation symbol.
-- Componentwise relatedness of two index tuples under a matrix. allRelated : Matrix → {k : ℕ} → Vec (Fin card) k → Vec (Fin card) k → Type allRelated M t s = ∀ p → T (M (lookup t p) (lookup s p)) allRelated? : ∀ M {k} (t s : Vec (Fin card) k) → Dec (allRelated M t s) allRelated? M t s = all? (λ p → T? (M (lookup t p) (lookup s p))) -- The carrier tuple encoded by a tuple of carrier indices. tupleOf : (f : OperationSymbolsOf 𝑆) → Vec (Fin card) (arCard f) → (ArityOf 𝑆 f → 𝕌[ 𝑨 ]) tupleOf f t a = enum (lookup t (arIdx f a)) -- The compatibility hit at symbol index fi: some pair of componentwise -- related index tuples whose images match (enum i , enum j) up to ≈. OpHit : Matrix → Fin opCard → Fin card → Fin card → Type ρ OpHit M fi i j = Any (λ t → Any (λ s → allRelated M t s × (enum i ≈ (f ^ 𝑨) (tupleOf f t)) × (enum j ≈ (f ^ 𝑨) (tupleOf f s))) (allVecs card (arCard f))) (allVecs card (arCard f)) where f = opEnum fi opHit? : ∀ M fi i j → Dec (OpHit M fi i j) opHit? M fi i j = anyL? (λ t → anyL? (λ s → allRelated? M t s ×-dec ((enum i ≟ (f ^ 𝑨) (tupleOf f t)) ×-dec (enum j ≟ (f ^ 𝑨) (tupleOf f s)))) (allVecs card (arCard f))) (allVecs card (arCard f)) where f = opEnum fi -- The transitivity hit: a two-step path through some middle index. TransHit : Matrix → Fin card → Fin card → Type TransHit M i j = ∃[ k ] (T (M i k) × T (M k j)) transHit? : ∀ M i j → Dec (TransHit M i j) transHit? M i j = any? (λ k → T? (M i k) ×-dec T? (M k j)) -- All the ways an entry can be set by one closure step. StepHit : Matrix → Fin card → Fin card → Type ρ StepHit M i j = T (M i j) ⊎ T (M j i) ⊎ TransHit M i j ⊎ (∃[ fi ] OpHit M fi i j) stepHit? : ∀ M i j → Dec (StepHit M i j) stepHit? M i j = T? (M i j) ⊎-dec T? (M j i) ⊎-dec transHit? M i j ⊎-dec any? (λ fi → opHit? M fi i j) -- One closure step. step : Matrix → Matrix step M i j = does (stepHit? M i j) -- Reading a stepped bit back as its proposition, and conversely. step-out : ∀ M {i j} → T (step M i j) → StepHit M i j step-out M {i} {j} = does-out (stepHit? M i j) step-in : ∀ M {i j} → StepHit M i j → T (step M i j) step-in M {i} {j} = does-in (stepHit? M i j) -- The step never unsets a bit. step-inflate : ∀ M i j → T (M i j) → T (step M i j) step-inflate M i j p = step-in M (inj₁ p)
The iteration. iterFix n M applies the step up to n times, stopping at
the first fixpoint reached; the fixpoint test is the decidable pointwise
equality matEq?. The mutual helper iterStep
takes the test's outcome as an argument, so that each lemma about the iteration
can follow the same case structure by ordinary pattern matching.
-- Decidable pointwise equality of matrices. MatEq : Matrix → Matrix → Type MatEq M N = ∀ i j → M i j ≡ N i j matEq? : ∀ M N → Dec (MatEq M N) matEq? M N = all? (λ i → all? (λ j → M i j ≟ᵇ N i j)) -- Fuelled iteration of the step, stopping at the first fixpoint. iterFix : ℕ → Matrix → Matrix iterStep : ℕ → (M : Matrix) → Dec (MatEq M (step M)) → Matrix iterFix zero M = M iterFix (suc n) M = iterStep n M (matEq? M (step M)) iterStep n M (yes _) = M iterStep n M (no _) = iterFix n (step M) -- Neither does the iteration unset a bit. iterFix-inflate : ∀ n M i j → T (M i j) → T (iterFix n M i j) iterStep-inflate : ∀ n M (d : Dec (MatEq M (step M))) i j → T (M i j) → T (iterStep n M d i j) iterFix-inflate zero M i j p = p iterFix-inflate (suc n) M i j p = iterStep-inflate n M (matEq? M (step M)) i j p iterStep-inflate n M (yes _) i j p = p iterStep-inflate n M (no _) i j p = iterFix-inflate n (step M) i j (step-inflate M i j p)
Reaching a fixpoint. A non-fixpoint step strictly increases the bit count
(step-strict); the count is bounded by entries; so as soon as
the fuel exceeds the remaining slack the iteration must hit a fixpoint. Run
with fuel suc entries, it always does.
-- A non-fixpoint step strictly increases the count of set bits. step-strict : ∀ M → ¬ MatEq M (step M) → matCount M < matCount (step M) step-strict M ¬eq = let (i₀ , ¬rowi₀) = ¬∀⟶∃¬ card (λ i → ∀ j → M i j ≡ step M i j) (λ i → all? (λ j → M i j ≟ᵇ step M i j)) ¬eq (j₀ , ¬eqij) = ¬∀⟶∃¬ card (λ j → M i₀ j ≡ step M i₀ j) (λ j → M i₀ j ≟ᵇ step M i₀ j) ¬rowi₀ (¬mij , sij) = bit-flip (step-inflate M i₀ j₀) ¬eqij in matCount-strict (step-inflate M) i₀ j₀ ¬mij sij -- With fuel exceeding the remaining slack, the iteration reaches a fixpoint. iterFix-fix : ∀ n M → entries < matCount M + n → MatEq (iterFix n M) (step (iterFix n M)) iterStep-fix : ∀ n M (d : Dec (MatEq M (step M))) → entries < matCount M + suc n → MatEq (iterStep n M d) (step (iterStep n M d)) iterFix-fix zero M lt = ⊥-elim (≤⇒≯ (matCount-bound M) (subst (entries <_) (+-identityʳ _) lt)) iterFix-fix (suc n) M lt = iterStep-fix n M (matEq? M (step M)) lt iterStep-fix n M (yes eq) lt = eq iterStep-fix n M (no ¬eq) lt = iterFix-fix n (step M) lt′ where lt′ : entries < matCount (step M) + n lt′ = <-≤-trans lt (≤-trans (≤-reflexive (+-suc (matCount M) n)) (+-monoˡ-≤ n (step-strict M ¬eq)))
The closure. Iterate from the seed with adequate fuel; record the fixpoint equation and the persistence of seeded bits.
-- The congruence-closure matrix of the presented pairs. closure : Matrix closure = iterFix (suc entries) seed -- The closure is a fixpoint of the step. closure-fix : MatEq closure (step closure) closure-fix = iterFix-fix (suc entries) seed (subst (entries <_) (sym (+-suc (matCount seed) entries)) (s≤s (m≤n+m entries (matCount seed)))) -- Seeded bits persist into the closure. closure-seed : ∀ {i j} → T (seed i j) → T (closure i j) closure-seed {i} {j} p = iterFix-inflate (suc entries) seed i j p
The closure properties of the fixpoint¶
Each congruence-forming rule, read off the seed or the fixpoint equation at
index level: the ≈-diagonal and the presented pairs come from the seed;
symmetry and transitivity from one application of the step at the fixpoint.
-- The closure contains the ≈-diagonal ... closure-diag : ∀ {i j} → enum i ≈ enum j → T (closure i j) closure-diag e = closure-seed (seed-in (inj₁ e)) -- ... and the presented pairs ... closure-base : ∀ {i j} → R (enum i) (enum j) → T (closure i j) closure-base r = closure-seed (seed-in (inj₂ r)) -- ... and is symmetric ... closure-sym : ∀ {i j} → T (closure i j) → T (closure j i) closure-sym {i} {j} p = subst T (sym (closure-fix j i)) (step-in closure (inj₂ (inj₁ p))) -- ... and transitive. closure-trans : ∀ {i j k} → T (closure i j) → T (closure j k) → T (closure i k) closure-trans {i} {j} {k} p q = subst T (sym (closure-fix i k)) (step-in closure (inj₂ (inj₂ (inj₁ (j , p , q)))))
Compatibility is the substantial case. For an enumerated symbol the recipe
is: encode the two carrier tuples as index tuples by tabulate-ing the chosen
indices along the arity enumeration; their componentwise relatedness is the
hypothesis, transported along lookup∘tabulate; the encoded
tuples are pointwise ≈ to the originals by the round trip
arEnum-arIdx, so their images match by the congruence of the
interpretation; hence the compatibility hit fires at the fixpoint. An arbitrary
symbol is then an enumerated one by surjectivity of the symbol enumeration.
-- The closure is compatible with every enumerated operation symbol ... closure-op-enum : (fi : Fin opCard) {u v : ArityOf 𝑆 (opEnum fi) → 𝕌[ 𝑨 ]} → (∀ a → T (closure (idx (u a)) (idx (v a)))) → T (closure (idx ((opEnum fi ^ 𝑨) u)) (idx ((opEnum fi ^ 𝑨) v))) closure-op-enum fi {u} {v} h = subst T (sym (closure-fix I J)) (step-in closure (inj₂ (inj₂ (inj₂ (fi , ophit))))) where f : OperationSymbolsOf 𝑆 f = opEnum fi I J : Fin card I = idx ((f ^ 𝑨) u) J = idx ((f ^ 𝑨) v) -- the index tuples encoding u and v t s : Vec (Fin card) (arCard f) t = tabulate (λ p → idx (u (arEnum f p))) s = tabulate (λ p → idx (v (arEnum f p))) -- they are componentwise related, by the hypothesis rel : allRelated closure t s rel p = subst₂ (λ a b → T (closure a b)) (sym (lookup∘tabulate (λ q → idx (u (arEnum f q))) p)) (sym (lookup∘tabulate (λ q → idx (v (arEnum f q))) p)) (h (arEnum f p)) -- the encoded tuples are pointwise ≈ the originals t≈u : ∀ a → tupleOf f t a ≈ u a t≈u a = subst (λ b → enum b ≈ u a) (sym eq) (idx-≈ (u a)) where eq : lookup t (arIdx f a) ≡ idx (u a) eq = trans (lookup∘tabulate (λ q → idx (u (arEnum f q))) (arIdx f a)) (cong (λ b → idx (u b)) (arEnum-arIdx f a)) s≈v : ∀ a → tupleOf f s a ≈ v a s≈v a = subst (λ b → enum b ≈ v a) (sym eq) (idx-≈ (v a)) where eq : lookup s (arIdx f a) ≡ idx (v a) eq = trans (lookup∘tabulate (λ q → idx (v (arEnum f q))) (arIdx f a)) (cong (λ b → idx (v b)) (arEnum-arIdx f a)) -- hence their images match those of the originals, by congruence of Interp ft≈fu : (f ^ 𝑨) (tupleOf f t) ≈ (f ^ 𝑨) u ft≈fu = Func.cong (Algebra.Interp 𝑨) (refl , t≈u) fs≈fv : (f ^ 𝑨) (tupleOf f s) ≈ (f ^ 𝑨) v fs≈fv = Func.cong (Algebra.Interp 𝑨) (refl , s≈v) -- so the compatibility hit fires at (I , J) ophit : OpHit closure fi I J ophit = lose (∈-allVecs t) (lose (∈-allVecs s) ( rel , ≈trans (idx-≈ ((f ^ 𝑨) u)) (≈sym ft≈fu) , ≈trans (idx-≈ ((f ^ 𝑨) v)) (≈sym fs≈fv) )) -- ... hence with every operation symbol, by surjectivity of the enumeration. -- -- The passage from an enumerated symbol to an arbitrary one transports along -- opEnum-sur by an explicit subst with the named motive OpCompat, not by a -- with-abstraction on opEnum-sur f: `with` normalizes the goal to find the -- occurrences it must abstract, and this goal mentions `closure`, whose -- unfolding (an iterated step on a symbolic matrix) is enormous — large -- enough to exhaust the CI heap budget. The subst keeps every conversion -- check syntactic. private OpCompat : OperationSymbolsOf 𝑆 → Type (𝓥 ⊔ α) OpCompat g = {u v : ArityOf 𝑆 g → 𝕌[ 𝑨 ]} → (∀ a → T (closure (idx (u a)) (idx (v a)))) → T (closure (idx ((g ^ 𝑨) u)) (idx ((g ^ 𝑨) v))) closure-op : (f : OperationSymbolsOf 𝑆) {u v : ArityOf 𝑆 f → 𝕌[ 𝑨 ]} → (∀ a → T (closure (idx (u a)) (idx (v a)))) → T (closure (idx ((f ^ 𝑨) u)) (idx ((f ^ 𝑨) v))) closure-op f = subst OpCompat (proj₂ (opEnum-sur f)) (closure-op-enum (proj₁ (opEnum-sur f)))
The decoded relation is a congruence¶
Decode the closure matrix along the chosen indices. The result is decidable by construction, and the fixpoint properties above make it a congruence.
-- The relation computed by the closure. closureRel : BinaryRel 𝕌[ 𝑨 ] 0ℓ closureRel x y = T (closure (idx x) (idx y)) -- closureRel is reflexive over ≈ ... closureRel-reflexive : ∀ {x y} → x ≈ y → closureRel x y closureRel-reflexive {x} {y} e = closure-diag (≈trans (idx-≈ x) (≈trans e (≈sym (idx-≈ y)))) -- ... symmetric ... closureRel-sym : ∀ {x y} → closureRel x y → closureRel y x closureRel-sym = closure-sym -- ... transitive (the middle indices agree on the nose) ... closureRel-trans : ∀ {x y z} → closureRel x y → closureRel y z → closureRel x z closureRel-trans = closure-trans -- ... and compatible with the basic operations. closureRel-compatible : 𝑨 ∣≈ closureRel closureRel-compatible f h = closure-op f h -- closureRel as a congruence. closureCon : Con 𝑨 0ℓ closureCon = closureRel , mkcon closureRel-reflexive (record { refl = closureRel-reflexive ≈refl ; sym = closureRel-sym ; trans = closureRel-trans }) closureRel-compatible
Soundness¶
Every set bit of the closure is a generated pair: by induction over the
iteration, where each step disjunct maps onto the corresponding rule of
Gen.
-- The soundness invariant of the iteration. Sound : Matrix → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) Sound M = ∀ i j → T (M i j) → GenR (enum i) (enum j) -- The seed is sound: its bits are ≈-pairs or presented pairs. seed-sound : Sound seed seed-sound i j p = handle (seed-out p) where handle : BaseHit i j → GenR (enum i) (enum j) handle (inj₁ e) = rfl e handle (inj₂ r) = base r -- The step preserves soundness: each disjunct is a Gen rule. step-sound : ∀ M → Sound M → Sound (step M) step-sound M s i j p = handle (step-out M p) where handle : StepHit M i j → GenR (enum i) (enum j) handle (inj₁ q) = s i j q handle (inj₂ (inj₁ q)) = symmetric (s j i q) handle (inj₂ (inj₂ (inj₁ (k , q₁ , q₂)))) = transitive (s i k q₁) (s k j q₂) handle (inj₂ (inj₂ (inj₂ (fi , hit)))) = ophandle (satisfied hit) where f : OperationSymbolsOf 𝑆 f = opEnum fi ophandle : (∃[ t ] Any (λ s′ → allRelated M t s′ × (enum i ≈ (f ^ 𝑨) (tupleOf f t)) × (enum j ≈ (f ^ 𝑨) (tupleOf f s′))) (allVecs card (arCard f))) → GenR (enum i) (enum j) ophandle (t , hitt) = let (s′ , rel , ei≈ , ej≈) = satisfied hitt in transitive (rfl ei≈) (transitive (compatible f (λ a → s (lookup t (arIdx f a)) (lookup s′ (arIdx f a)) (rel (arIdx f a)))) (symmetric (rfl ej≈))) -- Soundness persists through the iteration to the closure. iterFix-sound : ∀ n M → Sound M → Sound (iterFix n M) iterStep-sound : ∀ n M (d : Dec (MatEq M (step M))) → Sound M → Sound (iterStep n M d) iterFix-sound zero M s = s iterFix-sound (suc n) M s = iterStep-sound n M (matEq? M (step M)) s iterStep-sound n M (yes _) s = s iterStep-sound n M (no _) s = iterFix-sound n (step M) (step-sound M s) closure-sound : Sound closure closure-sound = iterFix-sound (suc entries) seed seed-sound -- On carrier elements: a computed pair is a generated pair. closureRel-sound : ∀ {x y} → closureRel x y → GenR x y closureRel-sound {x} {y} p = transitive (symmetric (rfl (idx-≈ x))) (transitive (closure-sound (idx x) (idx y) p) (rfl (idx-≈ y)))
Completeness¶
The presented relation is contained in the decoded congruence, so by the congruence generation theorem the whole generated congruence is.
-- The presented relation is contained in closureRel. R⊆closureRel : ∀ {x y} → R x y → closureRel x y R⊆closureRel {x} {y} r = closure-base (mapAny shift r) where shift : ∀ {p} → (x ≈ proj₁ p) × (y ≈ proj₂ p) → (enum (idx x) ≈ proj₁ p) × (enum (idx y) ≈ proj₂ p) shift (x≈a , y≈b) = ≈trans (idx-≈ x) x≈a , ≈trans (idx-≈ y) y≈b -- Completeness: a generated pair is a computed pair (Cg-least at closureCon). GenR⊆closureRel : ∀ {x y} → GenR x y → closureRel x y GenR⊆closureRel = Cg-least closureCon R⊆closureRel
L1: decidability of the generated congruence¶
To decide membership in Cg (fromPairs ps), test one bit of the closure matrix;
soundness and completeness translate the verdict both ways. The upgrade to a
DecCon then lands at the working congruence level, where
Setoid.Congruences.Presented.Basic's reconstruction theorem provides the converse
passage.
-- L1 (presentation decidability): membership in the congruence generated by -- a finite pair list is decidable on a finite finitary algebra. Cg-dec : ∀ x y → Dec (Gen (fromPairs {𝑨 = 𝑨} ps) x y) Cg-dec x y = map′ closureRel-sound GenR⊆closureRel (T? (closure (idx x) (idx y))) -- The congruence generated by a finite pair list, as a decidable congruence -- at the working level. Cg-DecCon : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) Cg-DecCon = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} ps) , Cg-dec
-
Lemma L1 of
docs/notes/flrp-two-layer-congruences.md§ 3. ↩ -
The module is deliberately built from many small named lemmas; the feasibility remark of ADR-008 applies here as well — the computation exists to discharge the decidability theorem, and no claim of practical efficiency is made for running up to
card ²iterations of a sweep over thecard × cardmatrix, each entry of which additionally searches the operation symbols and their arity tuples. ↩ -
The standard library's
toWitnessandfromWitnessstate these throughisYes, which does not reduce definitionally alongside thedoesprojection used throughout this module, so we match on the decision once ourselves.) ↩