Formalization of Shannon's Theorems
Formalization of Shannon's Theorems
复制标题
DOI：
10.1007/s10817-013-9298-1
复制
发表时间：
2014-06-01
期刊：
影响因子：
--
通讯作者：
Senizergues, Jonas
中科院分区：
文献类型：
--
作者：
Affeldt, Reynald;Hagiwara, Manabu;Senizergues, Jonas
信息理论最基本的结果是香农的定理。这些定理表示（1）可靠数据压缩和（2）在嘈杂通道上传输的界限。他们的证明是不平凡的，但很少有详细的详细说明，即使在介绍性文献中也是如此。缺乏正式的基础是更不幸的是，计算机安全的关键结果仅依赖于信息理论：这是所谓的“无条件安全”。在本文中，我们在COQ证明辅助剂的SSSEFRECT扩展中报告了信息理论库的形式化。特别是，我们产生了源编码定理的第一个正式证明，该证明引入了熵作为无损压缩的界限和通道编码定理的界限，该定理将能力引入能力，作为在噪音通道上可靠的通信的界限。
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.