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},
}
|