The Congruence Closure Algorithm: Foundations, Implementation, and Applications

Introduction

In the landscape of automated reasoning, few problems are as fundamental as determining when two terms are equal. Yet this seemingly simple question—“Are these two things the same?"—lies at the heart of some of the most sophisticated software verification systems ever built. Every time a modern SMT solver proves that a program cannot crash, every time a compiler optimizes away redundant computations, and every time a theorem prover confirms the correctness of a mathematical proof, it is relying on efficient algorithms for equality reasoning.

The congruence closure algorithm is the workhorse that powers this equality reasoning. It provides a way to compute the smallest equivalence relation containing a given set of equalities that is also closed under function application—the property that if two elements are equal, then any function applied to them must also produce equal results.

This article takes you on a journey through the congruence closure algorithm. We’ll build intuition from first principles, work through the formal mechanics, implement key data structures, walk through detailed examples, and explore the real-world systems that depend on this elegant algorithm. By the end, you’ll understand not just how congruence closure works, but why it’s indispensable for modern computational reasoning.

The Problem: Why Equality Matters

Equality in Formal Systems

Consider a simple mathematical theory with a binary function f and constants a, b, c. Suppose we’re given the equalities:

a = b
b = c

Intuitively, we know that a = c follows from transitivity. But now consider the function application:

f(a) = f(b)

This equality holds because a = b and the congruence property tells us that equal inputs to a function must produce equal outputs. Similarly, if we also know f(a) = d, then we can conclude f(b) = d and f(c) = d.

The congruence closure of a set of equalities is the smallest equivalence relation that contains those equalities and is also closed under function application. Computing this closure is exactly what the congruence closure algorithm does.

Why This Matters in Practice

The ability to reason about equality appears everywhere in computational systems:

Program Verification: When verifying that two program expressions always produce the same result, we need to track all equalities implied by assignments, conditional statements, and loop invariants.

SMT Solvers: Modern Satisfiability Modulo Theory solvers handle theories of arithmetic, arrays, bit-vectors, and more. Equality reasoning is the backbone that ties these theories together.

Compiler Optimization: Dead code elimination, constant propagation, and common subexpression elimination all rely on detecting when two computations must produce identical results.

Theorem Proving: In proof assistants like Coq, Isabelle, and Lean, equality reasoning is fundamental to rewriting and simplification.

Without efficient congruence closure computation, these applications would be intractable for real-world problems involving thousands or millions of terms.

Problem Statement

Equality in Equational Theories

Given a set of equalities $E = \{s_1 = t_1, s_2 = t_2, ..., s_n = t_n\}$, we want to determine whether a target equality $u = v$ is entailed by $E$.

┌─────────────────────────────────────────────────────────────────────┐
│                 EQUATIONAL REASONING                                      │
├─────────────────────────────────────────────────────────────────────┤
│                                                                      │
│   Given: E = {f(a,b) = b, a = c, g(x) = x}                        │
│                                                                      │
│   Question: Is g(f(a,c)) = c ?                                      │
│                                                                      │
│   Solution using congruence closure:                                  │
│                                                                      │
│   1. f(a,b) = b  (given)                                           │
│   2. a = c         (given)                                         │
│   3. f(a,c) = f(c,c)  (substitutivity of f)                     │
│   4. f(c,c) = c        (from 1, substituting a=c)                │
│   5. g(f(a,c)) = g(c)    (substitutivity of g)                  │
│   6. g(c) = c           (given g(x) = x)                       │
│   7. Therefore: g(f(a,c)) = c ✓                                  │
│                                                                      │
└─────────────────────────────────────────────────────────────────────┘

Formal Definition

A congruence relation $\approx$ on terms over a signature $\Sigma$ satisfies:

Reflexivity: $t \approx t$
Symmetry: $s \approx t \Rightarrow t \approx s$
Transitivity: $s \approx t, t \approx u \Rightarrow s \approx u$
Congruence: $s_1 \approx t_1, ..., s_n \approx t_n \Rightarrow f(s_1,...,s_n) \approx f(t_1,...,t_n)$

The congruence closure of $E$ is the smallest congruence relation containing $E$.

Core Intuition: Building Mental Models

From Simple Equality to Congruence

Before formalizing, let’s build intuition with a mental model.

Imagine you have a set of boxes, each containing a term. Some boxes are labeled as equal to each other—you can think of them as being connected by a rope. When you connect two boxes with a rope, you’re asserting their equality.

Now, imagine you have a machine that applies functions. If you apply the same function to two connected boxes, the results must also be connected. This is congruence: equal inputs propagate through function applications.

The congruence closure algorithm essentially simulates this process: start with some known equalities, then repeatedly apply the congruence rule until no new equalities can be discovered. The result is the congruence closure—the complete set of equalities implied by your initial assertions.

Here’s a crucial observation that makes the algorithm efficient: terms that are structurally identical should share representation. If we see f(g(a), h(b)) multiple times, we should have one canonical representation in memory.

This sharing is achieved through a data structure called a term graph or dag (directed acyclic graph). Each node represents a term; function applications are nodes with incoming edges to their argument nodes. When two terms become equal, their nodes in the dag become connected—but more on this when we discuss the formal algorithm.

Union-Find Structure

Disjoint Set Union (DSU)

The congruence closure algorithm is efficiently implemented using the Disjoint Set Union (also called Union-Find) data structure.

class UnionFind:
    """Union-Find with path compression and union by rank"""
    
    def __init__(self):
        self.parent = {}  # Maps elements to their parents
        self.rank = {}     # Rank for union by rank
    
    def make_set(self, x):
        """Create a new set containing x"""
        if x not in self.parent:
            self.parent[x] = x
            self.rank[x] = 0
    
    def find(self, x):
        """Find the representative (root) of x's set"""
        if x not in self.parent:
            self.make_set(x)
        
        # Path compression
        if self.parent[x] != x:
            self.parent[x] = self.find(self.parent[x])
        
        return self.parent[x]
    
    def union(self, x, y):
        """Unite the sets containing x and y"""
        root_x = self.find(x)
        root_y = self.find(y)
        
        if root_x == root_y:
            return  # Already in the same set
        
        # Union by rank
        if self.rank[root_x] < self.rank[root_y]:
            self.parent[root_x] = root_y
        elif self.rank[root_x] > self.rank[root_y]:
            self.parent[root_y] = root_x
        else:
            self.parent[root_y] = root_x
            self.rank[root_x] += 1
    
    def connected(self, x, y):
        """Check if x and y are in the same set"""
        return self.find(x) == self.find(y)

Basic Algorithm

Naive Congruence Closure

class CongruenceClosureNaive:
    """Naive implementation of congruence closure"""
    
    def __init__(self, signature):
        self.signature = signature  # Function symbols and arities
        self.uf = UnionFind()
        self.terms = set()
    
    def add_equality(self, s, t):
        """Add equality s = t to the system"""
        self.terms.add(s)
        self.terms.add(t)
        self.uf.make_set(s)
        self.uf.make_set(t)
        
        # Add the direct equality
        self.uf.union(s, t)
        
        # Propagate equality through congruence
        self._propagate()
    
    def _propagate(self):
        """Propagate equalities through function symbols"""
        changed = True
        while changed:
            changed = False
            
            # For each pair of congruent terms
            for s in self.terms:
                for t in self.terms:
                    if self.uf.connected(s, t):
                        # Check if their subterms are also connected
                        for f in self.signature:
                            s_subterms = self._get_subterms(s, f)
                            t_subterms = self._get_subterms(t, f)
                            
                            if self._all_connected(s_subterms, t_subterms):
                                # f(s) = f(t) is implied
                            # This naive approach is inefficient!
    
    def _get_subterms(self, term, func):
        """Get subterms of term at positions where func is applied"""
        # Implementation depends on term representation
        return []
    
    def _all_connected(self, terms1, terms2):
        """Check if all term pairs are connected"""
        return all(
            self.uf.connected(t1, t2) 
            for t1, t2 in zip(terms1, terms2)
        )
    
    def are_equal(self, s, t):
        """Check if s = t is entailed"""
        return self.uf.connected(s, t)

Efficient Algorithm

Optimized Congruence Closure

The efficient version maintains congruence classes and processes terms in a controlled manner.

class CongruenceClosure:
    """
    Efficient congruence closure algorithm.
    Based on the algorithm by Downey, Sethi, and Tarjan.
    """
    
    def __init__(self):
        # Union-Find structure
        self.parent = {}
        self.rank = {}
        
        # Lists for each congruence class
        self.representatives = {}  # root -> list of terms
        
        # Pending merges
        self.pending = []  # List of (term1, term2) pairs to process
    
    def make_set(self, term):
        """Initialize term as a singleton class"""
        if term not in self.parent:
            self.parent[term] = term
            self.rank[term] = 0
            self.representatives[term] = [term]
    
    def find(self, term):
        """Find canonical representative"""
        if term not in self.parent:
            self.make_set(term)
        
        # Path compression
        if self.parent[term] != term:
            self.parent[term] = self.find(self.parent[term])
        
        return self.parent[term]
    
    def union(self, term1, term2):
        """Merge congruence classes of term1 and term2"""
        root1 = self.find(term1)
        root2 = self.find(term2)
        
        if root1 == root2:
            return  # Already equal
        
        # Union by rank
        if self.rank[root1] < self.rank[root2]:
            root1, root2 = root2, root1
        
        self.parent[root2] = root1
        self.rank[root1] += 1
        
        # Merge representative lists
        self.representatives[root1].extend(self.representatives[root2])
        del self.representatives[root2]
        
        # Queue related terms for reprocessing
        self._queue_congruent_terms(root1)
    
    def _queue_congruent_terms(self, root):
        """Find all terms that share subterms with terms in this class"""
        # Implementation for processing
        pass
    
    def add_equalities(self, equalities):
        """
        Add multiple equalities and compute closure.
        
        Args:
            equalities: List of (term1, term2) pairs
        """
        # Initialize all terms
        for s, t in equalities:
            self.make_set(s)
            self.make_set(t)
        
        # Process all equalities
        for s, t in equalities:
            self.union(s, t)
        
        # Propagate until fixed point
        self._propagate()
    
    def _propagate(self):
        """Propagate equalities through congruence"""
        changed = True
        while changed:
            changed = False
            
            # Process representatives
            roots = list(self.representatives.keys())
            
            for root in roots:
                terms = self.representatives[root]
                
                # Check congruence for each function symbol
                for func in get_function_symbols(terms):
                    # Find congruence classes that should be merged
                    to_merge = self._find_congruent_classes(terms, func)
                    
                    # Merge congruent classes
                    for pair in to_merge:
                        old_size = len(self.representatives)
                        self.union(pair[0], pair[1])
                        if len(self.representatives) < old_size:
                            changed = True
    
    def _find_congruent_classes(self, terms, func):
        """Find pairs of congruence classes that are congruent under func"""
        # Group terms by their subterms at func positions
        from collections import defaultdict
        
        buckets = defaultdict(list)
        
        for term in terms:
            subterms = get_subterms_at_function(term, func)
            key = tuple(sorted(subterms))
            buckets[key].append(term)
        
        # Pairs within same bucket are congruent
        pairs = []
        for bucket_terms in buckets.values():
            for i in range(len(bucket_terms)):
                for j in range(i + 1, len(bucket_terms)):
                    pairs.append((bucket_terms[i], bucket_terms[j]))
        
        return pairs
    
    def are_equal(self, term1, term2):
        """Check if term1 = term2 is entailed"""
        return self.find(term1) == self.find(term2)

Example: Computing Closure

Step-by-Step Example

┌─────────────────────────────────────────────────────────────────────┐
│               CONGRUENCE CLOSURE EXAMPLE                                   │
├─────────────────────────────────────────────────────────────────────┤
│                                                                      │
│   Signature: f/2, g/1, a, b, c (constants)                         │
│                                                                      │
│   Input E = {f(a,b) = b, a = c}                                     │
│                                                                      │
│   Step 1: Initialize                                                  │
│   ┌─────────────────────────────────────────────────────────────┐    │
│   │ Terms: {a, b, c, f(a,b)}                                   │    │
│   │ Classes: {a}, {b}, {c}, {f(a,b)}                            │    │
│   └─────────────────────────────────────────────────────────────┘    │
│                                                                      │
│   Step 2: Add a = c                                                  │
│   ┌─────────────────────────────────────────────────────────────┐    │
│   │ Merge: {a, c}                                               │    │
│   │ Classes: {a,c}, {b}, {f(a,b)}                               │    │
│   └─────────────────────────────────────────────────────────────┘    │
│                                                                      │
│   Step 3: Propagate through f                                        │
│   ┌─────────────────────────────────────────────────────────────┐    │
│   │ f(a,b) and f(c,b) have congruent subterms:                 │    │
│   │ a ≈ c and b ≈ b, so f(a,b) ≈ f(c,b)                       │    │
│   │ Merge: {f(a,b), f(c,b)}                                     │    │
│   │ Classes: {a,c}, {b}, {f(a,b), f(c,b)}                      │    │
│   └─────────────────────────────────────────────────────────────┘    │
│                                                                      │
│   Step 4: Given f(a,b) = b                                          │
│   ┌─────────────────────────────────────────────────────────────┐    │
│   │ Merge: {f(a,b), f(c,b)} with {b}                             │    │
│   │ Classes: {a,c,b}, {f(a,b), f(c,b)}                          │    │
│   └─────────────────────────────────────────────────────────────┘    │
│                                                                      │
│   Result: a = b = c and f(a,b) = b                                 │
│                                                                      │
└─────────────────────────────────────────────────────────────────────┘

Python Implementation Example

# Example usage
def example_congruence_closure():
    # Create congruence closure
    cc = CongruenceClosure()
    
    # Add equalities: f(a,b) = b, a = c
    equalities = [
        ('f(a,b)', 'b'),
        ('a', 'c')
    ]
    
    cc.add_equalities(equalities)
    
    # Check queries
    print(f"a = c? {cc.are_equal('a', 'c')}")       # True
    print(f"f(a,b) = b? {cc.are_equal('f(a,b)', 'b')}")  # True
    print(f"f(c,b) = b? {cc.are_equal('f(c,b)', 'b')}")  # True
    print(f"a = f(a,b)? {cc.are_equal('a', 'f(a,b)')}")  # False

example_congruence_closure()

Incremental Algorithm

Maintaining Closure Incrementally

For applications like term rewriting systems, we need to maintain the congruence closure as equalities are added incrementally.

class IncrementalCongruenceClosure:
    """
    Incremental congruence closure algorithm.
    Supports efficient addition of new equalities.
    """
    
    def __init__(self):
        self.parent = {}
        self.rank = {}
        self.representatives = {}
        
        # For incremental processing
        self.merge_queue = []
        self.explored = set()
    
    def add_equality(self, s, t):
        """Add single equality and update closure incrementally"""
        self._ensure_set(s)
        self._ensure_set(t)
        
        # Queue this merge
        self.merge_queue.append((s, t))
        
        # Process until fixed point
        self._process_queue()
    
    def _ensure_set(self, term):
        """Ensure term exists in structure"""
        if term not in self.parent:
            self.parent[term] = term
            self.rank[term] = 0
            self.representatives[term] = [term]
    
    def _process_queue(self):
        """Process merge queue until stable"""
        while self.merge_queue:
            s, t = self.merge_queue.pop(0)
            
            root_s = self.find(s)
            root_t = self.find(t)
            
            if root_s == root_t:
                continue  # Already merged
            
            # Perform merge
            self._merge(root_s, root_t)
            
            # Find new congruences and add to queue
            self._find_new_congruences()
    
    def _merge(self, root1, root2):
        """Merge two equivalence classes"""
        if self.rank[root1] < self.rank[root2]:
            root1, root2 = root2, root1
        
        self.parent[root2] = root1
        self.rank[root1] += 1
        
        # Merge lists
        self.representatives[root1].extend(self.representatives[root2])
        del self.representatives[root2]
    
    def _find_new_congruences(self):
        """Find new congruences after a merge"""
        # Check all function applications
        for root in list(self.representatives.keys()):
            terms = self.representatives[root]
            
            for func in get_function_symbols(terms):
                # Group by subterms
                buckets = group_by_subterms(terms, func)
                
                for bucket_terms in buckets.values():
                    # Merge all terms in same bucket
                    for i in range(len(bucket_terms) - 1):
                        pair = (bucket_terms[i], bucket_terms[i + 1])
                        if pair not in self.explored:
                            self.merge_queue.append(pair)
                            self.explored.add(pair)

Applications

1. Theorem Proving

Congruence closure is fundamental in superposition calculus and equality handling in theorem provers.

% Example: Proving equality in first-order logic
% Given: f(a,b) = b, a = c
% Prove: f(c,b) = b

% The congruence closure quickly determines this is true

2. Equality Saturation

Used in egg (Equality Saturation Graphs) for program optimization.

# Equality saturation pseudo-code
def equality_saturation(program, rules):
    # Start with original program terms
    egraph = EGraph()
    egraph.add_terms(program)
    
    while not egraph.is_saturated():
        # Find applicable rules
        matches = egraph.find_matches(rules)
        
        # Add equalities from rule applications
        for match in matches:
            lhs, rhs = match.apply()
            egraph.add_equality(lhs, rhs)
        
        # Compute congruence closure
        egraph.compute_congruence_closure()
    
    return egraph.extract_best()

3. SMT Solving

SMT solvers use congruence closure for the equality with uninterpreted functions (EUF) theory.

# SMT-LIB pseudo-code
(set-logic QF_UF)  ; Uninterpreted Functions
(declare-const a Int)
(declare-const b Int)
(declare-const f (Array Int Int))

(assert (= (f a) b))
(assert (= a c))
(check-sat)  ; Uses congruence closure to determine sat

4. Symbolic Computation

Used in computer algebra systems for simplifying expressions.

# Symbolic simplification using congruence closure
def simplify(expr, equalities):
    cc = CongruenceClosure()
    cc.add_equalities(equalities)
    
    # Reduce expression using congruence classes
    return cc.reduce(expr)

Complexity Analysis

Time Complexity

Operation	Naive	Optimized
Add equality	O(n²)	O(α(n)) amortized
Query	O(n)	O(α(n))
Full closure	O(n³)	O(n log n)

Where $\alpha(n)$ is the inverse Ackermann function, effectively constant for practical purposes.

Space Complexity

Union-Find: O(n) where n is number of terms
Congruence classes: O(n)

Optimizations

Path Compression

def find(self, x):
    """Find with path compression"""
    if self.parent[x] != x:
        self.parent[x] = self.find(self.parent[x])  # Compress path
    return self.parent[x]

Union by Rank

def union(self, x, y):
    """Union by rank"""
    root_x = self.find(x)
    root_y = self.find(y)
    
    if root_x == root_y:
        return
    
    if self.rank[root_x] < self.rank[root_y]:
        self.parent[root_x] = root_y
    elif self.rank[root_x] > self.rank[root_y]:
        self.parent[root_y] = root_x
    else:
        self.parent[root_y] = root_x
        self.rank[root_x] += 1

Lazy Evaluation

Only compute congruence classes when needed for query answering.

Extensions

Congruence Closure with Theories

Combining congruence closure with background theories (arrays, integers, etc.):

┌─────────────────────────────────────────────────────────────────────┐
│              THEORY COMBINATION                                            │
├─────────────────────────────────────────────────────────────────────┤
│                                                                      │
│   Base: Congruence closure for uninterpreted functions               │
│                                                                      │
│   + Array Theory: a[i] = a[j] if i = j                               │
│   + Integer Theory: x + 0 = x, x + 1 ≠ x                           │
│   + List Theory: nil = nil, cons(x,y) ≠ nil                         │
│                                                                      │
│   Combined via Nelson-Oppen or Shostak algorithms                    │
│                                                                      │
└─────────────────────────────────────────────────────────────────────┘

Conclusion

The congruence closure algorithm is fundamental to:

Automated theorem proving - Efficient equality reasoning
SMT solving - Core component of EUF theory
Program optimization - Equality saturation
Symbolic computation - Expression simplification

Key insights:

Union-Find provides O(α(n)) operations
Congruence propagates through function symbols
Incremental versions support dynamic updates

Understanding this algorithm is essential for anyone working in formal methods, theorem proving, or symbolic AI.