---
layout: default
file: "src/Setoid/Congruences/Certificates/Schema.lagda.md"
title: "Setoid.Congruences.Certificates.Schema module (The Agda Universal Algebra Library)"
date: "2026-07-22"
author: "the agda-algebras development team"
---

### 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](docs/notes/flrp-wp6-freese-certificates.md): 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`{.AgdaDatatype}, `Vec`{.AgdaDatatype},
`List`{.AgdaDatatype}), 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`{.AgdaDatatype} of [Setoid.Congruences.Generation][], which is what the
   checker reconstructs from it.

Throughout, `n`{.AgdaBound} is the carrier enumeration size of the algebra under
discussion, `ops`{.AgdaBound} the operation-symbol enumeration size, and
`ar`{.AgdaBound}` : Fin ops → ℕ` the arity of each enumerated symbol; the checker
instantiates these with `card`{.AgdaField}, `opCard`{.AgdaField}, and
`arCard`{.AgdaFunction}` ∘ `{.AgdaFunction}`opEnum`{.AgdaField} 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.

<!--
```agda
{-# 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 `Fin`{.AgdaDatatype}` n` 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.

```agda
-- 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.

```agda
-- 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.

```agda
-- 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`{.AgdaField},
`rhs`{.AgdaField}) and records *why* the merged pair belongs to the congruence being
generated.

+  `seed s`{.AgdaInductiveConstructor} — the pair is (at position `s` of) the seed
   list `P` of the claim `θ ≑ Cg (fromPairs P)`; the checker turns it into the
   `base`{.AgdaInductiveConstructor} rule of `Gen`{.AgdaDatatype}.
+  `translate f c w r`{.AgdaInductiveConstructor} — 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`{.AgdaInductiveConstructor} 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`{.AgdaInductiveConstructor} position is an *absolute* index into the seed
list, while a `translate`{.AgdaInductiveConstructor} 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.

```agda
-- 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:[^1]

+  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][].

```agda
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:[^1]

+  `parts`{.AgdaField} — the list of all claimed congruences as normal-form parent vectors;

+  `bot`{.AgdaField} — the position of the claimed least congruence (the `≈`-diagonal),
   the base case of the checker's principal-join fold;

+  `prinT`{.AgdaField} — 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`{.AgdaField} (seed list: the one pair);

+  `meetT`{.AgdaField} — the claimed meet table; meets of partitions are pointwise
   root-pair intersections, so the checker verifies each entry definitionally, with
   no trace;

+  `joinT`{.AgdaField} — the claimed join table, each entry justified by a trace in
   `joinTr`{.AgdaField} 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.

```agda
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](docs/notes/flrp-wp6-freese-certificates.md) § 4.