Advertisement

Journal of Automated Reasoning

, Volume 49, Issue 2, pp 185–207 | Cite as

A Canonical Locally Named Representation of Binding

  • Randy Pollack
  • Masahiko Sato
  • Wilmer Ricciotti
Article

Abstract

This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables (Sato and Pollack, J Symb Comput 45:598–616, 2010). The present paper differs from our previous work by being more abstract. Whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal Isabelle representation of pure lambda terms. This metatheory is formalized in Isabelle/HOL. The final section outlines a formalization in Matita of a challenging language with multiple binding and simultaneous substitution. The Isabelle and Matita proof files are available online.

Keywords

Binding Lambda calculus Formal proof 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ambler, S.J., Crole, R.L., Momigliano, A.: A definitional approach to primitive recursion over higher order abstract syntax. In: MERLIN ’03: Proceedings of the 2003 Workshop on Mechanized Reasoning About Languages with Variable Binding, pp. 1–11. ACM Press (2003)Google Scholar
  2. 2.
    Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles on Programming Languages, pp. 3–15. ACM Press (2008)Google Scholar
  3. 3.
    Bengtson, J., Parrow, J.: Psi-calculi in isabelle. In: TPHOLs. LNCS, vol. 5674 (2009)Google Scholar
  4. 4.
    Berghofer, S., Urban, C.: Nominal inversion principles. In: Theorem Proving in Higher Order Logics, TPHOLs 2008. LNCS. Springer-Verlag (2008)Google Scholar
  5. 5.
    Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North Holland (1958)Google Scholar
  6. 6.
    de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math., 34(5), 381–392 (1972)Google Scholar
  7. 7.
    Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle (1879) (Translated in van Heijenoort, J.: From Frege to Gödel: a source book in mathematical logic, 1879–1931, pp. 1-82. Harvard University Press, Cambridge, MA (1967))Google Scholar
  8. 8.
    Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: Longo, G. (ed.) Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99), pp. 214–224 (1999)Google Scholar
  9. 9.
    Gentzen, G.: Untersuchungen über das logische schliessen. Math. Zeitschrift 39, 176–210 (1934) (English translation in Szabo, M.E. (ed.): The Collected Papers of Gerhard Gentzen. North Holland (1969))MathSciNetCrossRefGoogle Scholar
  10. 10.
    Gordon, A.: A mechanism of name-carrying syntax up to alpha-conversion. In: Higher Order Logic Theorem Proving and its Applications. Proceedings, 1993. LNCS 780, pp. 414–426. Springer-Verlag (1993)Google Scholar
  11. 11.
    Gordon, A., Melham, T.: Five axioms of alpha conversion. In: Von Wright, J., Grundy, J., Harrison, J. (eds.) Ninth Conference on Theorem Proving in Higher Order Logics TPHOL’96, Turku. LNCS, vol. 1125, pp. 173–190. Springer-Verlag (1996)Google Scholar
  12. 12.
    Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993) (Preliminary version in LICS’87)MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4–5) (2007)Google Scholar
  14. 14.
    Honsell, F., Miculan, M., Scagnetto, I.: The theory of contexts for first order and higher order abstract syntax. Electronic Notes Theor. Comp. Sci. 62, 116–135 (2002)CrossRefGoogle Scholar
  15. 15.
    McKinna, J., Pollack, R.: Pure type systems formalized. In: Bezem, M., Groote, J.F. (eds.) Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA’93, Utrecht. LNCS, number 664, pp. 289–305. Springer-Verlag (1993)Google Scholar
  16. 16.
    McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reason. 23(3–4), 373–409 (1999)MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Pfenning, F., Schürmann, C.: System description: twelf: a meta-logical framework for deductive systems. In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16). LNAI, Springer-Verlag (1999)Google Scholar
  18. 18.
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186, 165–193 (2003)MathSciNetMATHCrossRefGoogle Scholar
  19. 19.
    Pollack, R.: The theory of LEGO: a proof checker for the extended calculus of constructions. Ph.D. thesis, Univ. of Edinburgh (1994)Google Scholar
  20. 20.
    Pottinger, G.: A tour of the multivariate lambda calculus. In: Dunn, J.M., Gupta, A. (eds.) Truth or Consequences: Essays in Honor of Nuel Belnap. Kluwer (1990)Google Scholar
  21. 21.
    Prawitz, D.: Natural Deduction: Proof Theoretical Study. Almquist and Wiksell, Stockholm (1965)MATHGoogle Scholar
  22. 22.
    Sato, M.: External and internal syntax of the λ-calculus. In: Buchberger, B., Ida, T., Kutsia, T. (eds.) Proc. of the Austrian-Japanese Workshop on Symbolic Computation in Software Science, SCSS 2008. RISC-Linz Report Series, number 08–08, pp. 176–195 (2008)Google Scholar
  23. 23.
    Sato, M., Pollack, R.: External and internal syntax of the λ-calculus. J. Symb. Comput. 45, 598–616 (2010)MathSciNetMATHCrossRefGoogle Scholar
  24. 24.
    Stoughton, A.: Substitution revisited. Theor. Comp. Sci. 17, 317–325 (1988)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: Automated Deduction—CADE-21. LNCS, number 4603, pp. 35–50. Springer-Verlag (2007)Google Scholar
  26. 26.
    Urban, C.: Nominal techniques in isabelle/hol. J. Autom. Reason. 40(4), 327–356 (2008)MathSciNetMATHCrossRefGoogle Scholar
  27. 27.
    Urban, C., Pollack, R.: Strong induction principles in the locally nameless representation of binders (preliminary notes). Presented at (ACM) Workshop on Mechanizing Metatheory (2007)Google Scholar
  28. 28.
    van Heijenoort, J.: From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press, Cambridge, MA (1967)MATHGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2011

Authors and Affiliations

  • Randy Pollack
    • 1
  • Masahiko Sato
    • 2
  • Wilmer Ricciotti
    • 3
  1. 1.LFCS, School of InformaticsUniversity of EdinburghEdinburghUnited Kingdom
  2. 2.Graduate School of InformaticsKyoto UniversityKyotoJapan
  3. 3.Department of Computer ScienceUniversity of BolognaBolognaItaly

Personalised recommendations