@inproceedings{9a9f74a5945b451ebd7879e4d2cd8fe5,
title = "On the formalisation of Kolmogorov complexity",
abstract = "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.",
keywords = "Computability, Interactive proof systems, Kolmogorov complexity",
author = "Elliot Catt and Michael Norrish",
note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 ; Conference date: 17-01-2021 Through 19-01-2021",
year = "2021",
month = jan,
day = "17",
doi = "10.1145/3437992.3439921",
language = "English",
series = "CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021",
publisher = "Association for Computing Machinery (ACM)",
pages = "291--299",
editor = "Catalin Hritcu and Andrei Popescu",
booktitle = "CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021",
address = "United States",
}