[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Usable Rules for Context-Sensitive Rewrite Systems

  • Conference paper
Rewriting Techniques and Applications (RTA 2008)

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

Included in the following conference series:

  • 373 Accesses

Abstract

Recently, the dependency pairs (DP) approach has been generalized to context-sensitive rewriting (CSR). Although the context-sensitive dependency pairs (CS-DP) approach provides a very good basis for proving termination of CSR, the current developments basically correspond to a ten-years-old DP approach. Thus, the task of adapting all recently introduced dependency pairs techniques to get a more powerful approach becomes an important issue. In this direction, usable rules are one of the most interesting and powerful notions. Actually usable rule have been investigated in connection with proofs of innermost termination of CSR. However, the existing results apply to a quite restricted class of systems. In this paper, we introduce a notion of usable rules that can be used in proofs of termination of CSR with arbitrary systems. Our benchmarks show that the performance of the CS-DP approach is much better when such usable rules are considered in proofs of termination of CSR.

Work partially supported by the EU (FEDER) and the Spanish MEC, under grants TIN 2004-7943-C04-02, TIN 2007-68118-C02 and HA 2006-0007.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alarcón, B., Gutiérrez, R., Iborra, J., Lucas, S.: Proving Termination of Context-Sensitive Rewriting with MU-TERM. ENTCS 188, 105–115 (2007)

    Google Scholar 

  2. Alarcón, B., Gutiérrez, R., Lucas, S.: Context-Sensitive Dependency Pairs. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 297–308. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Alarcón, B., Gutiérrez, R., Lucas, S.: Improving the Context-Sensitive Dependency Graph. ENTCS 188, 91–103 (2007)

    Google Scholar 

  4. Alarcón, B., Lucas, S.: Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 73–87. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Arts, T., Giesl, J.: Proving Innermost Normalisation Automatically. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 157–171. Springer, Heidelberg (1997)

    Google Scholar 

  6. Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236(1–2), 133–178 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  7. Borralleras, C.: Ordering-Based Methods for Proving Termination Automatically. PhD thesis, Departament de Llenguatges i Sistemes Informàtics, UPC (2003)

    Google Scholar 

  8. 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, 2008)

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

  11. Giesl, J., Middeldorp, A.: Innermost Termination of Context-Sensitive Rewriting. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol. 2450, pp. 231–244. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Giesl, J., Middeldorp, A.: Transformation Techniques for Context-Sensitive Rewrite Systems. Journal of Functional Programming 14(4), 379–427 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  13. 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 (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Google Scholar 

  14. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. Journal of Automatic Reasoning 37(3), 155–203 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Gramlich, B.: Generalized Sufficient Conditions for Modular Termination of Rewriting. Applicable Algebra in Engineering, Communication and Computing 5, 131–151 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  16. Gutiérrez, R., Lucas, S., Urbain, X.: Usable Rules for Context-Sensitive Rewrite System, DSIC-II/03/08. Technical report, UPV (2008)

    Google Scholar 

  17. Hirokawa, N., Middeldorp, A.: Tyrolean Termination Tool: Techniques and Features. Information and Computation 205(4), 474–511 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  18. Lucas, S.: Context-Sensitive Computations in Functional and Functional Logic Programs. Journal of Functional and Logic Programming 1998(1), 1–61 (1998)

    Google Scholar 

  19. Lucas, S.: Termination of on-demand rewriting and termination of OBJ programs. In: Proc. of PPDP 2001, pp. 82–93. ACM Press, New York (2001)

    Chapter  Google Scholar 

  20. Lucas, S.: Context-Sensitive Rewriting Strategies. Information and Computation 178(1), 293–343 (2002)

    MathSciNet  Google Scholar 

  21. 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), http://zenon.dsic.upv.es/muterm/

    Google Scholar 

  22. Lucas, S.: Proving Termination of Context-Sensitive Rewriting by Transformation. Information and Computation 204(12), 1782–1846 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  23. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  24. Urbain, X.: Modular & Incremental Automated Termination Proofs. Journal of Automated Reasoning 32(4), 315–355 (2004)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Raúl Gutiérrez & Salvador Lucas

  2. Cédric-CNAM, ENSIIE, France

    Xavier Urbain

Authors
  1. Raúl Gutiérrez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Salvador Lucas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xavier Urbain
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gutiérrez, R., Lucas, S., Urbain, X. (2008). Usable Rules for Context-Sensitive Rewrite Systems. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70590-1_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70588-8

  • Online ISBN: 978-3-540-70590-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation