Skip to main content
SpringerLink
Log in

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

  • Conference paper
Frontiers of Combining Systems (FroCoS 2011)

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

Included in the following conference series:

Abstract

Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them.

This research is supported by the G.I.F. grant 966-116.6 and by the Netherlands Organisation for Scientific Research (NWO-EW) under grant 612.000.629 (HOT).

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aoto, T., Yamada, T.: Dependency pairs for simply typed term rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 120–134. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Aoto, T., Yamada, T.: Argument filterings and usable rules for simply typed dependency pairs. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 117–132. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47–61. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering: The end of a quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 1–14. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 531–547. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. Journal of Automated Reasoning (to appear, 2011)

    Google Scholar 

  8. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning 40(2-3), 195–220 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  9. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dependency pairs and inductive theorem proving. Journal of Automated Reasoning 47(2), 133–160 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  11. Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems 33 (2011)

    Google Scholar 

  12. Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  15. Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. Applicable Algebra in Engineering, Communication and Computing 5, 131–158 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  16. Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae 24, 3–23 (1995)

    MATH  MathSciNet  Google Scholar 

  17. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1,2), 172–199 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  18. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation 205(4), 474–511 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  19. Hirokawa, N., Middeldorp, A., Zankl, H.: Uncurrying for termination. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 667–681. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Jouannaud, J.-P., Okada, M.: Abstract data type systems. Theoretical Computer Science 173(2), 349–391 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  21. Jouannaud, J.-P., Rubio, A.: The higher-order recursive path ordering. In: Proc. LICS 1999, pp. 402–411 (1999)

    Google Scholar 

  22. Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Comparing curried and uncurried rewriting. Journal of Symbolic Computation 21(1), 15–39 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  23. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121(1-2), 279–308 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  24. Kop, C.: WANDA – a higher order termination tool, http://www.few.vu.nl/~kop/code.html

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

    Chapter  Google Scholar 

  26. Kop, C., van Raamsdonk, F.: Higher-order dependency pairs with argument filterings. In: Proc. WST 2010 (2010), http://www.few.vu.nl/~kop/wst10.pdf

  27. Kop, C., van Raamsdonk, F.: Higher order dependency pairs for algebraic functional systems. In: Proc. RTA 2011. LIPIcs, vol. 10, pp. 203–218. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

    Google Scholar 

  28. Kusakari, K., Sakai, M.: Enhancing dependency pair method using strong computability in simply-typed term rewriting. Applicable Algebra in Engineering, Communication and Computing 18(5), 407–431 (2007)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  30. Ohlebusch, E.: On the modularity of termination of term rewriting systems. Theoretical Computer Science 136(2), 333–360 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  31. Sakai, M., Watanabe, Y., Sakabe, T.: An extension of the dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems E84-D(8), 1025–1032 (2001)

    Google Scholar 

  32. Suzuki, S., Kusakari, K., Blanqui, F.: Argument filterings and usable rules in higher-order rewrite systems. IPSJ Transactions on Programming 4(2), 1–12 (2011)

    Google Scholar 

  33. Tannen, V., Gallier, G.H.: Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science 83(1), 3–28 (1991)

    Article  MATH  Google Scholar 

  34. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  35. Yamada, T.: Confluence and termination of simply typed term rewriting systems. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 338–352. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  36. Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, 52056, Aachen, Germany

    Carsten Fuhs

  2. Vrije Universiteit, De Boelelaan 1081a, 1081 HV, Amsterdam, The Netherlands

    Cynthia Kop

Authors
  1. Carsten Fuhs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cynthia Kop
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Iowa, USA

    Cesare Tinelli

  2. Max-Planck-Institut für Informatik, Campus E 1.4, 66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fuhs, C., Kop, C. (2011). Harnessing First Order Termination Provers Using Higher Order Dependency Pairs. In: Tinelli, C., Sofronie-Stokkermans, V. (eds) Frontiers of Combining Systems. FroCoS 2011. Lecture Notes in Computer Science(), vol 6989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24364-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24364-6_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24363-9

  • Online ISBN: 978-3-642-24364-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation