### Abstract

This entry provides a formalization of multidimensional binary trees, also known as k-d trees. It includes a balanced build algorithm as well as the nearest neighbor algorithm and the range search algorithm. It is based on the papers Multidimensional binary search trees used for associative searching and An Algorithm for Finding Best Matches in Logarithmic Expected Time.

### License

BSD License

### History

April 15, 2020
  Change representation of k-dimensional points from 'list' to HOL-Analysis.Finite_Cartesian_Product 'vec'. Update proofs to incorporate HOL-Analysis 'dist' and 'cbox' primitives.

### Topics

- Computer science/Data structures

### Session KD_Tree

- KD_Tree
- Build
- Range_Search
- Nearest_Neighbors

### Depends on

- The Median-of-Medians Selection Algorithm

## Cite

×

KD_Tree-AFP

    @article{KD_Tree-AFP,
      author  = {Martin Rau},
      title   = {Multidimensional Binary Search Trees},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/KD_Tree.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
- Jun 11, 2019 : Isabelle2019
- Jun 4, 2019 : Isabelle2018