Skip to main content
SpringerLink
Log in

Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10483))

Included in the following conference series:

Abstract

Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not \(\alpha \)-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.

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 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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

References

  1. Aoto, T., Kikuchi, K.: Nominal confluence tool. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 173–182. Springer, Cham (2016). doi:10.1007/978-3-319-40229-1_12

    Google Scholar 

  2. Aoto, T., Kikuchi, K.: A rule-based procedure for equivariant nominal unification. In: Proceedings of the 8th HOR (2016)

    Google Scholar 

  3. Ayala-Rincón, M., Fernández, M., Gabbay, M.J., Rocha-Oliveira, A.C.: Checking overlaps of nominal rewriting rules. Electron. Notes Theoret. Comput. Sci. 323, 39–56 (2016)

    Article  MathSciNet  Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  5. 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 34, 381–392 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  6. Cheney, J.: Equivariant unification. J. Autom. Reasoning 45, 267–300 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  7. Comon, H.: Completion of rewritie systems with membership constraints. Part I: deduction rules. J. Symbolic Comput. 25, 397–419 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  8. Fernández, M., Gabbay, M.J.: Nominal rewriting. Inform. Comput. 205, 917–965 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects Comput. 13, 341–363 (2002)

    Article  MATH  Google Scholar 

  10. Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27, 797–821 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  11. Jounnaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15, 1155–1194 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  12. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoret. Comput. Sci. 121, 279–308 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  13. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoret. Comput. Sci. 192, 3–29 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  14. Ohlebusch, E.: Church-Rosser theorems for abstract reduction modulo an equivalence relation. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 17–31. Springer, Heidelberg (1998). doi:10.1007/BFb0052358

    Chapter  Google Scholar 

  15. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002). doi:10.1007/978-1-4757-3661-8

    Book  MATH  Google Scholar 

  16. van Oostrom, V.: Developing developments. Theoret. Comput. Sci. 175, 159–181 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inform. Comput. 186, 165–193 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  18. Pollack, R., Sato, M., Ricciotti, W.: A canonical locally named representation of binding. J. Autom. Reasoning 49, 185–207 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  19. Suzuki, T., Kikuchi, K., Aoto, T., Toyama, Y.: Confluence of orthogonal nominal rewriting systems revisited. In: Proceedings of the 26th RTA, vol. 36. LIPIcs, pp. 301–317 (2015)

    Google Scholar 

  20. Suzuki, T., Kikuchi, K., Aoto, T., Toyama, Y.: Critical pair analysis in nominal rewriting. In: Proceedings of the 7th SCSS, vol. 39. EPiC, pp. 156–168. EasyChair (2016)

    Google Scholar 

  21. Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, North-Holland, pp. 393–407 (1988)

    Google Scholar 

  22. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoret. Comput. Sci. 323, 473–497 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  23. Vestergaard, R., Brotherston, J.: A formalised first-order confluence proof for the \(\lambda \)-calculus using one-sorted variable names. Inform. Comput. 183, 212–244 (2003)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We are grateful to the anonymous referees for valuable comments. This research was supported by JSPS KAKENHI Grant Numbers 15K00003 and 16K00091.

Author information

Authors and Affiliations

  1. RIEC, Tohoku University, Sendai, Japan

    Kentaro Kikuchi & Yoshihito Toyama

  2. Faculty of Engineering, Niigata University, Niigata, Japan

    Takahito Aoto

Authors
  1. Kentaro Kikuchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Takahito Aoto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yoshihito Toyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kentaro Kikuchi .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, United Kingdom

    Clare Dixon

  2. University of Sao Paulo, Sao Paulo, Brazil

    Marcelo Finger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Kikuchi, K., Aoto, T., Toyama, Y. (2017). Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems. In: Dixon, C., Finger, M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science(), vol 10483. Springer, Cham. https://doi.org/10.1007/978-3-319-66167-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66167-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66166-7

  • Online ISBN: 978-3-319-66167-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation