赤黒木 (Red-Black Tree) を実装したい

やること

• 赤黒木の実装理解
• Lean の勉強
• 赤黒木を Lean で実装して証明
• Rust でも実装
  • Box や Rc のパターンマッチが厳しそう
• OCaml で実装してみる

参考

• Chris Okasaki. 1999. Red-black trees in a functional setting. J. Funct. Program. 9, 4 (July 1999), 471–477. https://doi.org/10.1017/S0956796899003494
  • 永続赤黒木
  • 純粋関数型
  • 証明との相性がいい
• https://softwarefoundations.cis.upenn.edu/vfa-current/Redblack.html
  • Software Foundations Volume 3: Verified Functional Algorithms
  • Okasaki のアルゴリズムで insert を実装
  • Rocq (Coq) で証明
• Lean
• https://www.geeksforgeeks.org/dsa/introduction-to-red-black-tree/

その他

• https://matt.might.net/articles/red-black-delete/
• Stefan Kahrs. 2001. Red-black trees with types. J. Funct. Program. 11, 4 (July 2001), 425–432. https://doi.org/10.1017/S0956796801004026