### Abstract

This entry provides two related verified divide-and-conquer algorithms solving the fundamental Closest Pair of Points problem in Computational Geometry. Functional correctness and the optimal running time of O(n log n) are proved. Executable code is generated which is empirically competitive with handwritten reference implementations.

### License

BSD License

### History

April 14, 2020
  Incorporate Time_Monad of the AFP entry Root_Balanced_Tree.

### Topics

- Computer science/Algorithms/Geometry

### Related publications

- Rau, M., & Nipkow, T. (2020). Verification of Closest Pair of Points Algorithms. Lecture Notes in Computer Science, 341–357. https://doi.org/10.1007/978-3-030-51054-1_20
- Wikipedia

### Session Closest_Pair_Points

- Common
- Closest_Pair
- Closest_Pair_Alternative

### Depends on

- The Akra-Bazzi theorem and the Master theorem
- Root-Balanced Tree

## Cite

×

Closest_Pair_Points-AFP

    @article{Closest_Pair_Points-AFP,
      author  = {Martin Rau and Tobias Nipkow},
      title   = {Closest Pair of Points Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Closest_Pair_Points.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jan 14, 2020 : Isabelle2019