Abstract
We present five axioms of name-carrying lambda-terms identified up to alpha-conversion—that is, up to renaming of bound variables. We assume constructors for constants, variables, application and lambda-abstraction. Other constants represent a function Fv that returns the set of free variables in a term and a function that substitutes a term for a variable free in another term. Our axioms are (1) equations relating Fv and each constructor, (2) equations relating substitution and each constructor, (3) alpha-conversion itself, (4) unique existence of functions on lambda-terms defined by structural iteration, and (5) construction of lambda-abstractions given certain functions from variables to terms. By building a model from de Bruijn’s nameless lambda-terms, we show that our five axioms are a conservative extension of HOL. Theorems provable from the axioms include distinctness, injectivity and an exhaustion principle for the constructors, principles of structural induction and primitive recursion on lambda-terms, Hindley and Seldin’s substitution lemmas and the existence of their length function. These theorems and the model have been mechanically checked in the Cambridge HOL system.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H. P. (1984). The Lambda Calculus: Its Syntax and Semantics (Revised ed.), Volume 103 of Studies in logic and the foundations of mathematics. North-Holland.
Boulton, R., A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel (1992). Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute (Eds.), Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10/WG 10.2 International Conference, Nijmegen, June 1992, IFIP Transactions A-10, pp. 129–156. North-Holland.
Church, A. (1941). The Calculi of Lambda-Conversion. Princeton University Press.
Curry, H. B. and R. Feys (1958). Combinatory Logic, Volume 1. North-Holland.
de Bruijn, N. G. (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 381–392.
Despeyroux, J. and A. Hirschowitz (1994, July). Higher-order abstract syntax with induction in Coq. In F. Pfenning (Ed.), Fifth International Conference on Logic Programming and Automated Reasoning (LPAR'94), Kiev, Volume 882 of LNAI, pp. 159–173. Springer-Verlag.
Gordon, A. D. (1994). A mechanisation of name-carrying syntax up to alpha-conversion. In J. J. Joyce and C.-J. H. Seger (Eds.), Higher Order Logic Theorem Proving and its Applications. Proceedings, 1993, Number 780 in Lecture Notes in Computer Science, pp. 414–426. Springer-Verlag.
Gordon, M. J. C. and T. F. Melham (Eds.) (1993). Introduction to HOL: A theorem-proving environment for higher-order logic. Cambridge University Press.
Hindley, J. R. and J. P. Seldin (1986). Introduction to Combinators and the λ-calculus. Cambridge University Press.
Lambek, J. and P. J. Scott (1986). Introduction to higher order categorical logic. Cambridge University Press.
Landin, P. J. (1964, January). The mechanical evaluation of expressions. Computer Journal 6, 308–320.
Matthews, S. (1995, September). Implementing FS 0 in Isabelle: adding structure at the metalevel. In L. C. Paulson (Ed.), Proceedings of the First Isabelle Users Workshop. Available as Technical Report 379, University of Cambridge Computer Laboratory.
McKinna, J. and R. Pollack (1993). Pure Type Systems formalized. In TLCA’ 93 International Conference on Typed Lambda Calculi and Applications, Utrecht, 16–18 March 1993, Volume 664 of Lecture Notes in Computer Science, pp. 289–305. Springer-Verlag.
Melham, T. F. (1994). A mechanized theory of the π-calculus in HOL. Nordic Journal of Computing 1, 50–76.
Milner, R., J. Parrow, and D. Walker (1992). A calculus of mobile processes, parts I and II. Information and Computation 100, 1–40 and 41–77.
Nordström, B., K. Petersson, and J. M. Smith (1990). Programming in Martin-Löf's Type Theory. Clarendon Press, Oxford.
Owens, C. (1995, September). Coding binding and substitution explicitly in Isabelle. In L. C. Paulson (Ed.), Proceedings of the First Isabelle Users Workshop. Available as Technical Report 379, University of Cambridge Computer Laboratory.
Paulson, L. C. (1994). Isabelle: A Generic Theorem Prover, Volume 828 of Lecture Notes in Computer Science. Springer-Verlag.
Pfenning, F. and C. Elliott (1988, June). Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN’ 88 Symposium on Language Design and Implementation, pp. 199–208.
Pollack, R. (1994). The Theory of LEGO. Ph. D. thesis, University of Edinburgh.
Stoughton, A. (1988). Substitution revisited. Theoretical Computer Science 59, 317–325.
Talcott, C. L. (1993). A theory of binding structures and applications to rewriting. Theoretical Computer Science 112, 99–143.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gordon, A.D., Melham, T. (1996). Five axioms of alpha-conversion. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1996. Lecture Notes in Computer Science, vol 1125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105404
Download citation
DOI: https://doi.org/10.1007/BFb0105404
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61587-3
Online ISBN: 978-3-540-70641-0
eBook Packages: Springer Book Archive