Computational Back-And-Forth Arguments in Constructive Type Theory

Author Dominik Kirst



PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.22.pdf
  • Filesize: 0.73 MB
  • 12 pages

Document Identifiers

Author Details

Dominik Kirst
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Cite AsGet BibTex

Dominik Kirst. Computational Back-And-Forth Arguments in Constructive Type Theory. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 22:1-22:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.22

Abstract

The back-and-forth method is a well-known technique to establish isomorphisms of countable structures. In this proof pearl, we formalise this method abstractly in the framework of constructive type theory, emphasising the computational interpretation of the constructed isomorphisms. As prominent instances, we then deduce Cantor’s and Myhill’s isomorphism theorems on dense linear orders and one-one interreducible sets, respectively. By exploiting the symmetry of the abstract argument, our approach yields a particularly compact mechanisation of the method itself as well as its two instantiations, all implemented using the Coq proof assistant. As adequate for a proof pearl, we attempt to make the text and mechanisation accessible for a general mathematical audience.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • back-and-forth method
  • computable isomorphisms
  • Coq

Metrics

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

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  2. Georg Cantor. Beiträge zur Begründung der transfiniten Mengenlehre. Mathematische Annalen, 46(4):481-512, 1895. Google Scholar
  3. 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). working paper or preprint, February 2022. URL: https://hal.inria.fr/hal-03580081.
  4. 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, pages 38-51, 2019. Google Scholar
  5. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. In CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020. Google Scholar
  6. Martin Giese and Arno Schönegge. Any Two Countable, Densely Ordered Sets Without Endpoints are Isomorphic: A Formal Proof with KIV. Univ., Fak. für Informatik, 1995. Google Scholar
  7. Paul Halmos and Steven Givant. Introduction to Boolean algebras. Springer, 2009. Google Scholar
  8. Felix Hausdorff. Grundzüge der Mengenlehre, 1914. Google Scholar
  9. Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  10. Evan Marzion. Visualizing Cantor’s theorem on dense linear orders using Coq. Blog post. URL: https://emarzion.github.io/Cantor-Thm/.
  11. Alexander G Melnikov and Keng Meng Ng. The back-and-forth method and computability without delay. Israel Journal of Mathematics, 234(2):959-1000, 2019. Google Scholar
  12. John Myhill. Creative sets. Journal of Symbolic Logic, 22(1), 1957. Google Scholar
  13. Bruno Poizat. A course in model theory: an introduction to contemporary mathematical logic. Springer Science & Business Media, 2012. Google Scholar
  14. Pierre Pradic and Chad E. Brown. Cantor-Bernstein implies excluded middle. arXiv preprint arXiv:1904.09193, 2019. Google Scholar
  15. Richard Rado. Universal graphs and universal functions. Acta Arithmetica, 9(4):331-340, 1964. Google Scholar
  16. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  17. Charles L. Silver. Who invented Cantor’s back-and-forth argument? Modern Logic, 4(1):74-78, 1994. Google Scholar
  18. Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in Coq. Proceedings of the ACM on Programming Languages, 3(ICFP):1-29, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail