Document Open Access Logo

Mechanising Böhm Trees and λη-Completeness

Authors Chun Tian , Michael Norrish

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.28.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Computing methodologies → Theorem proving algorithms
Keywords
  • untyped λ-calculus
  • Böhm trees
  • higher-order logic
  • theorem proving

Metrics

Abstract

The Böhm tree is a critical notion in untyped λ-calculus, capturing the semantics of β-reduction. It underpins the proof that the equational theory of βη-equivalence is Hilbert-Post complete.
This paper presents the first formalisation of this result, following the classic text by Barendregt. It includes a coinductive definition of Böhm trees, and then uses the "Böhm out" technique to prove a restricted version of Böhm’s separability theorem, which leads to the completeness theorem.
Carrying out the proofs in HOL4, we develop a new technology to generate fresh names occurring in Böhm trees. We also simplify Barendregt’s approach, avoiding comparing Böhm trees, and leveraging more modern proofs about η-reduction (due to Takahashi).
Along the way, we also present the first mechanised proof that terms having head-normal forms are exactly those that are solvable (due to Wadsworth).

Cite As Get BibTex

Chun Tian and Michael Norrish. Mechanising Böhm Trees and λη-Completeness. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.28

Author Details

Chun Tian
  • School of Computing, The Australian National University, Canberra, Australia
Michael Norrish
  • School of Computing, The Australian National University, Canberra, Australia

References

  1. Beniamino Accattoli. Proof pearl: Abella formalization of λ-calculus cube property. In Chris Hawblitzel and Dale Miller, editors, LNCS 7679 - Certified Programs and Proofs (CPP 2012), pages 173-187. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-35308-6_15.
  2. Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '08, pages 3-15, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1328438.1328443.
  3. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: the PoplMark challenge. In TPHOLs'05, pages 50-65, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/11541868_4.
  4. Henk P. Barendregt. The type free lambda calculus. In Handbook of Mathematical Logic, pages 1091-1132. North-Holland, 1977. Google Scholar
  5. Henk P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 40 of Studies in Logic. North-Holland Publishing Company, 1984. Google Scholar
  6. Henk P. Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite, volume 94 of Studies in Logic. College Publications, 2022. Google Scholar
  7. Corrado Böhm. Alcune proprietà delle forme β-η-normali nel λ-k-calcolo. Pubblicazioni dell'Instituto per le Applicazioni del Calcolo, 696:1-19, 1968. Google Scholar
  8. 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, LNCS 10499 - Interactive Theorem Proving (ITP 2017), pages 189-206. Springer, Cham, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_13.
  9. Gérard P Huet. An analysis of Böhm’s theorem. Theoretical Computer Science, 121:145-167, 1993. URL: https://doi.org/10.1016/0304-3975(93)90087-A.
  10. Gérard P Huet. Regular Böhm trees. Mathematical Structures in Computer Science, 8(6):671-680, December 1998. URL: https://doi.org/10.1017/S0960129598002643.
  11. Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s theory of the λ-calculus, refreshed and formalized. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:22, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.13.
  12. James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23:373-409, 1999. URL: https://doi.org/10.1023/A:1006294005493.
  13. Michael Norrish. Mechanising λ-calculus using a classical first order theory of terms with permutations. Higher-Order and Symbolic Computation, 19(2-3):169-195, September 2006. URL: https://doi.org/10.1007/s10990-006-8745-7.
  14. Michael Norrish. Mechanised computability theory. In Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, LNCS 6898 - Interactive Theorem Proving (ITP 2011), pages 297-311. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22863-6_22.
  15. Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic. A formal equational theory for call-by-push-value. In LNCS 10895 - Interactive Theorem Proving (ITP 2018), pages 523-541. Springer, June 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_31.
  16. Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In LNCS 9236 - Interactive Theorem Proving (ITP 2015), pages 359-374. Springer, July 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_24.
  17. Natarajan Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 1988. URL: https://doi.org/10.1145/44483.44484.
  18. Masako Takahashi. Parallel reductions in λ-calculus. Information and Computation, 1995. URL: https://doi.org/10.1006/inco.1995.1057.
  19. Christian Urban. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning, 40(4):327-356, 2008. URL: https://doi.org/10.1007/s10817-008-9097-2.
  20. Xinyi Wan and Qinxiang Cao. Formalization of lambda calculus with explicit names as a nominal reasoning framework. In SETTA, 2023. URL: https://doi.org/10.1007/978-981-99-8664-4_15.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact