### Abstract

This entry contains a formalization of an algorithm enumerating all equivalence relations on an initial segment of the natural numbers. The approach follows the method described by Stanton and White [5,§ 1.5] using restricted growth functions.

The algorithm internally enumerates restricted growth functions (as lists), whose equivalence kernels then form the equivalence relations. This has the advantage that the representation is compact and lookup of the relation reduces to a list lookup operation.

The algorithm can also be used within a proof and an example application is included, where a sequence of variables is split by the possible partitions they can form.

### License

BSD License

### Topics

- Mathematics/Combinatorics
- Computer science/Algorithms/Mathematical

### Session Equivalence_Relation_Enumeration

- Equivalence_Relation_Enumeration

### Depends on

- Cardinality of Equivalence Relations

### Used by

- Formalization of Randomized Approximation Algorithms for Frequency Moments

### Auto-related entries

- Maximum Segment Sum

## Cite

×

Equivalence_Relation_Enumeration-AFP

    @article{Equivalence_Relation_Enumeration-AFP,
      author  = {Emin Karayel},
      title   = {Enumeration of Equivalence Relations},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Equivalence_Relation_Enumeration.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 6, 2022 : Isabelle2021-1