Skip to main content
SpringerLink
Log in

Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting

  • Chapter
  • First Online:
Logic, Rewriting, and Concurrency

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

Abstract

Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions of subterms that can be rewritten; or frozen, i.e., positions that cannot. Frozen positions can be used to denote subexpressions whose evaluation is delayed or just forbidden. A typical example is the if-then-else operator whose second and third arguments are not evaluated until the evaluation of the first argument yields either true or false. Imposing replacement restrictions can improve the termination behavior of rewriting-based computational systems. Termination of CSR has been investigated by several authors and a number of automatic tools are able to prove it. In this paper, we analyze how frozen subterms affect termination of CSR. This analysis helps us to improve our Context-Sensitive Dependency Pair (CS-DP) framework for automatically proving termination of CSR. We have implemented these improvements in our tool mu-term. The experiments show the power of the improvements in practice.

Partially supported by the EU (FEDER), MINECO project TIN 2013-45732-C4-1-P, and GV project PROMETEO/2011/052. Salvador Lucas’ research was developed during a sabbatical year at the CS Dept. of the UIUC and was also partially supported by NSF grant CNS 13-19109. Raúl Gutiérrez is also partially supported by a Juan de la Cierva Fellowship from the Spanish MINECO, ref. JCI-2012-13528.

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.

    The notion of context-sensitive rewriting was developed as part of Lucas’ Master Thesis (1994) to implement concurrent programming languages that, like the \(\pi \)-calculus, forbid reductions on some arguments of its operations.

  2. 2.

    Note that minimal non-\(\mu \)-terminating terms may contain minimal non-\(\mu \)-terminating terms (at frozen positions, though). We use darker shades for such nested minimal non-\(\mu \)-terminating terms.

  3. 3.

    In order to keep our presentation simple, we do not introduce here the notions related with completeness of processors, needed for nontermination proofs.

  4. 4.

    A binary relation \(\mathsf{R}\) on terms is \(\mu \)-monotonic if for all terms \(s, t, t_1,\ldots ,t_m\), and m-ary symbols f, whenever \(s\,\mathsf{R}\,t\) and \(i \in \mu (f)\) we have \(f(\ldots ,t_{i-1},s,\ldots )\,\mathsf{R}\, f(\ldots ,t_{i-1},t,\ldots )\).

  5. 5.

    See http://termcomp.uibk.ac.at/termcomp/.

References

  1. Alarcón, B., Emmes, F., Fuhs, C., Giesl, J., Gutiérrez, R., Lucas, S., Schneider-Kamp, P., Thiemann, R.: Improving context-sensitive dependency pairs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 636–651. Springer, Heidelberg (2008)

    Chapter  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.: Context-Sensitive dependency pairs. Inf. Comput. 208, 922–968 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 151–171. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  6. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)

    Article  MathSciNet  MATH  Google Scholar 

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

    Book  MATH  Google Scholar 

  8. Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P., Ringeissen, C.: An overview of ELAN. Electr. Notes Theor. Comput. Sci. 15, 55–70 (1998). http://dx.doi.org/10.1016/S15710661(05)825526

    Article  MATH  Google Scholar 

  9. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  10. Emmes, F.: Automated Termination Analysis of Context-Sensitive Term Rewrite Systems. Master’s thesis, Fakultät für Mathematik, Informatik und Naturwissenschaften der Rheinisch-Westfälischen Technischen Hochschule Aachen, Aachen, Germany (2008)

    Google Scholar 

  11. Futatsugi, K., Goguen, J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1985, pp. 52–66. ACM (1985)

    Google Scholar 

  12. Futatsugi, K., Nakagawa, A.: An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: Proceedings of the 1st International Conference on Formal Engineering Methods, ICFEM 1997, p. 170. IEEE Computer Society (1997)

    Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer, Boston (2000). chap. Introducing OBJ

    Book  Google Scholar 

  16. Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. Appl. Algebra Eng. Commun. Comput. 5, 131–151 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  17. Gutiérrez, R., Lucas, S.: Proving termination in the context-sensitive dependency pair framework. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 18–34. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Gutiérrez, R., Lucas, S.: Function calls at frozen positions in termination of context-sensitive rewriting. Technical report, DSIC, Universitat Politècnica de València, May 2015. http://hdl.handle.net/10251/50750

  19. Gutiérrez, R., Lucas, S., Urbain, X.: Usable rules for context-sensitive rewrite systems. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 126–141. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

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

  22. Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: techniques and features. Inf. Comput. 205(4), 474–511 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  23. Lucas, S.: Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998(1), 1–61 (1998)

    MathSciNet  MATH  Google Scholar 

  24. Lucas, S.: Termination of on-demand rewriting and termination of OBJ programs. In: De Nicola, R., Søndergaard, H. (eds.) Proceedings of the 3rd Internatinal Conference on Principles and Practice of Declarative Programming, PPDP 2001, pp. 82–93. ACM Press (2001)

    Google Scholar 

  25. Lucas, S.: Termination of rewriting with strategy annotations. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 666–680. Springer, Heidelberg (2001)

    Google Scholar 

  26. Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inf. Appl. 39(3), 547–586 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  27. Lucas, S.: Completeness of context-sensitive rewriting. Inf. Process. Lett. 115(2), 87–92 (2015). http://dx.doi.org/10.1016/j.ipl.2014.07.004

    Article  MathSciNet  MATH  Google Scholar 

  28. Ohlebusch, E.: On the modularity of termination of term rewriting systems. Theor. Comput. Sci. 136, 333–360 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  29. Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DSIC, Universitat Politècnica de València, Camino de Vera S/N, 46022, Valencia, Spain

    Raúl Gutiérrez & Salvador Lucas

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

Corresponding author

Correspondence to Raúl Gutiérrez .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Gutiérrez, R., Lucas, S. (2015). Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation