{"id":5007,"date":"2015-09-08T07:50:11","date_gmt":"2015-09-08T05:50:11","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5007"},"modified":"2015-09-08T07:50:49","modified_gmt":"2015-09-08T05:50:49","slug":"resena-matrices-jordan-normal-forms-and-spectral-radius-theory","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-matrices-jordan-normal-forms-and-spectral-radius-theory\/","title":{"rendered":"Rese\u00f1a: Matrices, Jordan normal forms, and spectral radius theory"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre<br \/>\n\u00e1lgebra lineal titulado <a href=\"http:\/\/afp.sourceforge.net\/entries\/Jordan_Normal_Form.shtml\">Matrices, Jordan normal forms, and spectral radius theory<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/thiemann\">Ren\u00e9 Thiemann<\/a>  y <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/ayamada\/\">Akihisa Yamada<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\/\">Computational Logic Group<\/a> en la <a href=\"http:\/\/bit.ly\/1ELGKOo\">Universidad de Innsbruck<\/a>, Austria)<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.<\/p>\n<p>  To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we did not yet formalize the Schur decomposition.<\/p>\n<p>  The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.<\/p>\n<p>  All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en <a href=\"http:\/\/afp.sourceforge.net\/index.shtml\">The Archive of Formal Proofs <\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Jordan_Normal_Form\/index.html\">aqu\u00ed<\/a>.<\/p>\n<p>Este art\u00edculo puede servir de lectura complementaria en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a>, <a href=\"http:\/\/www.cs.us.es\/cursos\/rac\/\">Razonamiento asistido por ordenador<\/a> y <em>L\u00f3gica computacional y teor\u00eda de modelos<\/em>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra lineal titulado Matrices, Jordan normal forms, and spectral radius theory. Sus autores son Ren\u00e9 Thiemann y Akihisa Yamada (del Computational Logic Group en la Universidad de Innsbruck, Austria) Su resumen es Matrix interpretations are useful as measure functions in termination proving. In order&#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\/5007"}],"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=5007"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5007\/revisions"}],"predecessor-version":[{"id":5009,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5007\/revisions\/5009"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5007"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5007"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5007"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}