Generalized Innermost Rewriting

  • Jaco van de Pol
  • Hans Zantema
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


We propose two generalizations of innermost rewriting for which we prove that termination of innermost rewriting is equivalent to termination of generalized innermost rewriting. As a consequence, by rewriting in an arbitrary TRS certain non-innermost steps may be allowed by which the termination behavior and efficiency is often much better, but never worse than by only doing innermost rewriting.


Normal Form Partial Order Induction Hypothesis Conjunctive Normal Form Termination Behavior 
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.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambr. Univ. Pr., Cambridge (1998)Google Scholar
  2. 2.
    Baeten, J.C.M., Bergstra, J.A., Klop, J.W., Weijland, W.P.: Term rewriting systems with rule priorities. Theoretical Computer Science 67, 283–301 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Fokkink, W.J., Kamperman, J.F.T., Walters, H.R.: Lazy rewriting and eager machinery. ACM Transactions on Programming Languages and Systems 22(1), 45–86 (2000)CrossRefGoogle Scholar
  4. 4.
    Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: algebraic specification in action, Kluwer, Dordrecht (2000)Google Scholar
  5. 5.
    Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae 24, 3–23 (1995)zbMATHMathSciNetGoogle Scholar
  6. 6.
    Lucas, S.: Context-sensitive rewriting strategies. Information and Computation 178, 294–343 (2002)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Nakamura, M., Ogata, K.: The evaluation strategy for head normal form with and without on-demand flags. In: Futatsugi, K. (ed.) The 3rd Int. W. on Rewriting / Logic and its Applications (WRLA 2000). Electronic Notes in Theoretical Computer Science, vol. 36, Elsevier, Amsterdam (2001)Google Scholar
  8. 8.
    O’Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol. 58. Springer, Heidelberg (1977)zbMATHGoogle Scholar
  9. 9.
    Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters 25, 141–143 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    van de Pol, J.C.: Just-in-time: on strategy annotations. In Int. Workshop on Reduction Strategies in Rewriting and Programming (WRS 2001). Electronic Notes in Theoretical Computer Science, vol. 57 (2001)Google Scholar
  11. 11.
    van de Pol, J.C.: JITty: a rewriter with strategy annotations. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 367–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jaco van de Pol
    • 1
    • 2
  • Hans Zantema
    • 2
  1. 1.Department of Software EngineeringCWIAmsterdamThe Netherlands
  2. 2.Department of Computer ScienceTU EindhovenEindhovenThe Netherlands

Personalised recommendations