Article

A formal treatment of the barendregt variable convention in rule inductions

Authors:

Christian Urban,

Michael NorrishAuthors Info & Claims

MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding

Pages 25 - 32

https://doi.org/10.1145/1088454.1088458

Published: 27 September 2005 Publication History

Get Access

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}.

Digital Library

Google Scholar

[2]

H. Barendregt. The Lambda Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1981.

Google Scholar

[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.

Digital Library

Google Scholar

[4]

J. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986.

Digital Library

Google Scholar

[5]

A. D. Gordon. A mechanisation of name-carrying syntax up to alpha-conversion. In Proceedings of Higher-order Logic Theorem Proving and its Applications (HUG'93), volume 780 of Lecture Notes in Computer Science, pages 414--426. Springer, 1994.

Digital Library

Google Scholar

[6]

A. D. Gordon and T. Melham. Five axioms of alpha conversion. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 173--190. Springer-Verlag, 1996.

Digital Library

Google Scholar

[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.

Google Scholar

[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.

Digital Library

Google Scholar

[9]

J. McKinna and R. Pollack. Some type theory and lambda calculus formalised. Journal of Automated Reasoning, 23(1-4), 1999.

Digital Library

Google Scholar

[10]

M. Norrish. Mechanising λ-calculus using a classical first order theory of terms with permutation. Higher Order and Symbolic Computation. To appear.

Digital Library

Google Scholar

[11]

B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

Digital Library

Google Scholar

[12]

A. M. Pitts. Nominal logic: A first order theory of names and binding. In Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings, volume 2215 of Lecture Notes in Computer Science, pages 219--242. Springer-Verlag, 2001.

Digital Library

Google Scholar

[13]

A. M. Pitts. Alpha-structural recursion and induction (extended abstract). In Hurd and Melham {8}, pages 17--34.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

Cited By

View all

van Brügge JMcKinna JPopescu ATraytel D(2025)Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with BindingsProceedings of the ACM on Programming Languages10.1145/37048939:POPL(1687-1718)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704893
Tasistro ÁCopello ESzasz N(2015)Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda CalculusElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2015.04.013312:C(215-230)Online publication date: 24-Apr-2015
https://dl.acm.org/doi/10.1016/j.entcs.2015.04.013
Popescu AGunter EOsborn C(2010)Strong Normalization for System F by HOAS on Top of FOASProceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.2010.48(31-40)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.1109/LICS.2010.48
Show More Cited By

Index Terms

A formal treatment of the barendregt variable convention in rule inductions
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Machine learning
    1. Machine learning approaches
      1. Rule learning
2. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus

Recommendations

Barendregt's Variable Convention in Rule Inductions
CADE-21: Proceedings of the 21st international conference on Automated Deduction: Automated Deduction

Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt's variable convention is nearly always employed (explicitly or implicitly) in order ...
Psi-Calculi in Isabelle

This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly ...
A formalised first-order confluence proof for the λ-calculus using one-sorted variable names
RTA 2001

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to ...

Comments

Information & Contributors

Information

Published In

MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding

September 2005

72 pages

ISBN:1595930728

DOI:10.1145/1088454

Program Chair:
Randy Pollack
University of Edinburgh, UK

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

MERLIN05

Sponsor:

MERLIN05: Mechanized Reasoning about Languages with Variable Binding 2005 Workshop

September 30, 2005

Tallinn, Estonia

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
226
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)4

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

van Brügge JMcKinna JPopescu ATraytel D(2025)Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with BindingsProceedings of the ACM on Programming Languages10.1145/37048939:POPL(1687-1718)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704893
Tasistro ÁCopello ESzasz N(2015)Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda CalculusElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2015.04.013312:C(215-230)Online publication date: 24-Apr-2015
https://dl.acm.org/doi/10.1016/j.entcs.2015.04.013
Popescu AGunter EOsborn C(2010)Strong Normalization for System F by HOAS on Top of FOASProceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.2010.48(31-40)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.1109/LICS.2010.48
Urban C(2008)Nominal Techniques in Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-008-9097-240:4(327-356)Online publication date: 1-May-2008
https://dl.acm.org/doi/10.1007/s10817-008-9097-2
Bengtson JParrow J(2007)Formalising the π-calculus using nominal logicProceedings of the 10th international conference on Foundations of software science and computational structures10.5555/1760037.1760045(63-77)Online publication date: 24-Mar-2007
https://dl.acm.org/doi/10.5555/1760037.1760045
Pitts AShinwell MHofmann MFelleisen M(2007)Generative unbinding of namesProceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1190216.1190232(85-95)Online publication date: 17-Jan-2007
https://dl.acm.org/doi/10.1145/1190216.1190232
Berdine JChawdhary ACook BDistefano DO'Hearn P(2007)Variance analyses from invariance analysesACM SIGPLAN Notices10.1145/1190215.119024942:1(211-224)Online publication date: 17-Jan-2007
https://dl.acm.org/doi/10.1145/1190215.1190249
Wiedermann BCook W(2007)Extracting queries by static analysis of transparent persistenceACM SIGPLAN Notices10.1145/1190215.119024842:1(199-210)Online publication date: 17-Jan-2007
https://dl.acm.org/doi/10.1145/1190215.1190248
Might M(2007)Logic-flow analysis of higher-order programsACM SIGPLAN Notices10.1145/1190215.119024742:1(185-198)Online publication date: 17-Jan-2007
https://dl.acm.org/doi/10.1145/1190215.1190247
Lee DCrary KHarper R(2007)Towards a mechanized metatheory of standard MLACM SIGPLAN Notices10.1145/1190215.119024542:1(173-184)Online publication date: 17-Jan-2007
https://dl.acm.org/doi/10.1145/1190215.1190245
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Barendregt's Variable Convention in Rule Inductions

Psi-Calculi in Isabelle

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations