Setoid.Congruences.Certificates.Schema

The congruence-certificate schema (Freese traces)

This is the Setoid.Congruences.Certificates.Schema module of the Agda Universal Algebra Library.

External engines (GAP, UACalc, SAT and model finders) compute congruence lattices of finite algebras far faster than any in-Agda decision procedure, but nothing they report is believed until Agda has re-checked it.

The certificate discipline that makes this possible is fixed in the design note: the engine emits a linear-size witness of each claim, and a checker verifies the witness with no fixpoint iteration and no search.

This module defines the witness data types — the schema — and nothing else: every type below is plain finite index data (Fin, Vec, List), with no algebra, setoid, or congruence in sight.

The checker modules (Setoid.Congruences.Certificates.Congruence and Setoid.Congruences.Certificates.Lattice) connect these data to a concrete finite finitary algebra and prove the soundness theorems.

The schema follows two short works of R. Freese, the algorithms underlying his Universal Algebra Calculator.

• Partition algorithms (1997) — partitions of a finite set represented as union-find forests (parent vectors), with a normal form making equality of partitions a syntactic vector comparison;
• Computing congruences efficiently (the cg2 preprint) — the worklist algorithm for the congruence Cg(a , b) generated by a pair, whose run is an ordered list of justified merges: each merge is a seed pair or the image of an earlier merge under a unary polynomial translate. That list — the Freese trace — is literally a derivation skeleton for the generation datatype Gen of Setoid.Congruences.Generation, which is what the checker reconstructs from it.

Throughout, n is the carrier enumeration size of the algebra under discussion, ops the operation-symbol enumeration size, and ar: Fin ops → ℕ the arity of each enumerated symbol; the checker instantiates these with card, opCard, and arCard∘opEnum of the finiteness interfaces (Setoid.Algebras.Finite, Setoid.Signatures.Finite), so that a certificate literal type-checks against the intended algebra with no residual side conditions.

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

module Setoid.Congruences.Certificates.Schema where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Fin.Base                          using  ( Fin ; _≤_ )
open import Data.Fin.Properties                    using  ( _≟_ ; _≤?_ ; all? )
open import Data.List.Base                         using  ( List ; map ; filter ; allFin )
open import Data.Nat.Base                          using  ( ℕ )
open import Data.Product                           using  ( _×_ ; _,_ )
open import Data.Vec.Base                          using  ( Vec ; lookup )
open import Relation.Binary.PropositionalEquality  using  ( _≡_ )
open import Relation.Nullary.Decidable             using  ( Dec ; ¬? ; _×-dec_ )

Parent vectors and the Freese normal form

A partition of Finn is stored as a parent vector: entry i is the representative (root) of the block of i. Two indices are in the same block exactly when their parents agree, so root lookups decide block membership in constant time — the reading the checker uses throughout.

-- A partition of Fin n as a vector of block representatives.
ParentVec : ℕ → Type
ParentVec n = Vec (Fin n) n

-- The parent (block representative) of an index.
parent : {n : ℕ} → ParentVec n → Fin n → Fin n
parent pv i = lookup pv i

A parent vector is in Freese normal form when every index points directly at its root (the vector is idempotent as a function) and every root is the ≤-least element of its block.

Given idempotence, leastness of roots is equivalent to the vector being decreasing (parent pv i ≤ i): the root of a block is then a member that lower-bounds all members. Normal form is what makes the representation canonical — two normal-form vectors present the same partition exactly when they are equal as vectors — and the checker exploits this to compare claimed congruences syntactically. Both conditions are decidable by a linear sweep.

-- Every index points directly at its root.
IdempotentParent : {n : ℕ} → ParentVec n → Type
IdempotentParent pv = ∀ i → parent pv (parent pv i) ≡ parent pv i

idempotentParent? : {n : ℕ} (pv : ParentVec n) → Dec (IdempotentParent pv)
idempotentParent? pv = all? λ i → parent pv (parent pv i) ≟ parent pv i

-- Every root is the least element of its block (given idempotence).
DecreasingParent : {n : ℕ} → ParentVec n → Type
DecreasingParent pv = ∀ i → parent pv i ≤ i

decreasingParent? : {n : ℕ} (pv : ParentVec n) → Dec (DecreasingParent pv)
decreasingParent? pv = all? λ i → parent pv i ≤? i

-- Freese normal form: idempotent and decreasing.
NormalForm : {n : ℕ} → ParentVec n → Type
NormalForm pv = IdempotentParent pv × DecreasingParent pv

normalForm? : {n : ℕ} (pv : ParentVec n) → Dec (NormalForm pv)
normalForm? pv = idempotentParent? pv ×-dec decreasingParent? pv

Forest edges

The forest edges of a parent vector are the pairs (i , parent pv i) for the non-root indices i — at most n − 1 of them. They generate the partition as an equivalence relation, and in normal form each edge reaches its root in a single step, so the checker can pass between an arbitrary related pair and a pair of edges by one symmetry-and-transitivity detour through the roots. The whole-lattice checker also uses the edge lists of two congruences as the seed list for a claimed join.

-- The (≤ n − 1) forest edges of a parent vector: each non-root with its root.
forestEdges : {n : ℕ} → ParentVec n → List (Fin n × Fin n)
forestEdges {n} pv =
  map (λ i → i , parent pv i) (filter (λ i → ¬? (i ≟ parent pv i)) (allFin n))

Justified merges and Freese traces

One entry of a Freese trace merges the blocks of two indices (lhs, rhs) and records why the merged pair belongs to the congruence being generated.

• seed s — the pair is (at position s of) the seed list P of the claim θ ≑ Cg (fromPairs P); the checker turns it into the base rule of Gen.
• translate f c w r — the pair is the image of the r-th previously merged pair under the unary polynomial translate of the basic operation f that lets coordinate c vary while freezing the remaining coordinates at w; the checker turns it into one compatible rule applied to the earlier merge. The entry of w at position c is dead data (the checker overwrites it with the moving argument); emitters write 0F there by convention.

Reference conventions, fixed here and enforced by the checker's validity predicate: a seed position is an absolute index into the seed list, while a translate reference is a backward offset into the list of merges already processed — 0 is the immediately preceding merge, 1 the one before it, and so on.

Backward offsets are what keep the checker a single structurally recursive fold; the merges processed so far accumulate most-recent-first, and a reference is a positional lookup into that accumulator. An out-of-range position simply fails the checker's (decidable) validity predicate, so an ill-formed certificate is rejected, never mis-read.

-- Why a merged pair belongs to the generated congruence.
data Justification (n ops : ℕ) (ar : Fin ops → ℕ) : Type where
  seed       :  ℕ → Justification n ops ar
  translate  :  (f : Fin ops) → Fin (ar f) → Vec (Fin n) (ar f) → ℕ
                → Justification n ops ar

-- One justified merge: the pair, and why it is in the congruence.
record Merge (n ops : ℕ) (ar : Fin ops → ℕ) : Type where
  constructor mkMerge
  field
    lhs  : Fin n
    rhs  : Fin n
    why  : Justification n ops ar

-- A Freese trace: the ordered list of justified merges of one cg2 run.
Trace : (n ops : ℕ) (ar : Fin ops → ℕ) → Type
Trace n ops ar = List (Merge n ops ar)

The per-congruence certificate

The certificate for a single claim θ ≑ Cg (fromPairs P) consists of the following data:¹

• the seed list P as index pairs,
• the claimed partition as a normal-form parent vector, and
• the Freese trace whose replay generates that partition.

The three checker obligations C1 (trace soundness), C2 (claimed ⊆ generated), and C3 (generated ⊆ claimed) are discharged against exactly these data by Setoid.Congruences.Certificates.Congruence.

record CgCert (n ops : ℕ) (ar : Fin ops → ℕ) : Type where
  constructor mkCgCert
  field
    seeds  : List (Fin n × Fin n)   -- the generating pairs P, as enumeration indices
    part   : ParentVec n            -- the claimed partition, in Freese normal form
    trace  : Trace n ops ar         -- the justified merge list generating it

The whole-lattice certificate

The certificate for a claim about the entire congruence lattice of a finite finitary algebra consists of the following data:¹

• parts — the list of all claimed congruences as normal-form parent vectors;

• bot — the position of the claimed least congruence (the ≈-diagonal), the base case of the checker's principal-join fold;

• prinT — for every carrier index pair (i , j), the position of the claimed principal congruence Cg(enum i , enum j), with its Freese trace in prinTr (seed list: the one pair);

• meetT — the claimed meet table; meets of partitions are pointwise root-pair intersections, so the checker verifies each entry definitionally, with no trace;

• joinT — the claimed join table, each entry justified by a trace in joinTr whose seed list is the concatenation of the two arguments' forest edges.

The engine-side devices that produce these tables quickly (the union-find join and root-pair-hashing meet of Freese's partition note) never appear here; the checker's verification is definitional and per-entry.

record LatticeCert (n ops : ℕ) (ar : Fin ops → ℕ) (m : ℕ) : Type where
  constructor mkLatticeCert
  field
    parts   : Vec (ParentVec n) m             -- all claimed congruences, normal form
    bot     : Fin m                           -- position of the claimed diagonal
    prinT   : Vec (Vec (Fin m) n) n           -- principal-congruence pointers ...
    prinTr  : Vec (Vec (Trace n ops ar) n) n  -- ... and their traces
    meetT   : Vec (Vec (Fin m) m) m           -- claimed meet table (no traces needed)
    joinT   : Vec (Vec (Fin m) m) m           -- claimed join table ...
    joinTr  : Vec (Vec (Trace n ops ar) m) m  -- ... and its traces

  -- The claimed congruence at a list position.
  partAt : Fin m → ParentVec n
  partAt k = lookup parts k

  -- The claimed principal congruence of a carrier index pair, and its trace.
  prin : Fin n → Fin n → Fin m
  prin i j = lookup (lookup prinT i) j

  prinTrace : Fin n → Fin n → Trace n ops ar
  prinTrace i j = lookup (lookup prinTr i) j

  -- The claimed meet and join of two list positions, and the join's trace.
  meet : Fin m → Fin m → Fin m
  meet k l = lookup (lookup meetT k) l

  join : Fin m → Fin m → Fin m
  join k l = lookup (lookup joinT k) l

  joinTrace : Fin m → Fin m → Trace n ops ar
  joinTrace k l = lookup (lookup joinTr k) l

---

---

1. see the design note § 4. ↩↩