A formal treatment of the barendregt variable convention in rule inductions

ABSTRACT

Barendregt's variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the variable convention, which makes it hard to formalise such informal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique.

REFERENCES

• 1: B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: the POPLmark challenge. In Hurd and Melham {8}.
• 2: H. Barendregt. The Lambda Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1981.
• 3: M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13:341--363, 2001.
• 4: Jean H. Gallier, Logic for computer science: foundations of automatic theorem proving, Harper & Row Publishers, Inc., New York, NY, 1985
• 5: Andrew D. Gordon, A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.413-425, August 11-13, 1993
• 6: Andrew D. Gordon , Thomas F. Melham, Five Axioms of Alpha-Conversion, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.173-190, August 26-30, 1996
• 7: P. Homeier. A proof of the Church-Rosser theorem for the lambda calculus in higher order logic. In R. J. Boulton and P. B. Jackson, editors, TPHOLs'01: Supplemental Proceedings, pages 207--222. Division of Informatics, University of Edinburgh, September 2001. Available as Informatics Research Report EDI-INF-RR-0046.
• 8: J. Hurd and T. Melham, editors. Theorem Proving in Higher Order Logics, 18th International Conference, volume 3603 of Lecture Notes in Computer Science. Springer, 2005.
• 9: James Mckinna , Robert Pollack, Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, v.23 n.3, p.373-409, November 1999 [doi>10.1023/A:1006294005493 ]
• 10: M. Norrish. Mechanising λ-calculus using a classical first order theory of terms with permutation. Higher Order and Symbolic Computation. To appear.
• 11: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 12: Andrew M. Pitts, Nominal Logic: A First Order Theory of Names and Binding, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.219-242, October 29-31, 2001
• 13: A. M. Pitts. Alpha-structural recursion and induction (extended abstract). In Hurd and Melham {8}, pages 17--34.
• 14: C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In Proc. of the 20th International Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Computer Science, pages 38--53, 2005.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based)

General Terms:
Theory, Verification

Keywords:
λ-calculus, POPLmark challenge, nominal logic