×

Formalization of Shannon’s theorems. (English) Zbl 1315.68216

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
94A17 Measures of information, entropy
94A24 Coding theorems (Shannon theory)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Affeldt, R.; Hagiwara, M., Formalization of Shannon’s Theorems in SSReflect-Coq, 233-249 (2012), Heidelberg · Zbl 1314.68270
[2] Affeldt, R., Hagiwara, M., Sénizergues, J.: Formalization of Shannon’s Theorems in SSReflect-Coq. Coq documentation and scripts available at http://staff.aist.go.jp/reynald.affeldt/shannon · Zbl 1314.68270
[3] Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Prog. 74(8), 568-589 (2009) · Zbl 1178.68667 · doi:10.1016/j.scico.2007.09.002
[4] Barthe, G.; Crespo, JM; Grégoire, B.; Kunz, C.; Zanella Béguelin, S., Computer-Aided Cryptographic Proofs, 11-27 (2012), Heidelberg · Zbl 1360.94294
[5] Bertot, Y.; Gonthier, G.; Ould Biha, S.; Pasca, I., Canonical Big Operators, 86-101 (2008), Heidelberg · Zbl 1165.68450
[6] Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. PhD Thesis, King’s College. University of Cambridge, UK (2010)
[7] The Coq Development Team. Reference Manual. Version 8.4. Available at http://coq.inria.fr. INRIA (2004-2012) · Zbl 1200.94005
[8] Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. Wiley-Interscience (2006) · Zbl 1140.94001
[9] Csiszár, I.: The method of types. IEEE Trans. Inform. Theory 44(6), 2505-2523 (1998) · Zbl 0933.94012 · doi:10.1109/18.720546
[10] Csiszár, I., Körner, J.: Information Theory—Coding Theorems for Discrete Memoryless Systems, 2nd edn. Cambridge University Press (2011) · Zbl 1256.94002
[11] Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Version 10. Technical Report RR-6455, INRIA (2011) · Zbl 1178.68667
[12] Hagiwara, M.: Coding Theory: Mathematics for Digital Communication. In Japanese. http://www.nippyo.co.jp/book/5977.html. Nippon Hyoron Sha (2012) · Zbl 1314.68270
[13] Hasan, O., Tahar, S.: Verification of expectation using theorem proving to verify expectation and variance for discrete random variables. J. Autom. Reason. 41, 295-323 (2008) · Zbl 1191.68621 · doi:10.1007/s10817-008-9113-6
[14] Hölzl, J.; Heller, A., Three Chapters of Measure Theory in Isabelle/HOL, 135-151 (2011), Heidelberg · Zbl 1342.68287
[15] Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, Trinity College, University of Cambridge, UK (2001)
[16] Mhamdi, T.; Hasan, O.; Tahar, S., On the Formalization of the Lebesgue Integration Theory in HOL, 387-402 (2010), Heidelberg · Zbl 1291.68362
[17] Mhamdi, T.; Hasan, O.; Tahar, S., Formalization of Entropy Measures in HOL, 233-248 (2010), Heidelberg · Zbl 1342.68295
[18] Khudanpur, S.: Information Theoretic Methods in Statistics. Lecture Notes. Available at http://old-site.clsp.jhu.edu/sanjeev/520.674/notes/GISAlgorithm.pdf (1999). Accessed 02 May 2013
[19] Shannon, C.E.: A Mathematical theory of communication. Bell Syst. Tech. J. 27, 379-423 and 623-656 (1948) · Zbl 1154.94303 · doi:10.1002/j.1538-7305.1948.tb01338.x
[20] Shannon, C.E.: Communication theory of secrecy systems. Bell Sys. Tech. J. 28, 656-715 (1949) · Zbl 1200.94005 · doi:10.1002/j.1538-7305.1949.tb00928.x
[21] Uyematsu, T.: Modern Shannon Theory, Information Theory with Types. In Japanese. Baifukan (1998) · Zbl 1154.94303
[22] Verdú, S.: Fifty years of Shannon theory. IEEE Trans. Inform. Theory 44(6), 2057-2078 (1998) · Zbl 1125.94300 · doi:10.1109/18.720531
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.