Skip Navigation



Journal of Logic and Computation Advance Access published online on September 13, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp049
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, M. J.
Right arrow Articles by Mathijssen, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

A Nominal Axiomatization of the Lambda Calculus

Murdoch J. Gabbay 1

School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh EH14 4AS, Scotland, Great Britain.

Aad Mathijssen

Department of Mathematics and Computer Science, Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands.
E-mail: a.h.j.mathijssen{at}tue.nl

Received 12 June 2008.

The lambda calculus is fundamental in computer science. It resists an algebraic treatment because of capture-avoidance sideconditions. Nominal algebra is a logic of equality designed for specifications involving binding. We axiomatize the lambda calculus using nominal algebra, demonstrate how proofs with these axioms reflect the informal arguments on syntax and we prove the axioms to be sound and complete. We consider both non-extensional and extensional versions (alpha-beta and alpha-beta-eta equivalence). This connects the nominal approach to names and binding with the view of variables as a syntactic convenience for describing functions. The axiomatization is finite, close to informal practice and it fits into a context of other research such as nominal rewriting and nominal sets.

Keywords: Lambda calculus; equational logic; nominal techniques

1Homepage: www.gabbay.org.uk



References

  1. Abadi M, Cardelli L, Curien P-L, Lévy J-J. Explicit substitutions. Journal of Functional Programming (1992) 1:375–416.
  2. Abramsky S, Ghica DR, Murawski AS, Ong C-H, Luke Stark IDB. Nominal games and full abstraction for the nu-calculus. (2004) IEEE Computer Society. 150–159. In Proceedings of 19th IEEE Symposium on Logic in Computer Science (LICS 2004).
  3. Andrews PB. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (1986) Academic Press.
  4. Andrews PB, Bishop M, Issar S, Nesmith D, Pfenning F, Xi H. TPS: a theorem proving system for classical type theory. Journal of Automated Reasoning (1996) 16:321–353.[CrossRef][Web of Science]
  5. Antonio Bucciarelli GM, Ehrhard T. Not enough points is enough. In: Proceedings of 21st International Workshop on Computer Science Logic (CSL 2007) (2007) Springer. 298–312. Vol. 4646 of Lecture Notes in Computer Science.
  6. Baader F, Nipkow T. Term Rewriting and All That (1998) Cambridge University Press.
  7. Barendregt HP. The Lambda Calculus: its Syntax and Semantics (Revised edn) (1984) North-Holland.
  8. Barwise J. An introduction to first-order logic. In: Handbook of Mathematical Logic—Barwise J, ed. (1977) North Holland. 5–46.
  9. Benton N, Leperchey B. Relational reasoning in a nominal semantics for storage. (2005) Springer. 86–101. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA), Vol. 3461 of Lecture Notes in Computer Science.
  10. Berline C. From computations to foundations via functions and application: the lambdacalculus and its webbed models. Theoretical Computer Science (2000) 249:81–161.[CrossRef][Web of Science]
  11. Berline C. Graph models of lambda-calculus at work, and variations. Mathematical Structures in Computer Science (2006) 16:185–221.[CrossRef][Web of Science]
  12. Bloo R, Rose KH. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: CSN-95: Computer Science in the Netherlands (1995).
  13. Brunner N. 75 years of independence proofs by Fraenkel-Mostowski permutation models. Mathematica Japonica (1996) 43:177–199.
  14. Cheney J. The complexity of equivariant unification. In. In: Proceedings of 31st International Colloquium on Automata, Languages and Programming (ICALP 2004) (2004) Springer. 332–344. Vol. 3142 of Lecture Notes in Computer Science.
  15. Church A. The calculi of lambda-conversion. In: Annals of Mathematics Studies (1941) 6.
  16. Clouston RA, Pitts AM. Nominal equational logic. Electronic Notes in Theoretical Computer Science (2007) 172:223–257.[CrossRef]
  17. Cohn PM. Universal Algebra (1965) Harper and Row.
  18. Coppo M, Dezani-Ciancaglini M, Honsell F, Longo G. Extended type structures and filter lambda-models. In: Proceedings of the Logic Colloquium’82—Lolli G, Longo G, Marcja A, eds. (1984) North-Holland. 241–262.
  19. Curry HB, Feys R. Combinatory Logic (1958) 1. North Holland.
  20. de Bruijn NG. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (1972) 5:381–392.[CrossRef]
  21. Fernández M, Gabbay Murdoch J. Curry-style types for nominal terms. In: Types for Proofs and Programs (Proceedings of TYPES’06) (2007) Springer. 125–139. Vol. 4502 of Lecture Notes in Computer Science.
  22. Fernández M, Gabbay MJ. Nominal rewriting. Information and Computation (2007) 205:917–965.[CrossRef][Web of Science]
  23. Fine K. Reasoning with Arbitrary Objects (1985) Blackwell.
  24. Gabbay MJ. A Theory of Inductive Definitions with alpha-Equivalence (2000) UK: Cambridge. PhD Thesis.
  25. Gabbay MJ. A general mathematics of names. Information and Computation (2007) 205:982–1011.[CrossRef][Web of Science]
  26. Gabbay MJ. Nominal algebra and the HSP theorem. Journal of Logic and Computation (2009) 19:341–367.[Abstract/Free Full Text]
  27. Gabbay MJ, Mathijssen A. Nominal algebra. In. 18th NordicWorkshop on Programming Theory (2006).
  28. Gabbay MJ, Mathijssen A. A formal calculus for informal equality with binding. In: WoLLIC’07: 14th Workshop on Logic, Language, Information and Computation (2007) Springer. 162–176. Vol. 4576 of Lecture Notes in Computer Science.
  29. Gabbay MJ, Mathijssen A. Capture-avoiding substitution as a nominal algebra. Formal Aspects of Computing (2008) 20:451–479.[CrossRef][Web of Science]
  30. Gabbay MJ, Mathijssen A. Nominal (universal) algebra: equational logic with names and binding. Journal of Logic and Computation (2009).
  31. Gabbay MJ, Mathijssen A. One-and-a-halfth-order Logic. Journal of Logic and Computation (2008) 18:521–562.[Abstract/Free Full Text]
  32. Gabbay MJ, Pitts AM. A new approach to abstract syntax with variable binding. Formal Aspects of Computing (2001) 13:341–363.[CrossRef]
  33. Henkin L, Donald Monk J, Tarski A. Cylindric Algebras, Parts I and II (1971, 1985) North Holland.
  34. Johnsson T. Lambda lifting: transforming programs to recursive equations. (1985) Springer. 190–203. In Conference on Functional Programming Languages and Computer Architecture.
  35. Ker AD, Nickau H, Luke Ong C-H. Innocent game models of untyped lambda-calculus. Theoretical Computer Science (2002) 272:247–292.[CrossRef][Web of Science]
  36. Leivant D. Higher order logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming—Gabbay D, Hogger CJ, Robinson JA, eds. (1994) 2. Oxford University Press. 229–322.
  37. Lescanne P. From lambda-sigma to lambda-upsilon: a journey through calculi of explicit substitutions. (1994) ACM Press. 60–69. In Proceedings of 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’94).
  38. Luís Caires LC. A spatial logic for concurrency (part II). Theoretical Computer Science (2004) 322:517–565.[CrossRef][Web of Science]
  39. Mathijssen A. Logical Calculi for Reasoning with Binding (2007) Technische Universiteit Eindhoven. PhDThesis.
  40. Miller D. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation (1991) 1:497–536.[Abstract/Free Full Text]
  41. Nanevski A, Pfenning F, Pientka B. Contextual modal type theory. Proceedings of ACM Transactions on Computational Logic (TOCL) (2008) 9. Article 23.
  42. Paulson LC. ML for theWorking Programmer (2nd edn) (1996) Cambridge University Press.
  43. Paulson LC. The foundation of a generic theorem prover. Journal of Automated Reasoning (1989) 5:363–397.[CrossRef]
  44. Pfenning F, Elliot C. Higher-order abstract syntax. (1988) ACM Press. 199–208. Proceedings of ACMSIGPLAN 1988 conference on Programming Language Design and Implementation (PLDI).
  45. Salibra A. On the algebraic models of lambda calculus. Theoretical Computer Science (2000) 249:197–240.[CrossRef][Web of Science]
  46. Schönfinkel M. On the building blocks of mathematical logic. In: From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931—van Heijenoort J, ed. (1967) Harvard University Press. Translated from [47] by Stefan Bauer-Mengelberg.
  47. Schönfinkel M. Über die bausteine der mathematischen logik. Mathematishe Annalen (1924) 92:305–316.[CrossRef]
  48. Selinger P. The lambda calculus is algebraic. Journal of Functional Programming (2002) 12:549–566.[Web of Science]
  49. Stoy JE. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977) MIT Press.
  50. Takahashi M. Parallel reductions in lambda-calculus. Information and Computation (1995) 1:120–127.
  51. Tan L-Y. Formalizing the meta-theory of Q0 in Rogue-Sigma-Pi. (2005) In 17th European Summer School in Logic, Language and Information (ESSLLI), Student Session.
  52. Thompson S. Haskell: The Craft of Functional Programming (1996) AddisonWesley.
  53. Tzevelekos N. Full abstraction for nominal general references. (2007) IEEE Computer Society. 399–410. In Proceedings of 22th IEEE Symposium on Logic in Computer Science (LICS 2007).
  54. Urban C, Pitts AM, Gabbay MJ. Nominal unification. Theoretical Computer Science (2004) 323:473–497.[CrossRef][Web of Science]

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Gabbay, M. J.
Right arrow Articles by Mathijssen, A.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?