Abstract
We formalize the metatheory of lambda calculus in Coq, in its classic form with explicit names. The formalization is founded upon an intuitive \(\alpha \)-equivalence definition without substitution or name swap**. Furthermore, we provide structural and rule induction principles that encapsulate the Barendregt Variable Convention, enabling formal proofs mirroring informally-styled ones. These principles are leveraged to establish foundational results such as the Church-Rosser theorem. Demonstrating the framework’s utility, we extend first-order logic with predicate definitions, ensuring its soundness through properties obtained from the metatheory by encoding propositions as lambda terms.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
An additional constraint is that all “correct” contexts can only be obtained through the operation in the \(\alpha _{ABS}\) rule. We assume it implicitly holds within this paper.
- 2.
We require all propositions to be well-formed, i.e. propositions should not contain any freely-occurring predicates and all predicates are applied to correct number of terms as their definitions.
References
Barendregt, H.P., et al.: The lambda calculus, vol. 3. North-Holland Amsterdam (1984)
Charguéraud, A.: The locally nameless representation. J. Autom. Reason. 49, 363–408 (2012)
Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 143–156 (2008)
Copello, E., Szasz, N., Tasistro, Á.: Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory. Electron. Notes Theor. Comput. Sci. 338, 79–95 (2018)
Copello, E., Szasz, N., Tasistro, Á.: Formalization of metatheory of the lambda calculus in constructive type theory using the Barendregt variable convention. Math. Struct. Comput. Sci. 31(3), 341–360 (2021)
De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae (Proceedings), vol. 75, pp. 381–392. Elsevier (1972)
Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 124–138. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0014049
Ebbinghaus, H.D., Flum, J., Thomas, W., Ferebee, A.S.: Mathematical Logic, vol. 1910. Springer, Heidelberg (1994). https://doi.org/10.1007/978-3-030-73839-6
Felty, A., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48(1), 43–105 (2012)
Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 173–190. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0105404
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)
Stark, K., Schäfer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 166–180 (2019)
Urban, C.: Nominal techniques in isabelle/hol. J. Autom. Reason. 40, 327–356 (2008)
Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 35–50. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_4
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comput. Sci. 323(1–3), 473–497 (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Wan, X., Cao, Q. (2024). Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework. In: Hermanns, H., Sun, J., Bu, L. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2023. Lecture Notes in Computer Science, vol 14464. Springer, Singapore. https://doi.org/10.1007/978-981-99-8664-4_15
Download citation
DOI: https://doi.org/10.1007/978-981-99-8664-4_15
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-8663-7
Online ISBN: 978-981-99-8664-4
eBook Packages: Computer ScienceComputer Science (R0)