Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-24T04:47:32.528Z Has data issue: false hasContentIssue false
  • English
  • Français

Balancing weight-balanced trees

Part of: JFP Research Articles

Published online by Cambridge University Press:  27 May 2011

YOICHI HIRAI  and
KAZUHIKO YAMAMOTO
YOICHI HIRAI
Affiliation:
The University of Tokyo, JSPS Research Fellow (e-mail: [email protected])
KAZUHIKO YAMAMOTO
Affiliation:
IIJ Innovation Institute Inc. (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

A weight-balanced tree (WBT) is a binary search tree, whose balance is based on the sizes of the subtrees in each node. Although purely functional implementations on a variant WBT algorithm are widely used in functional programming languages, many existing implementations do not maintain balance after deletion in some cases. The difficulty lies in choosing a valid pair of rotation parameters: one for standard balance and the other for choosing single or double rotation. This paper identifies the exact valid range of the rotation parameters for insertion and deletion in the original WBT algorithm where one and only one integer solution exists. Soundness of the range is proved using a proof assistant Coq. Completeness is proved using effective algorithms generating counterexample trees. For two specific parameter pairs, we also proved in Coq that set operations also maintain balance. Since the difference between the original WBT and the variant WBT is small, it is easy to change the existing buggy implementations based on the variant WBT to the certified original WBT with a rational solution.

Type
Articles
Information
Journal of Functional Programming , Volume 21 , Issue 3 , May 2011 , pp. 287 - 307
Copyright
Copyright © Cambridge University Press 2011

References

Adams, S. (1992) Implementing sets efficiently in a functional language, Technical report CSTR 92-10. University of Southampton.Google Scholar
Adams, S. (1993) Efficient sets: A balancing act. J. Funct. Program., 3 (4), 553–562.CrossRefGoogle Scholar
Adel'son-Vel'skii, G. M. & Landis, E. M. (1962) An algorithm for the organization of information. Dokl. Akad. Nauk SSSR, 146 (2), 263–266.Google Scholar
Bertot, Y. & Casteran, P. (2004) Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer.CrossRefGoogle Scholar
Borchers, B. (1999) CSDP, a c library for semidefinite programming. Optim. Methods Softw., 11 (1), 613–623.CrossRefGoogle Scholar
Charguéraud, A. (2010) Program verification through characteristic formulae. In Proceedings of the 15th International Conference on Functional Programming (ICFP). ACM.Google Scholar
Claessen, K. & Hughes, J. (2000) QuickCheck: A lightweight tool for random testing of haskell programs. In Proceedings. of the Fifth International Conference on Functional Programming (ICFP). ACM.Google Scholar
Filliâtre, J.-C. & Letouzey, P. (2004) Functors for proofs and programs. In Programming Languages and Systems, Schmidt, D. (ed), Lecture Notes in Computer Science, vol. 2986. Springer, pp. 370–384.CrossRefGoogle Scholar
Guibas, L. J. & Sedgewick, R. (1978) A dichromatic framework for balanced trees. In Proceedings of the 19th Annual Symposium on Foundations of Computer Science (SFCS '78). IEEE, pp. 8–21.CrossRefGoogle Scholar
Knuth, D. E. (1998) The Art of Computer Programming: Sorting and Searching. 2nd ed., vol. 3. Addison-Wesley.Google Scholar
Marlow, S. et al. , (2010) Haskell 2010 Language Report, Marlow, S. (ed), Available online http://www.haskell.org/ (May 2011).Google Scholar
Nievergelt, J. & Reingold, E. M. (1972) Binary search trees of bounded balance. In Proceedings of the Fourth Annual Acm Symposium on Theory of Computing. ACM, pp. 137–142.Google Scholar
Okasaki, C. (1998) Purely Functional Data Structures. Cambridge University Pres.CrossRefGoogle Scholar
Pugh, W. (1991) The Omega test: A fast and practical integer programming algorithm for dependence analysis. In Proceedings. of the 1991 ACM/IEEE Conference on Supercomputing. ACM.Google Scholar
Roura, S. (2001) A new method for balancing binary search trees. In Automata, Languages and Programming, Orejas, F., Spirakis, P. & van Leeuwen, J. (eds), Lecture Notes in Computer Science, vol. 2076. Springer, pp. 469–480.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.