{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:34Z","timestamp":1779836734474,"version":"3.53.1"},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2011,5,27]],"date-time":"2011-05-27T00:00:00Z","timestamp":1306454400000},"content-version":"unspecified","delay-in-days":26,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2011,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1017\/s0956796811000104","type":"journal-article","created":{"date-parts":[[2011,5,27]],"date-time":"2011-05-27T07:18:17Z","timestamp":1306480697000},"page":"287-307","source":"Crossref","is-referenced-by-count":9,"title":["Balancing weight-balanced trees"],"prefix":"10.1017","volume":"21","author":[{"given":"YOICHI","family":"HIRAI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KAZUHIKO","family":"YAMAMOTO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2011,5,27]]},"reference":[{"key":"S0956796811000104_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_26"},{"key":"S0956796811000104_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_39"},{"key":"S0956796811000104_ref11","unstructured":"Marlow S. , (2010) Haskell 2010 Language Report, Marlow S. (ed), Available online http:\/\/www.haskell.org\/ (May 2011)."},{"key":"S0956796811000104_ref6","volume-title":"Proceedings of the 15th International Conference on Functional Programming (ICFP)","author":"Chargu\u00e9raud","year":"2010"},{"key":"S0956796811000104_ref1","unstructured":"Adams S. (1992) Implementing sets efficiently in a functional language, Technical report CSTR 92-10. University of Southampton."},{"key":"S0956796811000104_ref10","volume-title":"The Art of Computer Programming: Sorting and Searching","author":"Knuth","year":"1998"},{"key":"S0956796811000104_ref5","doi-asserted-by":"publisher","DOI":"10.1080\/10556789908805765"},{"key":"S0956796811000104_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796811000104_ref7","volume-title":"Proceedings. of the Fifth International Conference on Functional Programming (ICFP)","author":"Claessen","year":"2000"},{"key":"S0956796811000104_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000885"},{"key":"S0956796811000104_ref12","first-page":"137","volume-title":"Proceedings of the Fourth Annual Acm Symposium on Theory of Computing","author":"Nievergelt","year":"1972"},{"key":"S0956796811000104_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1978.3"},{"key":"S0956796811000104_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"S0956796811000104_ref14","volume-title":"Proceedings. of the 1991 ACM\/IEEE Conference on Supercomputing","author":"Pugh","year":"1991"},{"key":"S0956796811000104_ref3","first-page":"263","article-title":"An algorithm for the organization of information","volume":"146","author":"Adel'son-Vel'skii","year":"1962","journal-title":"Dokl. Akad. Nauk SSSR"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796811000104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:01Z","timestamp":1779834961000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796811000104\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5]]},"references-count":15,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["S0956796811000104"],"URL":"https:\/\/doi.org\/10.1017\/s0956796811000104","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5]]}}}