Reseña: Formalization of Shannon’s theorems
Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de la información titulado Formalization of Shannon’s theorems.
Sus autores son
- Reynald Affeldt (del AIST (National Institute of Advanced Industrial Science and Technology) en Tsukuba, Japón),
- Manabu Hagiwara (de la Chiba University en Chiba, Japón) y
- Jonas Sénizergues (de la Ecole Normale Supérieure de Cachan, France).
Su resumen es
The most fundamental results of information theory are Shannon’s 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 “unconditional security”. 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.
El artículo, publicado en el JAR, es una extensión del trabajo Formalization of Shannon’s Theorems in SSReflect-Coq presentado en el ITP 2012.
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.