Skip to main content
SpringerLink
Log in

Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems

  • Conference paper
  • First Online:
Book cover Interactive Theorem Proving (ITP 2016)

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

Included in the following conference series:

Abstract

This paper presents the first formalization of three classic confluence criteria for first-order term rewrite systems by Huet and Toyama. We have formalized proofs, showing that (1) linear strongly closed systems, (2) left-linear parallel closed systems, and (3) left-linear almost parallel closed systems are confluent. The third result is extended to commutation. The proofs were carried out in the proof assistant Isabelle/HOL as part of the library IsaFoR and integrated into the certifier CeTA, significantly increasing the number of certifiable proofs produced by automatic confluence tools.

This work is supported by FWF (Austrian Science Fund) project P27528.

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 EPUB and 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

Notes

  1. 1.

    http://coco.nue.riec.tohoku.ac.jp/.

  2. 2.

    IsaFoR/CeTA and CPF are available at http://cl-informatik.uibk.ac.at/software/ceta/.

  3. 3.

    We do not impose the common variable conditions, i.e., the restriction that \(\ell \) is not a variable and all variables in r are contained in \(\ell \).

  4. 4.

    This bound is necessary to ensure termination of the certifier.

  5. 5.

    http://cops.uibk.ac.at.

References

  1. Aoto, T.: Disproving confluence of term rewriting systems by interpretation and ordering. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 311–326. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40885-4_22

    Chapter  Google Scholar 

  2. Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93–102. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02348-4_7

    Chapter  Google Scholar 

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

    Book  MATH  Google Scholar 

  4. Blanqui, F., Koprowski, A.: CoLoR, a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827–859 (2011). doi:10.1017/S0960129511000120

    Article  MathSciNet  MATH  Google Scholar 

  5. Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10. pp. 21–30. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2011). doi:10.4230/LIPIcs.RTA.2011.21

  6. Felgenhauer, B., Thiemann, R.: Reachability analysis with state-compatible automata. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 347–359. Springer, Heidelberg (2014). doi:10.1007/978-3-319-04921-2_28

    Chapter  Google Scholar 

  7. Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in the term rewriting, part 2: The confluence hierarchy. Inf. Comput. 178(1), 132–148 (2002). doi:10.1006/inco.2002.3150

    Article  MathSciNet  MATH  Google Scholar 

  8. Hirokawa, N., Klein, D.: Saigawa: a confluence tool. In: Hirokawa, N., Middeldorp, A. (eds.) IWC 2012, p. 49 (2012). http://cl-informatik.uibk.ac.at/events/iwc-2012/

  9. Hirokawa, N., Middeldorp, A.: Commutation via relative termination. In: Hirokawa, N., van Oostrom, V. (eds.) IWC 2013, pp. 29–33 (2013). http://www.jaist.ac.jp/~hirokawa/iwc2013/

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

    Article  MathSciNet  MATH  Google Scholar 

  11. Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 258–273. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_21

    Chapter  Google Scholar 

  12. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)

    Google Scholar 

  13. Nagele, J., Felgenhauer, B., Middeldorp, A.: Improving automatic confluence analysis of rewrite systems by redundant rules. In: Fernández, M. (ed.) RTA 2015. LIPIcs, vol. 36, pp. 257–268. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2015). doi:10.4230/LIPIcs.RTA.2015.257

  14. Nagele, J., Thiemann, R.: Certification of confluence proofs using CeTA. In: Aoto, T., Kesner, D. (eds.) IWC 2014, pp. 19–23 (2014). http://www.nue.riec.tohoku.ac.jp/iwc2014/

  15. Nagele, J., Zankl, H.: Certified rule labeling. In: Fernández, M. (ed.) RTA 2015. LIPIcs, vol. 36, pp. 269–284. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2015). doi:10.4230/LIPIcs.RTA.2015.269

  16. Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  17. van Oostrom, V.: Developing developments. Theoret. Comput. Sci. 175(1), 159–181 (1997). doi:10.1016/S0304-3975(96)00173-9

    Article  MathSciNet  MATH  Google Scholar 

  18. Shintani, K., Hirokawa, N.: CoLL: A confluence tool for left-linear term rewrite systems. In: Felty, A., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 127–136. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21401-6_8

    Google Scholar 

  19. Sternagel, C., Thiemann, R.: The certification problem format. In: Benzmüller, C., Woltzenlogel Paleo, B. (eds.) UITP 2014. EPTCS, vol. 167, pp. 61–72. Open Publishing Association (2014). doi:10.4204/EPTCS.167.8

    Google Scholar 

  20. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical ComputerScience, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  21. Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_31

    Chapter  Google Scholar 

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

    Google Scholar 

  23. Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – a confluence tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 499–505. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_38

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank Nao Hirokawa for suggesting Lemma 6 and Bertram Felgenhauer and Christian Sternagel for insightful discussion.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Innsbruck, Innsbruck, Austria

    Julian Nagele & Aart Middeldorp

Authors
  1. Julian Nagele
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Julian Nagele .

Editor information

Editors and Affiliations

  1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Jasmin Christian Blanchette

  2. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Stephan Merz

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Nagele, J., Middeldorp, A. (2016). Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-43144-4_18

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation