Maximum Segment Sum
by Nils Cremer 📧
diff --git a/web/authors/cremer/index.html b/web/authors/cremer/index.html --- a/web/authors/cremer/index.html +++ b/web/authors/cremer/index.html @@ -1,99 +1,99 @@
February 4, 2022
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.
Nils Cremer 📧 with contributions from Tobias Nipkow 🌐
September 29, 2022
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal publications. To cite an entry, please use the preferred citation style.
A development version of the archive is available as well.
ACM: Theory of computation~Design and analysis of algorithms
AMS: Computer science / Algorithms in computer science