TY - GEN
T1 - On the formalisation of Kolmogorov complexity
AU - Catt, Elliot
AU - Norrish, Michael
N1 - Publisher Copyright:
© 2021 ACM.
PY - 2021/1/17
Y1 - 2021/1/17
N2 - Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key to proving results in the theory of Intelligent Agents, specifically the results in Universal Artificial Intelligence. In this paper, we present a mechanisation of some of these fundamental results. In particular, building on HOL4's existing model of computability, we provide a formal definition of the complexity of a binary string, and then prove (i) that Kolmogorov complexity is uncomputable; (ii) the Kolmogorov Complexity invariance theorem; (iii) the Kraft and Kolmogorov-Kraft inequalities; and (iv) key Kolmogorov Complexity inequalities.
AB - Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key to proving results in the theory of Intelligent Agents, specifically the results in Universal Artificial Intelligence. In this paper, we present a mechanisation of some of these fundamental results. In particular, building on HOL4's existing model of computability, we provide a formal definition of the complexity of a binary string, and then prove (i) that Kolmogorov complexity is uncomputable; (ii) the Kolmogorov Complexity invariance theorem; (iii) the Kraft and Kolmogorov-Kraft inequalities; and (iv) key Kolmogorov Complexity inequalities.
KW - Computability
KW - Interactive proof systems
KW - Kolmogorov complexity
UR - http://www.scopus.com/inward/record.url?scp=85100548626&partnerID=8YFLogxK
U2 - 10.1145/3437992.3439921
DO - 10.1145/3437992.3439921
M3 - Conference contribution
T3 - CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021
SP - 291
EP - 299
BT - CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021
A2 - Hritcu, Catalin
A2 - Popescu, Andrei
PB - Association for Computing Machinery (ACM)
T2 - 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
Y2 - 17 January 2021 through 19 January 2021
ER -