A nominal axiomatization of the lambda calculus

Murdoch Gabbay, Aad Mathijssen

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)501-531
Number of pages31
JournalJournal of Logic and Computation
Volume20
Issue number2
DOIs
Publication statusPublished - Apr 2010

Keywords

  • Equational logic
  • Lambda calculus
  • Nominal techniques

Fingerprint Dive into the research topics of 'A nominal axiomatization of the lambda calculus'. Together they form a unique fingerprint.

Cite this