{"id":955017,"date":"2023-07-12T14:15:10","date_gmt":"2023-07-12T21:15:10","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=955017"},"modified":"2024-05-22T19:44:25","modified_gmt":"2024-05-23T02:44:25","slug":"fiptree-tr","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/fiptree-tr\/","title":{"rendered":"The Functional Essence of Imperative Binary Search Trees"},"content":{"rendered":"
\n
Algorithms on restructuring binary search trees are typically<\/div>\n
presented in imperative pseudocode. Understandably so, as their<\/div>\n
performance relies on in-place execution, rather than the repeated<\/div>\n
allocation of fresh nodes in memory. Unfortunately, these imperative<\/div>\n
algorithms are notoriously difficult to verify as their loop<\/div>\n
invariants must relate the unfinished tree fragments being<\/div>\n
rebalanced.<\/div>\n
<\/div>\n
This paper presents several novel functional algorithms<\/div>\n
for accessing and inserting elements in a restructuring binary search<\/div>\n
tree that are as fast as their imperative counterparts; yet the<\/div>\n
correctness of these functional algorithms is established using a<\/div>\n
simple inductive argument. For each data structure, move-to-root,<\/div>\n
splay, and zip trees, this paper describes both a bottom-up<\/div>\n
algorithm using zippers and a top-down algorithm using a novel<\/div>\n
first-class constructor context primitive.<\/div>\n
<\/div>\n
The functional and imperative algorithms are equivalent:<\/div>\n
we mechanise the proofs establishing this in the Coq<\/div>\n
proof assistant using the Iris framework. This yields a first fully<\/div>\n
verified implementation of well known algorithms on binary search trees with<\/div>\n
performance on par with the fastest implementations in C.<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193718],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[249475,249202],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-955017","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-field-of-study-algorithm-design","msr-field-of-study-programming-language"],"msr_publishername":"","msr_edition":"","msr_affiliation":"","msr_published_date":"2023-7-12","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"MSR-TR-2023-28","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"Microsoft","msr_how_published":"","msr_notes":"v4, Dec 27, 2023 (previously titled \"A Functional Correspondence between Top-down and Bottom-up Tree Algorithms\") This is an extended version of the PLDI'24 publication.","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/07\/fiptree-tr-v4.pdf","id":"995391","title":"fiptree-tr-v4","label_id":"243109","label":0}],"msr_related_uploader":"","msr_attachments":[{"id":995391,"url":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/12\/fiptree-tr-v4.pdf"},{"id":962301,"url":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/08\/fiptree-tr-v3.pdf"},{"id":957564,"url":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/07\/fiptree-tr-v2.pdf"},{"id":957558,"url":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/07\/fiptree-tr-64c57afa485ea.pdf"},{"id":955023,"url":"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2023\/07\/fiptree-tr.pdf"}],"msr-author-ordering":[{"type":"text","value":"Anton Lorenzen","user_id":0,"rest_url":false},{"type":"user_nicename","value":"Daan Leijen","user_id":31497,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=Daan Leijen"},{"type":"text","value":"Wouter Swierstra","user_id":0,"rest_url":false},{"type":"text","value":"Sam Lindley","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[199565],"msr_event":[],"msr_group":[144812],"msr_project":[170943],"publication":[],"video":[],"download":[],"msr_publication_type":"techreport","related_content":{"projects":[{"ID":170943,"post_title":"Koka","post_name":"koka","post_type":"msr-project","post_date":"2012-04-13 08:38:42","post_modified":"2021-06-18 11:46:37","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/","post_excerpt":"Koka is a strongly typed functional-style language with effect types and handlers.","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170943"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/955017"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":6,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/955017\/revisions"}],"predecessor-version":[{"id":995394,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/955017\/revisions\/995394"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=955017"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=955017"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=955017"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=955017"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=955017"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=955017"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=955017"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=955017"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=955017"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=955017"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=955017"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=955017"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=955017"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=955017"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=955017"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=955017"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}