---
layout: default
file: "src/Setoid/Congruences/Presented/Decidable.lagda.md"
title: "Setoid.Congruences.Presented.Decidable module (The Agda Universal Algebra Library)"
date: "2026-07-12"
author: "the agda-algebras development team"
---
### 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`{.AgdaFunction}.
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`{.AgdaRecord} ([Setoid.Algebras.Finite][]) *and*
+ the signature data `FiniteSignature`{.AgdaRecord} ([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)` when `enum i ≈ enum j` or the pair is
presented by `ps` — both decidable, by `_≟_`{.AgdaField} and
`fromPairs?`{.AgdaFunction}.
+ **Closure**. One *closure step* sets `(i , j)` when it was already set, or its
transpose was set (symmetry), or some `k` has `(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 tuples `allVecs`{.AgdaFunction}.
+ **Iteration**. The step is *iterated* `card ² + 1` times, stopping early at the
first fixpoint (`iterFix`{.AgdaFunction}). A non-fixpoint step strictly increases
the number of set bits (`matCount`{.AgdaFunction}), which is bounded by `card ²`,
so the fuel suffices and the result `closure`{.AgdaFunction} is a fixpoint of the
step — the pigeonhole argument is carried by the small counting lemmas `bit-*`,
`rowCount-*`, `matCount-*` below.
**Soundness** (`closure-sound`{.AgdaFunction}). Every set bit of the closure
witnesses a genuine derivation in the generation datatype `Gen`{.AgdaDatatype} of
[Setoid.Congruences.Generation][] — by induction over the iteration, each step
disjunct mapping to the corresponding rule of `Gen`{.AgdaDatatype}.
**Completeness** (`GenR⊆closureRel`{.AgdaFunction}). Decoding the fixpoint matrix
along chosen enumeration indices yields a relation `closureRel`{.AgdaFunction} 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`{.AgdaFunction})
the generated congruence is therefore contained in `closureRel`{.AgdaFunction}.
Soundness and completeness together give the decision procedure
`Cg-dec`{.AgdaFunction}: to decide `Gen (fromPairs ps) x y`, test one bit of the
closure matrix. `Cg-DecCon`{.AgdaFunction} packages the result as a
`DecCon`{.AgdaFunction} at the working congruence level `𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ` of
[Setoid.Congruences.Finite.Basic][].[^2]
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Setoid.Congruences.Presented.Decidable where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Bool.Base using ( Bool ; true ; false ; T )
open import Data.Bool.Properties using () renaming ( _≟_ to _≟ᵇ_ )
open import Data.Empty using ( ⊥-elim )
open import Data.Fin.Base using ( Fin ; zero ; suc )
open import Data.Fin.Properties using ( any? ; all? ; ¬∀⟶∃¬ )
open import Data.List.Base using ( List ; [] ; _∷_ ; map ; concatMap ; allFin )
open import Data.Nat.Base using ( ℕ ; zero ; suc ; _+_ ; _*_
; _≤_ ; _<_ ; z≤n ; s≤s )
open import Data.Nat.Properties using ( ≤-trans ; ≤-reflexive ; ≤⇒≯ ; m≤n+m
; +-suc ; +-identityʳ ; +-mono-≤ ; <-≤-trans
; +-mono-<-≤ ; +-mono-≤-< ; +-monoˡ-≤ )
open import Data.Product using ( _×_ ; _,_ ; proj₁ ; proj₂ ; ∃-syntax )
open import Data.Sum.Base using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Unit.Base using ( tt )
open import Data.Vec.Base using ( Vec ; [] ; _∷_ ; lookup ; tabulate )
open import Data.Vec.Properties using ( lookup∘tabulate )
open import Function using ( _∘_ ; Func )
open import Level using ( Level ; 0ℓ ; _⊔_ )
open import Relation.Binary using ( Setoid )
renaming ( Rel to BinaryRel )
open import Relation.Nullary using ( ¬_ ; ofʸ ; ofⁿ )
open import Relation.Nullary.Decidable using ( Dec ; yes ; no ; _because_ ; does ; map′
; T? ; _⊎-dec_ ; _×-dec_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong
; _≢_ ; trans ; subst ; subst₂ )
open import Data.List.Membership.Propositional using ( _∈_ ; lose )
open import Data.List.Relation.Unary.Any using ( Any ; here ; satisfied )
renaming ( any? to anyL? ; map to mapAny )
open import Data.List.Membership.Propositional.Properties
using ( ∈-allFin ; ∈-map⁺ ; ∈-concat⁺′ )
open import Overture using ( 𝓞 ; 𝓥 ; Signature ; ArityOf
; OperationSymbolsOf )
open import Setoid.Algebras.Basic using ( Algebra ; 𝕌[_] ; 𝔻[_] ; _^_ )
open import Setoid.Algebras.Finite using ( FiniteAlgebra )
open import Setoid.Congruences.Basic using ( Con ; mkcon ; _∣≈_ )
open import Setoid.Congruences.Finite.Basic using ( DecCon )
open import Setoid.Congruences.Generation using ( Gen ; Cg ; base ; rfl ; symmetric
; transitive ; compatible ; Cg-least )
open import Setoid.Congruences.Presented.Basic using ( fromPairs ; fromPairs? )
open import Setoid.Signatures.Finite using ( FiniteSignature )
private variable α ρ : Level
```
-->
#### 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 `_+_`.
```agda
bit : Bool → ℕ
bit true = 1
bit false = 0
bit-bound : (b : Bool) → bit b ≤ 1
bit-bound true = s≤s z≤n
bit-bound false = z≤n
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
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)
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 `does`{.AgdaField} bit and the decided
proposition.[^3]
```agda
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 _) ()
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.
```agda
rowCount : {n : ℕ} → (Fin n → Bool) → ℕ
rowCount {zero} g = 0
rowCount {suc n} g = bit (g zero) + rowCount (g ∘ suc)
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))
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)))
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.
```agda
matCount : {m n : ℕ} → (Fin m → Fin n → Bool) → ℕ
matCount {zero} M = 0
matCount {suc m} M = rowCount (M zero) + matCount (M ∘ suc)
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))
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)))
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`{.AgdaDatatype}, and `allVecs n k` lists all `n ^ k` of them;
`∈-allVecs`{.AgdaFunction} is the completeness of that enumeration, which the
compatibility proof uses to inject a concrete tuple into the search space.
```agda
allVecs : (n k : ℕ) → List (Vec (Fin n) k)
allVecs n zero = [] ∷ []
allVecs n (suc k) = concatMap (λ i → map (i ∷_) (allVecs n k)) (allFin n)
∈-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.
```agda
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
R : BinaryRel 𝕌[ 𝑨 ] (α ⊔ ρ)
R = fromPairs {𝑨 = 𝑨} ps
R? : ∀ x y → Dec (R x y)
R? = fromPairs? {𝑨 = 𝑨} _≟_ ps
GenR : BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
GenR = Gen {𝑨 = 𝑨} R
idx : 𝕌[ 𝑨 ] → Fin card
idx x = enum-sur x .proj₁
idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x
idx-≈ x = enum-sur x .proj₂
Matrix : Type
Matrix = Fin card → Fin card → Bool
entries : ℕ
entries = card * card
```
**The seed**. Entry `(i , j)` starts set when the enumerated pair is `≈`-equal
or presented.
```agda
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)
private
seed : Matrix
seed i j = does (baseHit? i j)
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.
```agda
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)))
tupleOf : (f : OperationSymbolsOf 𝑆)
→ Vec (Fin card) (arCard f) → (ArityOf 𝑆 f → 𝕌[ 𝑨 ])
tupleOf f t a = enum (lookup t (arIdx f a))
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
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))
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)
step : Matrix → Matrix
step M i j = does (stepHit? M i j)
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)
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?`{.AgdaFunction}. The mutual helper `iterStep`{.AgdaFunction}
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.
```agda
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))
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)
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`{.AgdaFunction}); 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.
```agda
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
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.
```agda
closure : Matrix
closure = iterFix (suc entries) seed
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))))
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.
```agda
closure-diag : ∀ {i j} → enum i ≈ enum j → T (closure i j)
closure-diag e = closure-seed (seed-in (inj₁ e))
closure-base : ∀ {i j} → R (enum i) (enum j) → T (closure i j)
closure-base r = closure-seed (seed-in (inj₂ r))
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)))
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`{.AgdaFunction}; the encoded
tuples are pointwise `≈` to the originals by the round trip
`arEnum-arIdx`{.AgdaFunction}, 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.
```agda
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)
t s : Vec (Fin card) (arCard f)
t = tabulate (λ p → idx (u (arEnum f p)))
s = tabulate (λ p → idx (v (arEnum f p)))
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))
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))
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)
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) ))
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.
```agda
closureRel : BinaryRel 𝕌[ 𝑨 ] 0ℓ
closureRel x y = T (closure (idx x) (idx y))
closureRel-reflexive : ∀ {x y} → x ≈ y → closureRel x y
closureRel-reflexive {x} {y} e =
closure-diag (≈trans (idx-≈ x) (≈trans e (≈sym (idx-≈ y))))
closureRel-sym : ∀ {x y} → closureRel x y → closureRel y x
closureRel-sym = closure-sym
closureRel-trans : ∀ {x y z} → closureRel x y → closureRel y z → closureRel x z
closureRel-trans = closure-trans
closureRel-compatible : 𝑨 ∣≈ closureRel
closureRel-compatible f h = closure-op f h
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`{.AgdaDatatype}.
```agda
Sound : Matrix → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
Sound M = ∀ i j → T (M i j) → GenR (enum i) (enum j)
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
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≈)))
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
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.
```agda
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
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`{.AgdaFunction} then lands at the working congruence level, where
[Setoid.Congruences.Presented.Basic][]'s reconstruction theorem provides the converse
passage.
```agda
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)))
Cg-DecCon : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)
Cg-DecCon = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} ps) , Cg-dec
```
--------------------------------------
[^1]: Lemma L1 of `docs/notes/flrp-two-layer-congruences.md` § 3.
[^2]: 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 the `card × card` matrix, each entry of which
additionally searches the operation symbols and their arity tuples.
[^3]: The standard library's `toWitness`{.AgdaFunction} and
`fromWitness`{.AgdaFunction} state these through `isYes`{.AgdaFunction}, which
does not reduce definitionally alongside the `does`{.AgdaField} projection used
throughout this module, so we match on the decision once ourselves.)