Document Open Access Logo

A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory

Authors William DeMeo , Jacques Carette

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.4.pdf
  • Filesize: 463 kB
  • 21 pages

Document Identifiers

Author Details

William DeMeo
  • New Jersey Institute of Technology, Newark, NJ, USA
Jacques Carette
  • McMaster University, Hamilton, Canada

Funding

  • DeMeo, William: partially supported by ERC Consolidator Grant No. 771005.

Acknowledgements

This work would not have been possible without the wonderful https://wiki.portal.chalmers.se/agda/pmwiki.php language and the https://agda.github.io/agda-stdlib/, developed and maintained by The Agda Team [The Agda Team, 2021]. We thank the three anonymous referees for carefully reading the manuscript and offering many excellent suggestions which resulted in a vast improvement in the overall presentation. One referee went above and beyond and provided us with a simpler formalization of free algebras which led to simplifications of the proof of the main theorem. We are extremely grateful for this.

Cite AsGet BibTex

William DeMeo and Jacques Carette. A Machine-Checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.4

Abstract

The Agda Universal Algebra Library is a project aimed at formalizing the foundations of universal algebra, equational logic and model theory in dependent type theory using Agda. In this paper we draw from many components of the library to present a self-contained, formal, constructive proof of Birkhoff’s HSP theorem in Martin-Löf dependent type theory. This achieves one of the project’s initial goals: to demonstrate the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures by using them to formalize a significant theorem in the field.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Computing methodologies → Representation of mathematical objects
  • Theory of computation → Type theory
Keywords
  • Agda
  • constructive mathematics
  • dependent types
  • equational logic
  • formal verification
  • Martin-Löf type theory
  • model theory
  • universal algebra

Metrics

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

Related Versions

Supplementary Materials

References

  1. Andreas Abel. Birkhoff’s Completeness Theorem for multi-sorted algebras formalized in Agda. CoRR, abs/2111.07936, 2021. URL: http://arxiv.org/abs/2111.07936.
  2. Gianluca Amato, Marco Maggesi, and Cosimo Perini Brogi. Universal Algebra in UniMath. CoRR, abs/2102.05952, 2021. URL: http://arxiv.org/abs/2102.05952.
  3. Clifford Bergman. Universal Algebra: fundamentals and selected topics, volume 301 of Pure and Applied Mathematics (Boca Raton). CRC Press, Boca Raton, FL, 2012. Google Scholar
  4. G Birkhoff. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society, 31(4):433-454, October 1935. Google Scholar
  5. Venanzio Capretta. Universal Algebra in Type Theory. In Theorem proving in higher order logics (Nice, 1999), volume 1690 of Lecture Notes in Comput. Sci., pages 131-148. Springer, Berlin, 1999. URL: https://doi.org/10.1007/3-540-48256-3_10.
  6. William DeMeo. The Agda Universal Algebra Library. GitHub.com, 2020. Ver. 1.0.0. Source code: URL: https://gitlab.com/ualib/ualib.gitlab.io.
  7. William DeMeo and Jacques Carette. A Machine-checked Proof of Birkhoff’s Variety Theorem in Martin-Löf Type Theory. CoRR, abs/2101.10166, 2021. Source code: https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda. URL: https://doi.org/10.48550/ARXIV.2101.10166.
  8. William DeMeo and Jacques Carette. The Agda Universal Algebra Library (agda-algebras). GitHub.com, 2021. Ver. 2.0.1. Source code: https://zenodo.org/record/5765793/files/ualib/agda-algebras-v.2.0.1.zip?download=1. Documentation: https://ualib.org. GitHub repo: https://github.com/ualib/agda-algebras. URL: https://doi.org/10.5281/zenodo.5765793.
  9. Martín Hötzel Escardó. Introduction to Univalent Foundations of mathematics with Agda. https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/, May 2019. Accessed on 30 Nov 2021.
  10. Martín Hötzel Escardó. Introduction to Univalent Foundations of mathematics with Agda. CoRR, abs/1911.00580, 2019. URL: http://arxiv.org/abs/1911.00580.
  11. Emmanuel Gunther, Alejandro Gadea, and Miguel Pagano. Formalization of Universal Algebra in Agda. Electronic Notes in Theoretical Computer Science, 338:147-166, 2018. The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017). URL: https://doi.org/10.1016/j.entcs.2018.10.010.
  12. Jason Z. S. Hu and Jacques Carette. Formalizing Category Theory in Agda. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 327-342, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439922.
  13. Artur Korniłowicz. Birkhoff theorem for many sorted algebras, 1999. Google Scholar
  14. Andreas Lynge and Bas Spitters. Universal Algebra in HoTT. In Proceedings of the 25th International Conference on Types for Proofs and Programs (TYPES 2019), 2019. URL: http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_7.
  15. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Google Scholar
  16. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Lulu and The Univalent Foundations Program, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.
  17. Bas Spitters and Eelis Van der Weegen. Type classes for mathematics in type theory. CoRR, abs/1102.1323, 2011. URL: http://arxiv.org/abs/1102.1323.
  18. The Agda Team. Agda Language Reference, 2021. URL: https://agda.readthedocs.io/en/v2.6.1/language/index.html.
  19. The Agda Team. Agda Language Reference section on Axiom K, 2021. URL: https://agda.readthedocs.io/en/v2.6.1/language/without-k.html.
  20. The Agda Team. Agda Language Reference section on Safe Agda, 2021. URL: https://agda.readthedocs.io/en/v2.6.1/language/safe-agda.html#safe-agda.
  21. The Agda Team. The Agda Standard Library, 2021. URL: https://github.com/agda/agda-stdlib.
  22. The Agda Team. Agda Tools Documentation section on Pattern matching and equality, 2021. URL: https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html#pattern-matching-and-equality.
  23. The Coq Development Team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0. URL: http://coq.inria.fr.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact