Email Gateway (Nov 14 2022 at 10:46): Email Gateway (Nov 14 2022 at 10:46):From: Tobias Nipkow <nipkow@in.tum.de>
Combinatorial Enumeration Algorithms
Paul Hofmeier and Emin Karayel
Combinatorial objects have configurations which can be enumerated by algorithms,
but especially for imperative programs, it is difficult to find out if they
produce the correct output and don’t generate duplicates. Therefore, for some of
the most common combinatorial objects, namely n_Sequences, n_Permutations,
n_Subsets, Powerset, Integer_Compositions, Integer_Partitions,
Weak_Integer_Compositions, Derangements and Trees, this entry formalizes
efficient functional programs and verifies their correctness. In addition, it
provides cardinality proofs for those combinatorial objects. Some cardinalities
are verified using the enumeration functions and others are shown using existing
libraries including other AFP entries.
https://www.isa-afp.org/entries/Combinatorial_Enumeration_Algorithms.html
PS More such enumeration algorithms are welcome.
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC