Generalized Innermost Rewriting
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.
KeywordsNormal Form Partial Order Induction Hypothesis Conjunctive Normal Form Termination Behavior
Unable to display preview. Download preview PDF.
- 1.Baader, F., Nipkow, T.: Term Rewriting and All That. Cambr. Univ. Pr., Cambridge (1998)Google Scholar
- 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
- 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
- 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