Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: An Efficient Generalization of...


view this post on Zulip Email Gateway (Aug 22 2022 at 21:08):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

the AFP has the following new entry.

Enjoy and thanks to Pasquale,
René

An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
by Pasquale Noce

Counting sort is a well-known algorithm that sorts objects of any kind mapped to
integer keys, or else to keys in one-to-one correspondence with some subset of
the integers (e.g. alphabet letters). However, it is suitable for direct use,
viz. not just as a subroutine of another sorting algorithm (e.g. radix sort),
only if the key range is not significantly larger than the number of the objects
to be sorted. This paper describes a tail-recursive generalization of counting
sort making use of a bounded number of counters, suitable for direct use in case
of a large, or even infinite key range of any kind, subject to the only
constraint of being a subset of an arbitrary linear order. After performing a
pen-and-paper analysis of how such algorithm has to be designed to maximize its
efficiency, this paper formalizes the resulting generalized counting sort
(GCsort) algorithm and then formally proves its correctness properties, namely
that (a) the counters' number is maximized never exceeding the fixed upper
bound, (b) objects are conserved, (c) objects get sorted, and (d) the algorithm
is stable.

https://www.isa-afp.org/entries/Generalized_Counting_Sort.html


Last updated: Apr 16 2024 at 08:18 UTC