Document Open Access Logo

Verification of the Garsia-Wachs Algorithm

Author Makoto Kanazawa

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.13.pdf
  • Filesize: 1.1 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Garsia-Wachs algorithm
  • Dafny

Metrics

Abstract

The Garsia-Wachs algorithm is an algorithm for finding a leaf-labeled binary tree whose leaf sequence exactly matches the input weight sequence and whose cost is as small as possible, where the cost is the sum of the weights labeling the leaves multiplied by their levels. The algorithm, along with a proof of correctness due to Kingston, is presented in Knuth’s The Art of Computer Programming, Vol. 3. The algorithm comes in two versions, the naive and the optimized. Both versions have quadratic time complexity, but the optimized version can be fine-tuned with a suitable data structure to yield an O(n log n)-time algorithm. I implement and verify a variant of each version of the algorithm in the verification-aware programming language Dafny. Unlike all previous presentations of the algorithm, these variants construct the desired optimum tree directly, without detour through a "nonalphabetic" tree whose leaf sequence is a rearrangement of the input sequence.

Cite As Get BibTex

Makoto Kanazawa. Verification of the Garsia-Wachs Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.13

Author Details

Makoto Kanazawa
  • Department of Advanced Sciences, Faculty of Science and Engineering, Hosei University, Tokyo, Japan

Supplementary Materials

References

  1. G. M. Adel’son-Vel’skiĭ and E. M. Landis. An algorithm for the organisation of information. Doklady Akadamii Nauk SSSR, 146:263-266, 1962. In Russian. English translation in Soviet Math. Doklady, 3:1259-1263, 1962. Google Scholar
  2. Richard Bird and Jeremy Gibbons. Algorithm Design with Haskell. Cambridge University Press, Cambridge, 2020. URL: https://doi.org/10.1017/9781108869041.
  3. Richard S. Bird. An optimal, purely functional implementation of the Garsia-Wachs algorithm. Journal of Functional Programming, 30:e3, 2020. URL: https://doi.org/10.1017/S0956796819000194.
  4. The dafny-lang community. Dafny Reference Manual, 2025. URL: https://dafny.org/latest/DafnyRef/DafnyRef.
  5. Jean-Christophe Filliâtre. A functional implementation of the Garsia-Wachs algorithm (functional pearl). In Proceedings of the 2008 ACM SIGPLAN Workshop on ML, ML '08, pages 91-96, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1411304.1411317.
  6. Adriano M. Garsia and Michelle L. Wachs. A new algorithm for minimum cost binary trees. SIAM Journal on Computing, 6(4):622-642, 1977. URL: https://doi.org/10.1137/0206045.
  7. E. N. Gilbert and E. F. Moore. Variable-length binary encodings. The Bell System Technical Journal, 38(4):933-967, 1959. URL: https://doi.org/10.1002/j.1538-7305.1959.tb01583.x.
  8. T. C. Hu and M. T. Shing. Combinatorial Algorithms: Enlarged Second Edition. Dover Publications, Mineola, N.Y., 2002. Google Scholar
  9. Marek Karpinski, Lawrence L. Larmore, and Wojciech Rytter. Correctness of constructing optimal alphabetic trees revisited. Theoretical Computer Science, 180(1):309-324, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00296-4.
  10. Jeffrey H. Kingston. A new proof of the Garsia-Wachs algorithm. Journal of Algorithms, 9(1):129-136, 1988. URL: https://doi.org/10.1016/0196-6774(88)90009-0.
  11. Donald E. Knuth. The Art of Computer Programming, Volume 3: Sorting and Searching. Addison-Wesley, Reading, Mass., 2nd edition, 1998. Seventh digital release, September 2025. Google Scholar
  12. Donald E. Knuth. GARSIA-WACHS: Simple implementation of Algorithm 6.2.2G, 2004. Accessed 2026-02-11. URL: https://cs.stanford.edu/~knuth/programs/garsia-wachs.w.
  13. Donald E. Knuth. Earliest errata for Volume 3 (2nd ed.), 2011. URL: https://www-cs-faculty.stanford.edu/~knuth/all3-prepre.ps.gz.
  14. The Lean Language Reference, GetElem. Accessed 2026-02-11. URL: https://lean-lang.org/doc/reference/4.27.0/Type-Classes/Basic-Classes/#GetElem___mk.
  15. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 348-370, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  16. K. Rustan M. Leino. Program Proofs. MIT Press, Cambridge, Mass., USA, 2023. Google Scholar
  17. Wojciech Rytter. Trees with minimum weighted path length. In Dinesh P. Mehta and Sartaj Sahni, editors, Handbook of Data Structures and Applications, pages 215-232. CRC Press, second edition, 2018. Google Scholar
  18. Aaron Tomb and Jean-Baptiste Tristan. Avoiding verification brittleness in Dafny, 2023. URL: https://dafny.org/blog/2023/12/01/avoiding-verification-brittleness/.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact