Document Open Access Logo

Synthetic Kolmogorov Complexity in Coq

Authors Yannick Forster , Fabian Kunze, Nils Lauermann

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.12.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Yannick Forster
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
  • Inria, Gallinette Project-Team, Nantes, France
Fabian Kunze
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Nils Lauermann
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
  • University of Cambridge, Cambridge, United Kingdom

Funding

  • Forster, Yannick: received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.

Acknowledgements

We want to thank Dominik Kirst and Gert Smolka for many fruitful discussions.

Cite AsGet BibTex

Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.12

Abstract

We present a generalised, constructive, and machine-checked approach to Kolmogorov complexity in the constructive type theory underlying the Coq proof assistant. By proving that nonrandom numbers form a simple predicate, we obtain elegant proofs of undecidability for random and nonrandom numbers and a proof of uncomputability of Kolmogorov complexity. We use a general and abstract definition of Kolmogorov complexity and subsequently instantiate it to several definitions frequently found in the literature. Whereas textbook treatments of Kolmogorov complexity usually rely heavily on classical logic and the axiom of choice, we put emphasis on the constructiveness of all our arguments, however without blurring their essence. We first give a high-level proof idea using classical logic, which can be formalised with Markov’s principle via folklore techniques we subsequently explain. Lastly, we show a strategy how to eliminate Markov’s principle from a certain class of computability proofs, rendering all our results fully constructive. All our results are machine-checked by the Coq proof assistant, which is enabled by using a synthetic approach to computability: rather than formalising a model of computation, which is well known to introduce a considerable overhead, we abstractly assume a universal function, allowing the proofs to focus on the mathematical essence.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Kolmogorov complexity
  • computability theory
  • random numbers
  • constructive matemathics
  • synthetic computability theory
  • constructive type theory
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  2. Andrej Bauer. On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, 10(3):167-181, 2017. URL: https://doi.org/10.1515/tmj-2017-0107.
  3. Douglas Bridges and Fred Richman. Varieties of constructive mathematics, volume 97. Cambridge University Press, 1987. URL: https://doi.org/10.1017/CBO9780511565663.
  4. Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:17, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.12.
  5. Elliot Catt and Michael Norrish. On the formalisation of Kolmogorov complexity. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, January 2021. URL: https://doi.org/10.1145/3437992.3439921.
  6. Gregory J. Chaitin. On the simplicity and speed of programs for computing infinite sets of natural numbers. Journal of the ACM, 16(3):407-422, July 1969. URL: https://doi.org/10.1145/321526.321530.
  7. Thierry Coquand and Gérard P Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  8. Andrej Dudenhefner. The undecidability of system F typability and type checking for reductionists. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-10. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470520.
  9. Andrej Dudenhefner. Constructive many-one reduction from the halting problem to semi-unification. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 18:1-18:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.18.
  10. Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, and Mauricio Ayala-Rincón. Formalization of rice’s theorem over a functional language model. Technical report, University of Brasília, 2020. URL: https://www.mat.unb.br/~ayala/RiceThFormalization.pdf.
  11. Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
  12. Yannick Forster. Computability in Constructive Type Theory. PhD thesis, Saarland University, 2021. URL: https://doi.org/10.22028/D291-35758.
  13. Yannick Forster. Parametric church’s thesis: Synthetic computability without choice. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022, Proceedings, volume 13137 of Lecture Notes in Computer Science, pages 70-89. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-93100-1_6.
  14. Yannick Forster, Felix Jahn, and Gert Smolka. A Constructive and Synthetic Theory of Reducibility: Myhill’s Isomorphism Theorem and Post’s Problem for Many-one and Truth-table Reducibility in Coq (Full Version), February 2022. preprint. URL: https://hal.inria.fr/hal-03580081.
  15. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2019. ACM Press, 2019. URL: https://doi.org/10.1145/3293880.3294091.
  16. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  17. Yannick Forster and Gert Smolka. Weak call-by-value lambda calculus as a model of computation in Coq. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pages 189-206. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_13.
  18. R. M. Friedberg. Two recursively enumerable sets of incomparable degrees of unsovlability (solution of post’s problem, 1944. Proceedings of the National Academy of Sciences, 43(2):236-238, February 1957. URL: https://doi.org/10.1073/pnas.43.2.236.
  19. Lennard Gäher and Fabian Kunze. Mechanising complexity theory: The cook-levin theorem in Coq. In 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ITP.2021.20.
  20. Marcus Hutter. Universal Artificial Intellegence. Springer Berlin Heidelberg, 2005. URL: https://doi.org/10.1007/b138233.
  21. Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq. In Automated Reasoning, pages 79-96. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_5.
  22. Steven C. Kleene and Emil L. Post. The upper semi-lattice of degrees of recursive unsolvability. The Annals of Mathematics, 59(3):379, May 1954. URL: https://doi.org/10.2307/1969708.
  23. John R. Kline. The April meeting in New York. Bulletin of the American Mathematical Society, 54(7):622-648, July 1948. URL: https://doi.org/10.1090/s0002-9904-1948-09030-9.
  24. Andrei N Kolmogorov. On tables of random numbers. Sankhyā: The Indian Journal of Statistics, Series A, pages 369-376, 1963. URL: https://doi.org/10.1016/S0304-3975(98)00075-9.
  25. Andrei N. Kolmogorov. Three approaches to the quantitative definition of information. Problems of information transmission, 1(1):3-11, 1965. Google Scholar
  26. Martin Kummer. On the complexity of random strings. In Annual Symposium on Theoretical Aspects of Computer Science, pages 25-36. Springer, 1996. URL: https://doi.org/10.1007/3-540-60922-9_3.
  27. Dominique Larchey-Wendling. Typing total recursive functions in Coq. In International Conference on Interactive Theorem Proving, pages 371-388. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_24.
  28. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:20. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.27.
  29. Nils Lauermann. A formalization of Kolmogorov complexity in synthetic computability theory. Bachelor’s thesis, Saarland University, 2021. URL: https://ps.uni-saarland.de/~lauermann/bachelor.php.
  30. Ming Li and Paul Vitányi. An Introduction to Kolmogorov Complexity and Its Applications. Springer New York, 2008. URL: https://doi.org/10.1007/978-0-387-49820-1.
  31. Albert Abramovich Muchnik. On strong and weak reducibility of algorithmic problems. Sibirskii Matematicheskii Zhurnal, 4(6):1328-1341, 1963. Google Scholar
  32. John Myhill. Creative sets. Zeitschr. f. math. Logik und Grundlagen d. Math., 1957. URL: https://doi.org/10.1002/malq.19550010205.
  33. Michael Norrish. Mechanised computability theory. In ITP 2011, volume 6898 of LNCS, pages 297-311. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_22.
  34. Piergiorgio Odifreddi. Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier, 1992. Google Scholar
  35. Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  36. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions, January 2015. URL: https://hal.inria.fr/hal-01094195.
  37. Emil L. Post. Recursively enumerable sets of positive integers and their decision problems. bulletin of the American Mathematical Society, 50(5):284-316, 1944. URL: https://doi.org/10.1090/S0002-9904-1944-08111-1.
  38. Emil L. Post. Degrees of recursive unsolvability - preliminary report. In Bulletin of the American Mathematical Society, volume 54(7), pages 641-642. American Mathematical Society (AMS), July 1948. Google Scholar
  39. Henry G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2):358-366, 1953. URL: https://doi.org/10.1090/S0002-9947-1953-0053041-6.
  40. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. URL: https://doi.org/10.2307/2273473.
  41. Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, MA, USA, 1987. Google Scholar
  42. A. Shen, V. Uspensky, and N. Vereshchagin. Kolmogorov Complexity and Algorithmic Randomness. American Mathematical Society, November 2017. URL: https://doi.org/10.1090/surv/220.
  43. Michael Sipser. Introduction to the Theory of Computation, volume 2. Thomson Course Technology Boston, 2006. URL: https://doi.org/10.1145/230514.571645.
  44. Ray J. Solomonoff. A preliminary report on a general theory of inductive inference (revision of report v-131). Contract AF, 49(639):376, 1960. Google Scholar
  45. R.J. Solomonoff. A formal theory of inductive inference. part i. Information and Control, 7(1):1-22, March 1964. URL: https://doi.org/10.1016/s0019-9958(64)90223-2.
  46. R.J. Solomonoff. A formal theory of inductive inference. part II. Information and Control, 7(2):224-254, June 1964. URL: https://doi.org/10.1016/s0019-9958(64)90131-7.
  47. The Coq Development Team. The Coq proof assistant version 8.13.2, January 2021. URL: https://doi.org/10.5281/zenodo.4501022.
  48. Paul M.B. Vitányi. How incomputable is Kolmogorov complexity? Entropy, 22(4):408, April 2020. URL: https://doi.org/10.3390/e22040408.
  49. Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing machines and computability theory in Isabelle/HOL. In International Conference on Interactive Theorem Proving, pages 147-162. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_13.
  50. A K Zvonkin and L A Levin. The complexity of finite objects and the development of the concepts of information and randomness by means of the theory of algorithms. Russian Mathematical Surveys, 25(6):83-124, December 1970. URL: https://doi.org/10.1070/rm1970v025n06abeh001269.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact