{"id":4056,"date":"2014-01-26T08:07:32","date_gmt":"2014-01-26T07:07:32","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4056"},"modified":"2014-01-26T08:16:43","modified_gmt":"2014-01-26T07:16:43","slug":"applications-of-the-gauss-jordan-algorithm-done-right","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/applications-of-the-gauss-jordan-algorithm-done-right\/","title":{"rendered":"Applications of the Gauss-Jordan algorithm, done right"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> sobre \u00e1lgebra lineal titulado <a href=\"http:\/\/arxiv.org\/pdf\/1401.5910v1\">Applications of the Gauss-Jordan algorithm, done right<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.unirioja.es\/cu\/jearansa\">Jes\u00fas Mar\u00eda Aransay<\/a> y <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\">Jos\u00e9 Divas\u00f3n<\/a> (de la Univ. de la Rioja).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n<a href=\"http:\/\/en.wikipedia.org\/wiki\/Computer_algebra_system\">Computer Algebra systems<\/a> are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations are implemented and carried out in a way which is sometimes not transparent to the users, and that can lead to unexpected failures. <\/p>\n<p>In this paper we present a formalisation in a proof assistant system of a <i>naive<\/i> version of the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Gaussian_elimination\">Gauss-Jordan algorithm<\/a>, with explicit proofs of some of its applications, and additionally a process to obtain versions of this algorithm in two different functional languages (<a href=\"http:\/\/en.wikipedia.org\/wiki\/Standard_ML\">SML<\/a> and <a href=\"http:\/\/en.wikipedia.org\/wiki\/Haskell_%28programming_language%29\">Haskell<\/a>) by means of code generation techniques from the verified algorithm. The obtained programs are then applied to test cases, which, despite the simplicity of the original algorithm, have shown remarkable features in comparison to some Computer Algebra systems, such as <a href=\"http:\/\/en.wikipedia.org\/wiki\/Mathematica\">Mathematica<\/a> (where some of these computations are even incorrect), or <a href=\"http:\/\/en.wikipedia.org\/wiki\/Sage_%28mathematics_software%29\">Sage<\/a> (in comparison to which the generated programs show a compelling performance). <\/p>\n<p>The aim of the paper is to show that, with the current technology in Theorem Proving, formalising Linear Algebra procedures is a challenging but rewarding task, which provides programs that can be compared in some aspects to <i>state of the art<\/i> procedures in Computer Algebra systems, and whose correctness is formally proved.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\/Isabelle\/Gauss-Jordan-2013-2\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra lineal titulado Applications of the Gauss-Jordan algorithm, done right. Sus autores son Jes\u00fas Mar\u00eda Aransay y Jos\u00e9 Divas\u00f3n (de la Univ. de la Rioja). Su resumen es Computer Algebra systems are widely spread because of some of their remarkable features such as their&#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":[144,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\/4056"}],"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=4056"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4056\/revisions"}],"predecessor-version":[{"id":4059,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4056\/revisions\/4059"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4056"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4056"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4056"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}