Setoid.Congruences.Presented.Basic

Finitely presented congruences: reconstruction from generating pairs

This is the Setoid.Congruences.Presented.Basic module of the Agda Universal Algebra Library.

A congruence in this library is a Type-valued relation, and on that semantic layer even a two-element carrier has classically-loaded congruences.¹

We adopt a two-layer congruence discipline that builds a decidable layer, whose defining property is reconstructibility from generating pairs: a decidable congruence on a finite carrier is determined by the finite list of enumerated pairs it relates; this module proves that property.²

Concretely, for an algebra 𝑨 with the carrier-finiteness data of Setoid.Algebras.Finite and a decidable congruence d : DecCon 𝑨 ℓ (Setoid.Congruences.Finite.Basic) we define

• fromPairs ps — the binary relation presented by a pair list ps: two elements are related when ps lists a pair to which they are componentwise ≈-equal;
• relatedPairs d — the finite list of d-related pairs of enumerated elements, obtained by filtering all pairs of enumerated elements through d's decision procedure;

We prove the following reconstruction theorem:

proj₁ d ≑ Cg (fromPairs (relatedPairs d))

That is, d is, up to mutual containment, the congruence generated by its own related-pairs list.

One inclusion is the base rule of Cg applied to completeness of the list; the other is Cg-least applied to soundness of the list.³

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Congruences.Presented.Basic where

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Fin.Base                       using  ( Fin )
open import Data.List.Base                      using  ( List ; allFin ; filter
                                                       ; map ; cartesianProduct )
open import Data.List.Membership.Propositional  using  ( _∈_ ; lose )
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.All        using  ( All ; lookupAny )
open import Data.List.Relation.Unary.All.Properties
                                                using  ( all-filter )
open import Data.List.Relation.Unary.Any        using  ( Any ; any? )
open import Data.Product                        using  ( _×_ ; _,_ ; proj₁ ; proj₂ )
open import Level                               using  ( Level ; _⊔_ )
open import Relation.Binary                     using  ( Setoid ; IsEquivalence )
                                                renaming ( Rel to BinaryRel )
open import Relation.Nullary.Decidable          using  ( Dec ; _×-dec_ )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture                         using ( 𝓞 ; 𝓥 ; Signature )
open import Setoid.Algebras.Basic            using  ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite           using  ( FiniteAlgebra )
open import Setoid.Congruences.Basic         using  ( Con ; reflexive ; is-equivalence )
open import Setoid.Congruences.Finite.Basic  using  ( DecCon ; ConRel )
open import Setoid.Congruences.Generation    using  ( Cg ; base ; Cg-least ; _⊑_ )
open import Setoid.Congruences.Lattice       using  ( _≑_ )

private variable α ρ ℓ : Level

The relation presented by a list of pairs

Fix an algebra 𝑨. A pair list ps presents the relation that holds between x and y exactly when some listed pair (a , b) has x ≈ a and y ≈ b — membership in the list, up to ≈ componentwise. Because the relation quantifies existentially over the list (via Any), it is decidable as soon as ≈ is; no other structure is needed.

module _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρ} where
  open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( sym to ≈sym )

  -- The relation presented by a pair list: componentwise ≈-membership.
  fromPairs : List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ]) → BinaryRel 𝕌[ 𝑨 ] (α ⊔ ρ)
  fromPairs ps x y = Any (λ p → x ≈ proj₁ p × y ≈ proj₂ p) ps

  -- The presented relation is decidable whenever ≈ is.
  fromPairs? : (∀ x y → Dec (x ≈ y)) → (ps : List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ]))
    → ∀ x y → Dec (fromPairs ps x y)
  fromPairs? _≟_ ps x y = any? (λ p → x ≟ proj₁ p ×-dec y ≟ proj₂ p) ps

A small helper used repeatedly below: a congruence relates ≈-equal replacements of related elements. This is just reflexivity-over-≈ composed with the equivalence laws, but naming it keeps the proofs legible.

  -- From a θ b infer x θ y for any x ≈ a and y ≈ b.
  con-resp-≈ : ((_θ_ , _) : Con 𝑨 ℓ) {x y a b : 𝕌[ 𝑨 ]}
    → x ≈ a → y ≈ b → a θ b → x θ y

  con-resp-≈ (_ , θcon) x≈a y≈b aθb =
    θtrans (reflexive θcon x≈a) (θtrans aθb (θsym (reflexive θcon y≈b)))
    where
    open IsEquivalence (is-equivalence θcon) using ()
      renaming ( sym to θsym ; trans to θtrans )

The related-pairs list of a decidable congruence

Now fix carrier-finiteness data 𝑭 for 𝑨 (a nested module, so that fromPairs and its consumers share the ambient algebra). The pairs of enumerated elements form a finite list, and a decidable congruence filters it: relatedPairs d keeps exactly the pairs that d's decision procedure accepts.

  module _ (𝑭 : FiniteAlgebra 𝑨) where
    open FiniteAlgebra 𝑭 using ( card ; enum ; enum-sur )

    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)

    -- All pairs of enumerated elements.
    enumPairs : List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ])
    enumPairs = map (λ p → enum (proj₁ p) , enum (proj₂ p))
                    (cartesianProduct (allFin card) (allFin card))

    -- The pairs of enumerated elements related by a decidable congruence.
    relatedPairs : DecCon 𝑨 ℓ → List (𝕌[ 𝑨 ] × 𝕌[ 𝑨 ])
    relatedPairs d = filter (λ p → proj₂ d (proj₁ p) (proj₂ p)) enumPairs

Soundness: every listed pair is d-related — immediately from the filter. Consequently the relation presented by the list is contained in d, using con-resp-≈ to absorb the componentwise ≈-steps.

    -- Every pair on the list is d-related.
    relatedPairs-related : (d : DecCon 𝑨 ℓ)
      →  All (λ p → ConRel d (proj₁ p) (proj₂ p)) (relatedPairs d)
    relatedPairs-related d =
      all-filter (λ p → proj₂ d (proj₁ p) (proj₂ p)) enumPairs

    -- Hence the presented relation of the list is contained in d.
    fromPairs-relatedPairs-⊆ : (d : DecCon 𝑨 ℓ) {x y : 𝕌[ 𝑨 ]}
      →  fromPairs (relatedPairs d) x y → ConRel d x y
    fromPairs-relatedPairs-⊆ d mem =
      let (aθb , x≈a , y≈b) = lookupAny (relatedPairs-related d) mem
      in  con-resp-≈ (proj₁ d) x≈a y≈b aθb

Completeness: every d-related pair is presented by the list. Given x θ y, pass to the enumerated representatives enum (idx x) and enum (idx y): they are θ-related by con-resp-≈, so the pair survives the filter, and x, y are componentwise ≈-equal to it.

    -- Every d-related pair is presented by the list.
    relatedPairs-complete : (d : DecCon 𝑨 ℓ) {x y : 𝕌[ 𝑨 ]}
      →  ConRel d x y → fromPairs (relatedPairs d) x y
    relatedPairs-complete d {x} {y} xθy =
      lose pair∈related (≈sym (idx-≈ x) , ≈sym (idx-≈ y))
      where
      eθe : ConRel d (enum (idx x)) (enum (idx y))
      eθe = con-resp-≈ (proj₁ d) (idx-≈ x) (idx-≈ y) xθy

      pair∈enum : (enum (idx x) , enum (idx y)) ∈ enumPairs
      pair∈enum = ∈-map⁺ (λ p → enum (proj₁ p) , enum (proj₂ p))
                         (∈-cartesianProduct⁺ (∈-allFin (idx x)) (∈-allFin (idx y)))

      pair∈related : (enum (idx x) , enum (idx y)) ∈ relatedPairs d
      pair∈related = ∈-filter⁺ (λ p → proj₂ d (proj₁ p) (proj₂ p)) pair∈enum eθe

The reconstruction theorem (L2)

The two containments between d and the congruence generated by its related-pairs list, at any relation level; then, at the working level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ, their conjunction as an _≑_. Note that Cg (fromPairs (relatedPairs d)) lands at level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ on the nose, because the generation closure absorbs the operation, arity, and carrier levels.

    -- The generated congruence of the list is contained in d ... (via Cg-least)
    Cg-relatedPairs-⊑ : (d : DecCon 𝑨 ℓ) → Cg (fromPairs (relatedPairs d)) ⊑ proj₁ d
    Cg-relatedPairs-⊑ d = Cg-least (proj₁ d) (fromPairs-relatedPairs-⊆ d)

    -- ... and conversely d is contained in it (via the base rule).
    ⊑-Cg-relatedPairs : (d : DecCon 𝑨 ℓ) → proj₁ d ⊑ Cg (fromPairs (relatedPairs d))
    ⊑-Cg-relatedPairs d xθy = base (relatedPairs-complete d xθy)

    -- L2: a decidable congruence at the working level is ≑ to the congruence
    -- generated by its related-pairs list.
    reconstruction : (d : DecCon 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ))
      →  proj₁ d ≑ Cg (fromPairs (relatedPairs d))
    reconstruction d = ⊑-Cg-relatedPairs d , Cg-relatedPairs-⊑ d

---

---

1. Recall the oracle congruences and the "no-go" theorem of FLRP.Problem. ↩

2. See ADR-008 and Lemma L2 of docs/notes/flrp-two-layer-congruences.md § 3. ↩

3. Two scope remarks.

   1. Only carrier finiteness is used — in fact only the card/enum/enum-sur fields; not even the _≟_ field is needed, since d carries its own decision procedure. In particular no FiniteSignature hypothesis appears: signature finiteness enters only for the converse direction of the layer-D programme — that Cg of a finite pair list is again decidable (Lemma L1) — which is the business of Setoid.Congruences.Presented.Decidable.

   2. The containments hold for a DecCon at any relation level and are stated heterogeneously via _⊑_; at the working congruence level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ of Setoid.Congruences.Finite the two sides live at the same level and combine into an honest _≑_.

   ↩