Skip to main content
SpringerLink
Log in

Natural Narrowing for General Term Rewriting Systems

  • Conference paper
Term Rewriting and Applications (RTA 2005)

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

Included in the following conference series:

Abstract

For narrowing to be an efficient evaluation mechanism, several lazy narrowing strategies have been proposed, although typically for the restricted case of left-linear constructor systems. These assumptions, while reasonable for functional programming applications, are too restrictive for a much broader range of applications to which narrowing can be fruitfully applied, including applications where rules have a non-equational meaning either as transitions in a concurrent system or as inferences in a logical system. In this paper, we propose an efficient lazy narrowing strategy called natural narrowing which can be applied to general term rewriting systems with no restrictions whatsoever. An important consequence of this generalization is the wide range of applications that can now be efficiently supported by narrowing, such as symbolic model checking and theorem proving.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Antoy, S.: Definitional trees. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 143–157. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  2. Antoy, S.: Constructor-based conditional narrowing. In: Proc. of PPDP 2001, pp. 199–206. ACM, New York (2001)

    Chapter  Google Scholar 

  3. Antoy, S., Echahed, R., Hanus, M.: Parallel evaluation strategies for functional logic languages. In: Proc. of ICLP 1997, pp. 138–152. MIT Press, Cambridge (1997)

    Google Scholar 

  4. Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. Journal of the ACM 47(4), 776–822 (2000)

    Article  MathSciNet  Google Scholar 

  5. Antoy, S., Lucas, S.: Demandness in rewriting and narrowing. In: Proc. of WFLP 2002. ENTCS, vol. 76, Elsevier, Amsterdam (2002)

    Google Scholar 

  6. Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 285, 155–185 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  7. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  8. Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 913–962. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  9. Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation 159(1/2), 151–186 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  10. Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996)

    MATH  Google Scholar 

  11. Escobar, S.: Refining weakly outermost-needed rewriting and narrowing. In: Proc. of PPDP 2003, pp. 113–123. ACM, New York (2003)

    Chapter  Google Scholar 

  12. Escobar, S.: Implementing natural rewriting and narrowing efficiently. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 147–162. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Escobar, S., Meseguer, J., Thati, P.: Natural narrowing as a general unified mechanism for programming and proving. Technical Report DSIC-II/16/04, DSIC, Universidad Politécnica de Valencia (2004), Available at http://www.dsic.upv.es/users/elp/papers.html

  14. Escobar, S., Meseguer, J., Thati, P.: Natural rewriting for general term rewriting systems. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 101–116. Springer, Heidelberg (2005) (to appear)

    Chapter  Google Scholar 

  15. Fay, M.: First order unification in equational theories. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 161–167. Springer, Heidelberg (1980)

    Google Scholar 

  16. Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific, Singapore (1998)

    MATH  Google Scholar 

  17. Giovannetti, E., Levi, G., Moiso, C., Palamidessi, C.: Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences 42(2), 139–185 (1991)

    Article  MATH  Google Scholar 

  18. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer, Dordrecht (2000)

    Google Scholar 

  19. González-Moreno, J.C., Hortalá-González, M.T., López-Fraguas, F.J., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. Journal of Logic Programming 40(1), 47–87 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  20. Hanus, M.: The integration of functions into logic programming: From theory to practice. Journal of Logic Programming 19&20, 583–628 (1994)

    Article  MathSciNet  Google Scholar 

  21. Hanus, M., Lucas, S., Middeldorp, A.: Strongly sequential and inductively sequential term rewriting systems. Information Processing Letters 67(1), 1–8 (1998)

    Article  MathSciNet  Google Scholar 

  22. Huet, G., Lévy, J.-J.: Computations in Orthogonal Term Rewriting Systems, Part I + II. In: Computational logic: Essays in honour of J. Alan Robinson, pp. 395–414, 415–443. MIT Press, Cambridge (1992)

    Google Scholar 

  23. Hullot, J.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)

    Google Scholar 

  24. Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 361–373. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  25. Loogen, R., López-Fraguas, F., Rodríguez-Artalejo, M.: A Demand Driven Computation Strategy for Lazy Narrowing. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 184–200. Springer, Heidelberg (1993)

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  27. Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Handbook of Philosophical Logic, vol. 9, pp. 1–88. Kluwer, Dordrecht (2001)

    Google Scholar 

  28. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  29. Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to analysis of cryptographic protocols. In: Proc. of WRLA 2004. ENTCS, vol. 117, pp. 153–182. Elsevier, Amsterdam (2004)

    Google Scholar 

  30. Middeldorp, A.: Call by Need Computations to Root-Stable Form. In: Proc. of POPL 1997, pp. 94–105. ACM, New York (1997)

    Chapter  Google Scholar 

  31. Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Proc. of LICS 1996, pp. 473–483. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  32. Sekar, R., Ramakrishnan, I.: Programming in equational logic: Beyond strong sequentiality. Information and Computation 104(1), 78–109 (1993)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  34. Thati, P., Meseguer, J.: Complete symbolic reachability analysis using backand-forth narrowing (2005) (submitted for publication.)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Politécnica de Valencia, Spain

    Santiago Escobar

  2. University of Illinois at Urbana-Champaign, USA

    José Meseguer

  3. Carnegie Mellon University, USA

    Prasanna Thati

Authors
  1. Santiago Escobar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Prasanna Thati
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Germany

    Jürgen Giesl

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Escobar, S., Meseguer, J., Thati, P. (2005). Natural Narrowing for General Term Rewriting Systems. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32033-3_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25596-3

  • Online ISBN: 978-3-540-32033-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation