Email Gateway (Sep 23 2024 at 10:13): Email Gateway (Sep 23 2024 at 10:13):From: Manuel Eberl <manuel@pruvisto.org>
Another interesting randomised algorithm in the AFP, including a proof
of the expected running time:
Rabin's Closest Pair of Points Algorithm
by Emin Karayel and Zixuan Fan
Abstract: This entry formalizes Rabin’s randomized algorithm for the
closest pair of points problem with expected linear running time.
Remarkable is that the best-known deterministic algorithms have
super-linear running times. Hence this algorithm is one of the first
known examples of randomized algorithms that outperform deterministic
algorithms. The formalization also introduces a probabilistic time
monad, which builds on the existing deterministic time monad.
https://www.isa-afp.org/entries/Randomized_Closest_Pair.html
Enjoy!
Manuel
Last updated: Jan 04 2025 at 20:18 UTC