Natural Narrowing for General Term Rewriting Systems

  • Santiago Escobar
  • José Meseguer
  • Prasanna Thati
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


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.


Theorem Prove Concurrent System Symbolic Model Check Reachability Problem Root Position 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Antoy, S.: Definitional trees. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 143–157. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  2. 2.
    Antoy, S.: Constructor-based conditional narrowing. In: Proc. of PPDP 2001, pp. 199–206. ACM, New York (2001)CrossRefGoogle Scholar
  3. 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. 4.
    Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. Journal of the ACM 47(4), 776–822 (2000)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Antoy, S., Lucas, S.: Demandness in rewriting and narrowing. In: Proc. of WFLP 2002. ENTCS, vol. 76, Elsevier, Amsterdam (2002)Google Scholar
  6. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 913–962. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  9. 9.
    Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation 159(1/2), 151–186 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996)zbMATHGoogle Scholar
  11. 11.
    Escobar, S.: Refining weakly outermost-needed rewriting and narrowing. In: Proc. of PPDP 2003, pp. 113–123. ACM, New York (2003)CrossRefGoogle Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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
  14. 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)CrossRefGoogle Scholar
  15. 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. 16.
    Futatsugi, K., Diaconescu, R.: CafeOBJ Report. AMAST Series. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  17. 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)zbMATHCrossRefGoogle Scholar
  18. 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. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Hanus, M.: The integration of functions into logic programming: From theory to practice. Journal of Logic Programming 19&20, 583–628 (1994)CrossRefMathSciNetGoogle Scholar
  21. 21.
    Hanus, M., Lucas, S., Middeldorp, A.: Strongly sequential and inductively sequential term rewriting systems. Information Processing Letters 67(1), 1–8 (1998)CrossRefMathSciNetGoogle Scholar
  22. 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. 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. 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)CrossRefGoogle Scholar
  25. 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. 26.
    Lucas, S.: Context-sensitive rewriting strategies. Information and Computation 178(1), 294–343 (2002)zbMATHMathSciNetGoogle Scholar
  27. 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. 28.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 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. 30.
    Middeldorp, A.: Call by Need Computations to Root-Stable Form. In: Proc. of POPL 1997, pp. 94–105. ACM, New York (1997)CrossRefGoogle Scholar
  31. 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. 32.
    Sekar, R., Ramakrishnan, I.: Programming in equational logic: Beyond strong sequentiality. Information and Computation 104(1), 78–109 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  33. 33.
    TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)Google Scholar
  34. 34.
    Thati, P., Meseguer, J.: Complete symbolic reachability analysis using backand-forth narrowing (2005) (submitted for publication.)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Santiago Escobar
    • 1
  • José Meseguer
    • 2
  • Prasanna Thati
    • 3
  1. 1.Universidad Politécnica de ValenciaSpain
  2. 2.University of Illinois at Urbana-ChampaignUSA
  3. 3.Carnegie Mellon UniversityUSA

Personalised recommendations