{"id":4973,"date":"2015-08-19T06:49:10","date_gmt":"2015-08-19T04:49:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4973"},"modified":"2015-08-19T06:49:10","modified_gmt":"2015-08-19T04:49:10","slug":"resena-formal-study-of-functional-orbits-in-finite-domains","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-study-of-functional-orbits-in-finite-domains\/","title":{"rendered":"Rese\u00f1a: Formal study of functional orbits in finite domains"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\">Coq<\/a> titulado <a href=\"http:\/\/\/icube-publis.unistra.fr\/docs\/8330\/Orbits14FV.pdf\">Formal study of functional orbits in finite domains<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/dpt-info.u-strasbg.fr\/~jfd\">Jean-Fran\u00e7ois Dufourd<\/a> (del grupo <a href=\"http:\/\/icube-igg.unistra.fr\/en\/index.php\/Main_Page\">Computer Science in Geometry and Graphics (IGG)<\/a> en la Univ. de Estrasburgo, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  In computer science, functional orbits \u2212 i.e tracks left by iterating a function \u2212 in a finite domain naturally appear at a high or a low level. This paper introduces a Coq logical orbit framework, the purpose of which is to help rigorously developing software systems with some complex data structures from specification to implementation.<\/p>\n<p>  The result is a Coq library of orbit concepts formalized as definitions, lemmas and theorems. Most of them are inspired by our previous work in geometric modelling, where combinatorial hypermaps were used to describe surface subdivisions appearing in computational geometry problems, e.g. building convex hulls or Delaunay diagrams. Now, this domain remains a reference for us, but our results are drastically extended and usable in other computer science areas. The proof of Floyd\u2019s cycle-detection algorithm, known as \u201cthe tortoise and the hare\u201d, confirms that point.<\/p>\n<p>  The library contains operations to observe, traverse and update orbits \u2212 addition, deletion, mutation, transposition \u2212 with proofs of their behavior. It focuses on the important case where the involved function is a partial injection. In this case, it defines a connectivity relationship and evaluates the variation of the number of connected components during updates.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <em>Theoretical Computer Science<\/em>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado Formal study of functional orbits in finite domains. Su autor es Jean-Fran\u00e7ois Dufourd (del grupo Computer Science in Geometry and Graphics (IGG) en la Univ. de Estrasburgo, Francia). Su resumen es In computer science, functional orbits \u2212 i.e tracks left by iterating a function&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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\/4973"}],"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=4973"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4973\/revisions"}],"predecessor-version":[{"id":4974,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4973\/revisions\/4974"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4973"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4973"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4973"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}