{"id":5012,"date":"2015-09-11T07:35:20","date_gmt":"2015-09-11T05:35:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5012"},"modified":"2015-09-11T07:35:20","modified_gmt":"2015-09-11T05:35:20","slug":"resena-formalization-of-shannons-theorems","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-shannons-theorems\/","title":{"rendered":"Rese\u00f1a: Formalization of Shannon&#8217;s theorems"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> sobre teor\u00eda de la informaci\u00f3n titulado <a href=\"http:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/shannon_theorems.pdf\">Formalization of Shannon&#8217;s theorems<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/\">Reynald Affeldt<\/a> (del <a href=\"http:\/\/bit.ly\/1Kwq0gn\">AIST (National Institute of Advanced Industrial Science and Technology)<\/a> en Tsukuba, Jap\u00f3n), <\/li>\n<li><a href=\"http:\/\/dblp.uni-trier.de\/pers\/hd\/h\/Hagiwara:Manabu\">Manabu Hagiwara<\/a> (de la <a href=\"http:\/\/bit.ly\/1ii4PT6\">Chiba University<\/a> en Chiba, Jap\u00f3n) y<\/li>\n<li><a href=\"http:\/\/dblp.uni-trier.de\/pers\/hd\/s\/S=eacute=nizergues:Jonas\">Jonas S\u00e9nizergues<\/a> (de la <a href=\"https:\/\/en.wikipedia.org\/wiki\/%C3%89cole_normale_sup%C3%A9rieure_de_Cachan\">Ecole Normale Sup\u00e9rieure de Cachan<\/a>, France).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  The most fundamental results of information theory are Shannon\u2019s theorems. These theorems express the bounds for (1) reliable data compression and (2) data transmission over a noisy channel. Their proofs are non-trivial but are rarely detailed, even in the introductory literature. This lack of formal foundations is all the more unfortunate that crucial results in computer security rely solely on information theory: this is the so-called \u201cunconditional security\u201d. In this article, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem, that introduces the entropy as the bound for lossless compression, and of the channel coding theorem, that introduces the capacity as the bound for reliable communication over a noisy channel.\n<\/p><\/blockquote>\n<p>El art\u00edculo, publicado en  el <a href=\"http:\/\/bit.ly\/1ii5JPw\">JAR<\/a>, es una extensi\u00f3n del trabajo <a href=\"http:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/affeldt-itp2012-preprint.pdf\">Formalization of Shannon&#8217;s Theorems in SSReflect-Coq<\/a> presentado en el <a href=\"http:\/\/itp2012.cs.princeton.edu\/\">ITP 2012<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/shannon\">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 <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/LCyTM-15\">L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre teor\u00eda de la informaci\u00f3n titulado Formalization of Shannon&#8217;s theorems. Sus autores son Reynald Affeldt (del AIST (National Institute of Advanced Industrial Science and Technology) en Tsukuba, Jap\u00f3n), Manabu Hagiwara (de la Chiba University en Chiba, Jap\u00f3n) y Jonas S\u00e9nizergues (de la Ecole Normale Sup\u00e9rieure&#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":[1],"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\/5012"}],"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=5012"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5012\/revisions"}],"predecessor-version":[{"id":5013,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5012\/revisions\/5013"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5012"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5012"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5012"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}