Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2006: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science pp 297–308Cite as

Context-Sensitive Dependency Pairs

  • Conference paper

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

Abstract

Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the dependency pair approach, one of the most powerful techniques for proving termination of rewriting, has not been investigated in connection with proofs of termination of CSR. In this paper, we show how to use dependency pairs in proofs of termination of CSR. The implementation and practical use of the developed techniques yield a novel and powerful framework which improves the current state-of-the-art of methods for proving termination of CSR.

This work has been partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN 2004-7943-C04-02, the Generalitat Valenciana under grant GV06/285, and the ICT for EU-India Cross-Cultural Dissemination ALA/95/23/2003/077-054 project. Beatriz Alarcón was partially supported by the Spanish MEC under FPU grant AP2005-3399.

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. Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Alarcón, B., Gutiérrez, R., Iborra, J., Lucas, S.: Proving Termination of Context-Sensitive Rewriting with MU-TERM. Electronic Notes in Theoretical Computer Science (to appear, 2007)

    Google Scholar 

  3. Borralleras, C., Lucas, S., Rubio, A.: Recursive Path Orderings Can Be Context-Sensitive. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 314–331. Springer, Heidelberg (2002)

    Google Scholar 

  4. Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving Operational Termination of Membership Equational Programs. Higher-Order and Symbolic Computation (to appear, 2006)

    Google Scholar 

  5. Giesl, J., Arts, T., Ohlebusch, E.: Modular Termination Proofs for Rewriting Using Dependency Pairs. Journal of Symbolic Computation 34(1), 21–58 (2002)

    Article  MathSciNet  Google Scholar 

  6. Gramlich, B., Lucas, S.: Simple termination of context-sensitive rewriting. In: Proc. of RULE 2002, pp. 29–41. ACM Press, New York (2002)

    Chapter  Google Scholar 

  7. Giesl, J., Middeldorp, A.: Transforming Context-Sensitive Rewrite Systems. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 271–285. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Giesl, J., Middeldorp, A.: Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming 14(4), 379–427 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  9. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Hirokawa, N., Middeldorp, A.: Dependency Pairs Revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. Lucas, S.: Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998)

    Google Scholar 

  13. Lucas, S.: Context-sensitive rewriting strategies. Information and Computation 178(1), 293–343 (2002)

    MathSciNet  Google Scholar 

  14. Lucas, S.: MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200–209. Springer, Heidelberg (2004), Available at: http://www.dsic.upv.es/~slucas/csr/termination/muterm

    Chapter  Google Scholar 

  15. Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 318–332. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications 39(3), 547–586 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  17. Lucas, S.: Proving termination of context-sensitive rewriting by transformation. Information and Computation (to appear, 2006)

    Google Scholar 

  18. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin (2002)

    MATH  Google Scholar 

  19. TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  20. Zantema, H.: Termination of Context-Sensitive Rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 172–186. Springer, Heidelberg (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DSIC, Universidad Politécnica de Valencia, Spain

    Beatriz Alarcón, Raúl Gutiérrez & Salvador Lucas

Authors
  1. Beatriz Alarcón
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raúl Gutiérrez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Salvador Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology Delhi, P.O. Box, 110016, New Delhi, India

    S. Arun-Kumar

  2. Indian Institute of Technology, Delhi

    Naveen Garg

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alarcón, B., Gutiérrez, R., Lucas, S. (2006). Context-Sensitive Dependency Pairs. In: Arun-Kumar, S., Garg, N. (eds) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2006. Lecture Notes in Computer Science, vol 4337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11944836_28

Download citation

  • DOI: https://doi.org/10.1007/11944836_28

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-49994-7

  • Online ISBN: 978-3-540-49995-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation