Enumeration of Equivalence Relations

 

Title: Enumeration of Equivalence Relations
Author: Emin Karayel
Submission date: 2022-02-04
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.

BibTeX:
@article{Equivalence_Relation_Enumeration-AFP,
  author  = {Emin Karayel},
  title   = {Enumeration of Equivalence Relations},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2022,
  note    = {\url{https://isa-afp.org/entries/Equivalence_Relation_Enumeration.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Card_Equiv_Relations
Used by: Frequency_Moments
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.