Setoid.Congruences.Finite.Decidable¶
Constructive completeness of the decidable congruence layer¶
This is the Setoid.Congruences.Finite.Decidable module of the Agda Universal Algebra Library.
Setoid.Congruences.Finite.Basic defines the congruence-side finiteness interface
FiniteCongruences, whose complete field asserts that a
finite list of decidable congruences exhausts the whole congruence lattice up to ≑.
That field quantifies over all semantic congruences Con, and the
non-constructivity ("no-go") theorem shows it carries genuine classical content (its
strength sits between weak excluded middle and excluded middle).1
This module supplies the constructive counterpart.2 It builds, from a
FiniteAlgebra (Setoid.Algebras.Finite) and a
FiniteSignature (Setoid.Signatures.Finite) alone, a finite list of
DecCons that is complete for DecCon — every
decidable congruence is ≑ to a listed one — with no classical axiom.
The resulting interface record is FiniteCongruencesᵈ, the
decidable-layer sibling of FiniteCongruences, identical in shape, but
its completeness field completeᵈ quantifies only over
DecCon, which is exactly why it can be proved rather than assumed.
The two records are genuinely distinct interfaces — they differ in the domain of
quantification, DecCon versus Con — and are not
synonyms.3
The construction, and how it reuses slices L1 and L2¶
A DecCon on a finite carrier is determined, up to ≑, by the
card × card grid of its decisions on enumerated
elements: two decidable congruences that agree on enum i , enum j for all indices
are mutually contained, because the enumeration is surjective and congruences
respect ≈. So enumerating all such grids enumerates all decidable congruences up
to ≑. A grid is a Boolean matrix, represented here as a Vec of
Vecs of Bool, and allGrids lists
all 2 ^ (card ²) of them; ∈-allGrids is the completeness of that
enumeration.
Each grid is decoded to a DecCon by generating the congruence of
its kept pairs: decode V = Cg-DecCon (gpairs V), where gpairs V
lists the enumerated pairs the matrix turns on, and Cg-DecCon —
Lemma L1 of Setoid.Congruences.Presented.Decidable — packages the congruence
generated by a finite pair list as a DecCon, already carrying its
own decision procedure.
(In the code decode splits this into a transparent underlying
congruence decodeCon and an abstract decision procedure
decodeDec, so the enormous symbolic congruence-closure term L1's
decider carries is never normalized into a completeness goal — the elaboration-cost
analogue of L1's own with-normalization caution.)
This is a deliberate deviation from the design note's suggested recipe of filtering
the matrices to congruences and decoding each to a raw Boolean-lookup relation:
filtering is unnecessary because Cg of any pair list is already
a congruence, so decoding through Cg-DecCon reuses all of L1's
soundness, completeness, and compatibility work as a black box instead of re-deriving
operation-compatibility for an arbitrary matrix fixpoint.
Completeness is then the reconstruction argument of L2
(Setoid.Congruences.Presented.Basic), specialized to the matrix-derived list: for
a DecCon d, its own grid gridOf d is in allGrids,
and proj₁ d ≑ proj₁ (decode (gridOf d)) holds because the pairs gpairs (gridOf d)
keeps are exactly the d-related enumerated pairs.
The two containments are the base rule of
Cg (d is contained in the generated congruence) and
Cg-least (the generated congruence is contained in d), assembled
from con-resp-≈ of Setoid.Congruences.Presented.Basic exactly as in
reconstruction of L2 — matching gpairs (gridOf d) to relatedPairs d
as lists would require filter/map-fusion lemmas, so we re-run the two-inclusion pattern
of L2 on the matrix-derived list rather than transport its theorem.4
The Layer-D congruence interface¶
FiniteCongruencesᵈ 𝑨 bundles a finite list consᵈ of
decidable congruences with a proof completeᵈ that the list exhausts the
decidable congruences of 𝑨 up to ≑. Contrast with
FiniteCongruences of Setoid.Congruences.Finite.Basic: that record's
complete field ranges over every Con (Layer S, the
classical bridge), whereas completeᵈ ranges only over
DecCon (Layer D), which is what makes it constructively provable
below. The witnessᵈ* projections mirror the witness* helpers of
the semantic record.
record FiniteCongruencesᵈ {𝑆 : Signature 𝓞 𝓥}(𝑨 : Algebra {𝑆 = 𝑆} α ρ) : Type (lsuc (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)) where field -- a finite list of decidable congruences of 𝑨 ... consᵈ : List (DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)) -- ... exhausting the decidable congruences of 𝑨, up to ≑ completeᵈ : ∀ d → Σ[ e ∈ DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) ] (e ∈ consᵈ) × (proj₁ d ≑ proj₁ e) witnessᵈ : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) witnessᵈ = proj₁ ∘ completeᵈ witnessᵈ∈ : ∀ d → witnessᵈ d ∈ consᵈ witnessᵈ∈ = proj₁ ∘ proj₂ ∘ completeᵈ witnessᵈ≑ : ∀ d → proj₁ d ≑ proj₁ (witnessᵈ d) witnessᵈ≑ = proj₂ ∘ proj₂ ∘ completeᵈ
Enumerating vectors over a finite list¶
The matrix enumeration is built from one generic, signature-agnostic tool:
listVecs xs k lists every length-k Vec whose
entries are drawn from the list xs, and ∈-listVecs is its
completeness — a vector all of whose entries occur in xs occurs in the list. This
is the Data.List-analogue of allVecs of
Setoid.Congruences.Presented.Decidable, generalized from allFin
to an arbitrary source list; keeping the entries as honest inductive data (rather
than functions out of Fin) is what lets membership be stated up to
propositional _≡_ with no appeal to function extensionality.
-- All length-k vectors whose entries come from xs. listVecs : {A : Type ℓ} → List A → (k : ℕ) → List (Vec A k) listVecs xs zero = [] ∷ [] listVecs xs (suc k) = concatMap (λ a → map (a ∷_) (listVecs xs k)) xs -- A vector whose every entry occurs in xs occurs in listVecs xs k. ∈-listVecs : {A : Type ℓ}(xs : List A){k : ℕ}(v : Vec A k) → (∀ p → lookup v p ∈ xs) → v ∈ listVecs xs k ∈-listVecs xs [] _ = here refl ∈-listVecs xs {suc k}(a ∷ v) h = ∈-concat⁺′ (∈-map⁺ (a ∷_) (∈-listVecs xs v (λ p → h (suc p)))) (∈-map⁺ (λ b → map (b ∷_) (listVecs xs k)) (h zero))
The source list of a single bit is true ∷ false ∷ [], complete for
Bool.
-- The two Boolean values, as a list ... allBits : List Bool allBits = true ∷ false ∷ [] -- ... which is complete. ∈-allBits : (b : Bool) → b ∈ allBits ∈-allBits true = here refl ∈-allBits false = there (here refl)
The enumeration of decidable congruences¶
Fix a finite finitary algebra: an algebra 𝑨 with carrier-finiteness data 𝑭 and
signature-finiteness data 𝑺. Only card, enum, and
enum-sur of 𝑭 are used directly here; the _≟_ field and
all of 𝑺 enter only through Cg-DecCon.
module _ {𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥}{𝑨 : Algebra {𝑆 = 𝑆} α ρ}(𝑭 : FiniteAlgebra 𝑨)(𝑺 : FiniteSignature 𝑆) where open FiniteAlgebra 𝑭 using ( card ; enum ; enum-sur ) open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( sym to ≈sym ) private -- A chosen enumeration index for each carrier element, and its correctness. idx : 𝕌[ 𝑨 ] → Fin card idx x = proj₁ (enum-sur x) idx-≈ : (x : 𝕌[ 𝑨 ]) → enum (idx x) ≈ x idx-≈ x = proj₂ (enum-sur x)
A grid is a Boolean matrix over the carrier enumeration, stored as a vector of
rows; entryOf V i j reads the (i , j) bit. The enumeration
allGrids lists every grid, and ∈-allGrids is its
completeness, both by two applications of listVecs.
-- Candidate relations, represented as Boolean matrices (rows of bits). Grid : Type Grid = Vec (Vec Bool card) card -- Reading the (i , j) entry of a grid. entryOf : Grid → Fin card → Fin card → Bool entryOf V i j = lookup (lookup V i) j -- All rows, and all grids, with their completeness. allRows : List (Vec Bool card) allRows = listVecs allBits card ∈-allRows : (r : Vec Bool card) → r ∈ allRows ∈-allRows r = ∈-listVecs allBits r (λ p → ∈-allBits (lookup r p)) allGrids : List Grid allGrids = listVecs allRows card ∈-allGrids : (V : Grid) → V ∈ allGrids ∈-allGrids V = ∈-listVecs allRows V (λ i → ∈-allRows (lookup V i))
The grid of a decidable congruence d records the decision of d on each pair
of enumerated elements; entryOf-gridOf reads that bit back, by two
applications of lookup∘tabulate.
-- The grid of d: its decision bit on each enumerated pair. gridOf : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) → Grid gridOf d = tabulate (λ i → tabulate (λ j → does (proj₂ d (enum i) (enum j)))) -- Reading an entry of that grid back as d's decision bit. entryOf-gridOf : ∀ d → (i j : Fin card) → entryOf (gridOf d) i j ≡ does (proj₂ d (enum i) (enum j)) entryOf-gridOf d i j = trans (cong (λ r → lookup r j) (lookup∘tabulate (λ i → tabulate (λ j → does (proj₂ d (enum i) (enum j)))) i)) (lookup∘tabulate (λ j → does (proj₂ d (enum i) (enum j))) j)
Each grid is decoded to a DecCon by generating the congruence of the
enumerated pairs it keeps: gpairs V is the list of those pairs, and
decode V is Cg-DecCon of it. The whole enumeration
allDecCons decodes every grid.
-- All index pairs of the enumeration. idxPairs : List (Fin card × Fin card) idxPairs = cartesianProduct (allFin card) (allFin card) -- The enumerated pairs a grid keeps. gpairs : Grid → List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ]) gpairs V = map (λ p → enum (proj₁ p) , enum (proj₂ p)) (filter (λ p → T? (entryOf V (proj₁ p) (proj₂ p))) idxPairs) -- The underlying congruence of a decoded grid: Cg of its kept pairs. This is -- transparent and closure-free, so `proj₁ (decode V)` reduces cheaply. decodeCon : Grid → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) decodeCon V = Cg {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (gpairs V)) -- Its decision procedure, supplied by Cg-DecCon of L1. It is kept `abstract` -- because it carries the enormous symbolic congruence-closure term -- (`closure`/`iterFix` over the `card ² × card ²` search); were it transparent, -- type-checking `decode V ∈ allDecCons` — which compares whole decoded -- `DecCon` values — would force Agda to normalize it and exhaust the CI budget. -- Blocking the unfolding keeps the decider opaque while leaving the underlying -- congruence `decodeCon` transparent, which is all the completeness proof reads. abstract decodeDec : (V : Grid) → ∀ x y → Dec (proj₁ (decodeCon V) x y) decodeDec V = proj₂ (Cg-DecCon 𝑭 𝑺 (gpairs V)) -- Decoding a grid to the decidable congruence generated by its kept pairs. decode : Grid → DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) decode V = decodeCon V , decodeDec V -- The enumeration of decidable congruences. allDecCons : List (DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ)) allDecCons = map decode allGrids
Completeness of the enumeration¶
For any DecCon d, its decoded grid is on the list and is ≑ to d.
The ≑ is the L2 reconstruction argument, specialized: soundness
(fromGrid⊆d) reads every kept pair as d-related and absorbs the
≈-steps with con-resp-≈, so Cg-least contains the
generated congruence in d (gridCg⊆d); completeness
(d⊆gridCg) sends a d-related pair to its enumerated
representatives, which the grid keeps, so base contains
d in the generated congruence. Because the underlying congruence
decodeCon is transparent, proj₁ (decode (gridOf d)) reduces to
Cg (fromPairs (gpairs (gridOf d))) and the two containments apply on the nose.
-- every enumerated pair d's grid keeps is d-related grid-related : ∀ d → All (λ q → ConRel d (proj₁ q) (proj₂ q)) (gpairs (gridOf d)) grid-related d = map⁺ {P = λ (q₁ , q₂) → ConRel d q₁ q₂} {f = λ (p₁ , p₂) → enum p₁ , enum p₂} (all-map keptRelated (all-filter (λ (p₁ , p₂) → T? (entryOf (gridOf d) p₁ p₂)) idxPairs)) where keptRelated : {(p₁ , p₂) : Fin card × Fin card} → T (entryOf (gridOf d) p₁ p₂) → ConRel d (enum p₁) (enum p₂) keptRelated {(p₁ , p₂)} t = does-out (proj₂ d (enum p₁) (enum p₂)) (subst T (entryOf-gridOf d p₁ p₂) t) -- soundness: the presented relation of the grid list is contained in d fromGrid⊆d : ∀ d → {x y : 𝕌[ 𝑨 ]} → fromPairs {𝑨 = 𝑨} (gpairs (gridOf d)) x y → ConRel d x y fromGrid⊆d d mem = let (aθb , x≈a , y≈b) = lookupAny (grid-related d) mem in con-resp-≈ (proj₁ d) x≈a y≈b aθb -- hence Cg of the grid list is contained in d (via Cg-least) gridCg⊆d : ∀ d → {x y : 𝕌[ 𝑨 ]} → Gen (fromPairs {𝑨 = 𝑨} (gpairs (gridOf d))) x y → ConRel d x y gridCg⊆d d = Cg-least (proj₁ d) (fromGrid⊆d d) -- d is contained in Cg of the grid list (via base) d⊆gridCg : ∀ d → {x y : 𝕌[ 𝑨 ]} → ConRel d x y → Gen {𝑨 = 𝑨} (fromPairs {𝑨 = 𝑨} (gpairs (gridOf d))) x y d⊆gridCg d {x} {y} dxy = base (lose grid-keeps (≈sym (idx-≈ x) , ≈sym (idx-≈ y))) where -- d relates the enumerated representatives of x and y eθe : ConRel d (enum (idx x)) (enum (idx y)) eθe = con-resp-≈ (proj₁ d) (idx-≈ x) (idx-≈ y) dxy -- so d's grid keeps their index pair, which is thus on the grid list kept : T (entryOf (gridOf d) (idx x) (idx y)) kept = subst T (sym (entryOf-gridOf d (idx x) (idx y))) (does-in (proj₂ d (enum (idx x)) (enum (idx y))) eθe) grid-keeps : (enum (idx x) , enum (idx y)) ∈ gpairs (gridOf d) grid-keeps = ∈-map⁺ (λ (p₁ , p₂) → enum p₁ , enum p₂) (∈-filter⁺ (λ (p₁ , p₂) → T? (entryOf (gridOf d) p₁ p₂)) (∈-cartesianProduct⁺ (∈-allFin (idx x)) (∈-allFin (idx y))) kept) -- decoded grid of d is on the enumeration decode∈list : ∀ d → decode (gridOf d) ∈ allDecCons decode∈list d = ∈-map⁺ decode (∈-allGrids (gridOf d)) -- decoded grid of d is ≑ to d: the two containments at Cg of the grid list. -- (proj₁ (decode (gridOf d)) reduces to Cg (fromPairs (gpairs (gridOf d))) since -- decodeCon is transparent, so the two containments apply on the nose.) d≑decode : ∀ d → proj₁ d ≑ proj₁ (decode (gridOf d)) d≑decode d = d⊆gridCg d , gridCg⊆d d -- completeness: decoded grid of d is on the enumeration and is ≑ to d allDecCons-complete : ∀ d → Σ[ e ∈ DecCon 𝑨 _ ] (e ∈ allDecCons) × (proj₁ d ≑ proj₁ e) allDecCons-complete d = decode (gridOf d) , decode∈list d , d≑decode d
The Layer-D witness¶
Assembling the enumeration and its completeness gives the constructive
FiniteCongruencesᵈ witness for any finite finitary algebra, with no
classical assumption. This is the L3 deliverable and the constructive counterpart of
FiniteCongruences; the passage to the semantic completeness of
FiniteCongruences is the separate classical bridge (L4), not derivable
here.
-- L3: a finite finitary algebra has a constructively complete list of decidable congruences. open FiniteCongruencesᵈ FiniteAlgebra→FiniteCongruencesᵈ : {𝑨 : Algebra {𝑆 = 𝑆} α ρ} → FiniteAlgebra 𝑨 → FiniteSignature 𝑆 → FiniteCongruencesᵈ 𝑨 FiniteAlgebra→FiniteCongruencesᵈ 𝑭 𝑺 .consᵈ = allDecCons 𝑭 𝑺 FiniteAlgebra→FiniteCongruencesᵈ 𝑭 𝑺 .completeᵈ = allDecCons-complete 𝑭 𝑺
-
It is the single Layer-S→Layer-D bridge of ADR-008 (
docs/adr/008-two-layer-congruence-discipline.md). ↩ -
first described as Lemma L3 in the design note
docs/notes/flrp-two-layer-congruences.md§ 3. ↩ -
FiniteCongruencesᵈis the working notion the FLRP program quantifies over, whileFiniteCongruencesremains the semantic form, crossed to exactly once through the bridge. ↩ -
As ADR-008 records, the enumeration is exponential and exists to discharge the completeness theorem; in practice the congruence list is supplied by certificates (WP-6), not by running
allGrids. ↩