Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Theoretical Aspects of Computing

ICTAC 2006: Theoretical Aspects of Computing - ICTAC 2006 pp 198–212Cite as

Capture-Avoiding Substitution as a Nominal Algebra

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4281))

Abstract

Substitution is fundamental to computer science, underlying for example quantifiers in predicate logic and beta-reduction in the lambda-calculus. So is substitution something we define on syntax on a case-by-case basis, or can we turn the idea of ‘substitution’ into a mathematical object?

We exploit the new framework of Nominal Algebra to axiomatise substitution. We prove our axioms sound and complete with respect to a canonical model; this turns out to be quite hard, involving subtle use of results of rewriting and algebra.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Burris, S., Sankappanavar, H.: A Course in Universal Algebra. Springer, Heidelberg (1981) (available online)

    MATH  Google Scholar 

  2. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323(1–3), 473–497 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  3. Gabbay, M.J., Mathijssen, A.: Nominal algebra. In: STACS 2007 (submitted, 2006)

    Google Scholar 

  4. Gabbay, M.J., Bulò, S.R., Marin, A.: Substitution as an abstract notion: holy functions. In: STACS 2007 (submitted, 2006)

    Google Scholar 

  5. Gabbay, M.J., Mathijssen, A.: One-and-a-halfth-order logic. In: PPDP 2006: Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, pp. 189–200. ACM Press, New York (2006)

    Chapter  Google Scholar 

  6. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13(3–5), 341–363 (2001)

    Google Scholar 

  7. Hodges, W.: Elementary predicate logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 1, pp. 1–131. Kluwer, Dordrecht (2001)

    Google Scholar 

  8. Fernández, M., Gabbay, M.J., Mackie, I.: Nominal rewriting systems. In: Proc. 6th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP 2004), pp. 108–119. ACM, New York (2004)

    Chapter  Google Scholar 

  9. Fernández, M., Gabbay, M.J.: Nominal rewriting. Journal version, Information and Computation (submitted, 2005)

    Google Scholar 

  10. Fernández, M., Gabbay, M.J.: Nominal rewriting with name generation: abstraction vs. locality. In: Proc. 7th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP 2005), pp. 47–58. ACM, New York (2005)

    Chapter  Google Scholar 

  11. Newman, M.: On theories with a combinatorial definition of equivalence. Annals of Mathematics 43(2), 223–243 (1942)

    Article  MathSciNet  Google Scholar 

  12. Groote, J.F.: A new strategy for proving omega-completeness applied to process algebra. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 314–331. Springer, Heidelberg (1990)

    Google Scholar 

  13. Lescanne, P.: From lambda-sigma to lambda-upsilon a journey through calculi of explicit substitutions. In: POPL 1994: Proc. 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60–69. ACM Press, New York (1994)

    Chapter  Google Scholar 

  14. Paulson, L.C.: The foundation of a generic theorem prover. Journal of Automated Reasoning 5(3), 363–397 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  15. Crabbé, M.: Une axiomatisation de la substitution. Comptes rendus de l’Académie des Sciences de Paris, Série I 338, 433–436 (2004)

    MATH  Google Scholar 

  16. Crabbé, M.: On the notion of substitution. Logic Journal of the IGPL 12(2), 111–124 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Feldman, N.: Axiomatization of polynomial substitution algebras. Journal of Symbolic Logic 47(3), 481–492 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  18. Lusin, S., Salibra, A.: The lattice of lambda theories. Journal of Logic and Computation 14(3), 373–394 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  19. Salibra, A.: On the algebraic models of lambda calculus. Theoretical Computer Science 249(1), 197–240 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  20. Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics (revised edn.). Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

  21. Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology, Eindhoven (1997)

    Google Scholar 

  22. de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae 5(34), 381–392 (1972)

    Google Scholar 

  23. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Extensions of Logic Programming 475, 253–281 (1991)

    Article  Google Scholar 

  24. Huet, G.: Higher order unification 30 years later (Extended abstract). In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 3–12. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Gabbay, M.J.: A new calculus of contexts. In: Proc. 7th Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP 2005). ACM, New York (2005)

    Google Scholar 

  26. Gabbay, M.J.: Hierarchical nominal rewriting. In: LFMTP 2006, pp. 32–47 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Murdoch J. Gabbay

  2. Department of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB, Eindhoven, The Netherlands

    Aad Mathijssen

Authors
  1. Murdoch J. Gabbay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aad Mathijssen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 192 rue Saint Martin, Paris Cedex 03, France

    Kamel Barkaoui

  2. Department of Computer Science, University of York, York, UK

    Ana Cavalcanti

  3. UNU-IIST, Macau SAR, China

    Antonio Cerone

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gabbay, M.J., Mathijssen, A. (2006). Capture-Avoiding Substitution as a Nominal Algebra. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_14

Download citation

  • DOI: https://doi.org/10.1007/11921240_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-48815-6

  • Online ISBN: 978-3-540-48816-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation