Reseña: Formalization of Shannon’s theorems in SSReflect-Coq
Se ha publicado un nuevo artículo de razonamiento formalizado en Coq, titulado Formalization of Shannon’s theorems in SSReflect-Coq.
Sus autores son Reynald Affeldt y Manabu Hagiwara (del National Institute of Advanced Industrial Science and Technology en Tsukuba, Japón).
El trabajo se presentó ayer en el ITP 2012 (Interactive Theorem Proving).
El resumen del trabajo es
The most fundamental results of information theory are Shannon’s theorems. These theorems express the bounds for reliable data compression and transmission over a noisy channel. Their proofs are non-trivial but rarely detailed, even in the introductory literature. This lack of formal foundations makes it all the more unfortunate that crucial results in computer security rely solely on information theory (the so-called “unconditional security”). In this paper, 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 the direct part of the more difficult channel coding theorem (that introduces the capacity as the bound for reliable communication over a noisy channel).
El código de la formalización se encuentra aquí.