{"id":6223,"date":"2018-09-19T17:13:35","date_gmt":"2018-09-19T15:13:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6223"},"modified":"2018-09-19T17:13:35","modified_gmt":"2018-09-19T15:13:35","slug":"resena-proving-tree-algorithms-for-succinct-data-structures","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-proving-tree-algorithms-for-succinct-data-structures\/","title":{"rendered":"Rese\u00f1a: Proving tree algorithms for succinct data structures"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\/\">Coq<\/a> sobre algor\u00edtmica titulado <a href=\"http:\/\/jssst.or.jp\/files\/user\/taikai\/2018\/PPL\/ppl3-3.pdf\">Proving tree algorithms for succinct data structures<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/\">Reynald Affeldt<\/a> (del <a href=\"http:\/\/www.aist.go.jp\/\">National Institute of Advanced Industrial Science and Technology (AIST)<\/a> en Jap\u00f3n),<\/li>\n<li><a href=\"https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/\">Jacques Garrigue<\/a> (de la <a href=\"http:\/\/www.math.nagoya-u.ac.jp\/\">Nagoya University<\/a> en Jap\u00f3n),<\/li>\n<li><a href=\"https:\/\/www.xuanruiqi.com\/\">Xuanrui Qi<\/a> (de la <a href=\"https:\/\/www.cs.tufts.edu\/\">Tufts University<\/a> en EE.UU.) y<\/li>\n<li>Kazunari Tanaka<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq\/SSReflect of two different succinct tree algorithms. One is the Level-Order Unary Degree Sequence (aka LOUDS), which encodes the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.<\/p><\/blockquote>\n<p>El trabajo se ha presentado el 30 de agosto en el <a href=\"https:\/\/jssst2018.wordpress.com\/\">JSSST 2018<\/a> (<i>The 35th Meeting of the Japan Society for Software Science and Technology<\/i>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"https:\/\/github.com\/affeldt-aist\/succinct\">GitHub<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre algor\u00edtmica titulado Proving tree algorithms for succinct data structures. Sus autores son Reynald Affeldt (del National Institute of Advanced Industrial Science and Technology (AIST) en Jap\u00f3n), Jacques Garrigue (de la Nagoya University en Jap\u00f3n), Xuanrui Qi (de la Tufts University en EE.UU.) y Kazunari&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6223"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=6223"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6223\/revisions"}],"predecessor-version":[{"id":6224,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6223\/revisions\/6224"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6223"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6223"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6223"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}