Skip to main content
SpringerLink
Log in

Relating Nominal and Higher-Order Rewriting

  • Conference paper
Book cover Mathematical Foundations of Computer Science 2014 (MFCS 2014)

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

  • 674 Accesses

Abstract

We present a translation function from nominal rewriting systems (NRSs) to combinatory reduction systems (CRSs), transforming closed nominal rules and ground nominal terms to CRSs rules and terms while preserving the rewriting relation. This result, together with previous translations from CRSs to NRSs and between CRSs and other higher-order rewriting formalisms, opens up the path for a transfer of results between higher-order and nominal rewriting. In particular, techniques and properties of the rewriting relation, such as termination, can be exported from one formalism to the other.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Nipkow, T.: Term Rewriting and all that. CUP (1988)

    Google Scholar 

  2. Dershowitz, N.: Terese: Term Rewrite Systems. CAMTCS, vol. 55. CUP (2003)

    Google Scholar 

  3. Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics, Revised edn. Studies in Log. and the Found. of Math. North-Holland, vol. 103 (1984)

    Google Scholar 

  4. Klop, J.W.: Combinatory reduction systems. PhD thesis, Utrecht University (1980)

    Google Scholar 

  5. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comp. Sci. 121, 279–308 (1993)

    Article  MATH  Google Scholar 

  6. Nipkow, T.: Higher-order critical pairs. In: LICS, pp, 342–349 (1991)

    Google Scholar 

  7. Khasidashvili, Z.: Expression reduction systems. In: Proc. of I. Vekua Institute of Applied Mathematics, vol. 36, pp. 200–220 (1990)

    Google Scholar 

  8. Glauert, J., Kesner, D., Khasidashvili, Z.: Expression reduction systems and extensions: An overview. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes... (Klop Festschrift). LNCS, vol. 3838, pp. 496–553. Springer, Heidelberg (2005)

    Google Scholar 

  9. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comp. Sci. 192(1), 3–29 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  10. Hamana, M.: Semantic labelling for proving termination of combinatory reduction systems. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol. 5979, pp. 62–78. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Nipkow, T., Prehofer, C.: Higher-order rewriting and equational reasoning. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction — A Basis for Applications. Volume I: Foundations. J. of App. Log., vol. 8, pp. 399–430. Kluwer (1998)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  13. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  14. Fernández, M., Gabbay, M.J.: Nominal rewriting. Inf. Comput. 205(6), 917–965 (2007)

    Article  MATH  Google Scholar 

  15. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comp. Sci. 323(13), 473–497 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  16. Calvès, C., Fernández, M.: Matching and alpha-equivalence check for nominal terms. J. of Comp. and Syst. Sci. (2009); Special issue: Selected papers from WOLLIC 2008

    Google Scholar 

  17. Cheney, J.: Relating nominal and higher-order pattern unification. In: Proc. of UNIF, pp. 104–119 (2005)

    Google Scholar 

  18. Fernández, M., Gabbay, M.J., Mackie, I.: Nominal rewriting systems. In: Proc. of 6th ACM SIGPLAN, PPDP 2004, pp. 108–119. ACM, New York (2004)

    Google Scholar 

  19. Levy, J., Villaret, M.: Nominal unification from a higher-order perspective. ACM Trans. Comput. Logic 13(2), 10:1–10:31 (2012)

    Google Scholar 

  20. Fernández, M., Rubio, A.: Nominal completion for rewrite systems with binders. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 201–213. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. Domínguez, J.: A tool to apply nominal recursive path ordering to nominal rules (2014), http://www.inf.kcl.ac.uk/pg/domijesu/nrpo.tgz

  22. Domínguez, J.: A tool to translate between closed nominal rewriting systems and combinatory reduction systems (2014), http://www.inf.kcl.ac.uk/pg/domijesu/NRS2CRS.tar.gz

  23. van Oostrom, V., van Raamsdonk, F.: Comparing combinatory reduction systems and higher-order rewrite systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, pp. 276–304. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  24. Bertolissi, C., Cirstea, H., Kirchner, C.: Expressing combinatory reduction systems derivations in the rewriting calculus. Higher-Ord. and Symb. Comp. 19, 00110869 (2006)

    Google Scholar 

  25. Cirstea, H., Kirchner, C.: The rewriting calculus — Part I. J. of Pure and App. Logs. 9(3), 427–463 (2001)

    MathSciNet  Google Scholar 

  26. Cirstea, H., Kirchner, C.: The rewriting calculus - Part II. IGPL 9(3), 377–410 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  27. Bognar, M.: Contexts in Lambda Calculus. PhD thesis, Vrije Universiteit Amsterdam (2002)

    Google Scholar 

  28. van Raamsdonk, F.: Higher-order rewriting. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 220–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  29. Kop, C.: Simplifying algebraic functional systems. In: Winkler, F. (ed.) CAI 2011. LNCS, vol. 6742, pp. 201–215. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  30. Jouannaud, J.-P.: Higher-order rewriting: Framework, confluence and termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes... (Klop Festschrift). LNCS, vol. 3838, pp. 224–250. Springer, Heidelberg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, King’s College London, Strand, WC2R 2LS, UK

    Jesús Domínguez & Maribel Fernández

Authors
  1. Jesús Domínguez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maribel Fernández
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Eötvös Loránd University, Pázmány Péter sétány 1/C, 1117, Budapest, Hungary

    Erzsébet Csuhaj-Varjú

  2. Fakultät für Informatik und Automatisierung, Technische Universität Ilmenau, Helmholtzplatz, 598693, Ilmenau, Germany

    Martin Dietzfelbinger

  3. Institute of Informatics, Szeged University, Tisza Lajos krt. 103, 6720, Szeged, Hungary

    Zoltán Ésik

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag GmbH Berlin Heidelberg

About this paper

Cite this paper

Domínguez, J., Fernández, M. (2014). Relating Nominal and Higher-Order Rewriting. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44522-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-44522-8_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-44521-1

  • Online ISBN: 978-3-662-44522-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation