Experiments with partial evaluation domains for rewrite specifications

  • Reinhard Bündgen
  • Werner Lauterbach
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


We describe a method to improve the efficiency of normalization procedures for term rewriting systems. This improvement does not restrict the semantics of the term rewriting specification in any respect. In particular, the expressive power of term rewriting systems as a programming language for generic programs and as a theorem prover has been preserved. Our method is based on the following observation. Many rewrite specifications are instances of theories for which efficient data structures exist. In that case we can exploit the canonical representation of objects of such a data structure by translating terms to corresponding objects, and retranslating these objects to terms (in normal form). We will call an implementation of a data structure that allows for this kind of transformations for all (not necessarily ground) terms an evaluation domain. This is then extended to the case where only part of a rewrite specification can directly be transformed using an evaluation domain. We develop the semantical requirements for such evaluation domains and discuss how evaluation domains can support the normalization process. We propose language extensions necessary for term rewriting software to take advantage of evaluation domains. Many experiments with an implementation based on the ReDuX term rewriting laboratory emphasize the efficiency of our approach.


Normal Form Partial Evaluation Evaluation Candidate Ground Term Abstract Data Type 
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.
    Avenhaus, J., and Becker, K.: Operational specifications with built-ins. In Enlbert, P., Mayr, E. W., and Wagner, K. W., editors, STACS 94 (LNCS 775). Springer-Verlag, 1994.Google Scholar
  2. 2.
    Benninghofen, B., Kemmerich, S., and Richter, M. M.: Systems of Reductions. Springer-Verlag, Berlin, 1987.Google Scholar
  3. 3.
    Bryant, R. E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.Google Scholar
  4. 4.
    Bubeck, T., Kebschull, U., and Rosenstiel, W.:-Sparrow — Ein Mikroprozessor-Entwurfs-und Ausbildungssystem. Technical Report 93-07, Wilhelm-Schickard-Institut, Universität Tübingen, D-72076 Tübingen, 1993. (in German).Google Scholar
  5. 5.
    Bündgen, R.: Reduce the redex → ReDuX. In Kirchner, C., editor, Rewriting Techniques and Applications (LNCS 690). Springer-Verlag, 1993.Google Scholar
  6. 6.
    Bündgen, R.: Combining computer algebra and rule based reasoning. In Integrating Symbolic Mathematical Computation and Artificial Intelligence. Springer-Verlag, 1995.Google Scholar
  7. 7.
    Bündgen, R.: Preserving confluence for rewrite systems with built-in operations. In Dershowitz, N., and Lindenstrauss, N., editors, Conditional and Typed Rewriting Systems (LNCS 968). Springer-Verlag, 1995.Google Scholar
  8. 8.
    Bündgen, R., and Eckhardt, H.: A fast algorithm for ground normal form analysis. In Kirchner, H., and Levi, G., editors, Algebraic and Logic Programming (LNCS 632). Springer-Verlag, 1992.Google Scholar
  9. 9.
    Bündgen, R., Göbel, M., and Küchlin, W.: Strategy compliant multi-threaded term completion. Journal of Symbolic Computation, 1996. (to appear).Google Scholar
  10. 10.
    Bündgen, R., Küchlin, W., and Lauterbach, W.: Verification of the Sparrow processor. In Engineering of Computer-Based Systems. IEEE Press, 1996.Google Scholar
  11. 11.
    Bündgen, R., Sinz, C., and Walter, J. ReDuX 1.5: New facets of rewriting. In Ganzinger, H., editor, Rewriting Techniques and Applications. Springer-Verlag, 1996. (to appear).Google Scholar
  12. 12.
    Collins, G. E.: ALDES and SAC-2 now available. SIGSAM Bull., 12(2): 19, 1980.Google Scholar
  13. 13.
    Dershowitz, N., and Jouannaud, J.-R: Rewrite systems. In Leeuven, J. van, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, chapter 6. Elsevier, 1990.Google Scholar
  14. 14.
    Goguen, J. A., Winkler, T., Meseguer, J., Futatsugi, K., and Jouannaud, J.-P.: Introducing OBJ, October 1993.Google Scholar
  15. 15.
    Guttag, J. V., and Horning, J. J.: Larch: Languages and tools for Formal Specification. Springer-Verlag, 1993.Google Scholar
  16. 16.
    Hsiang, J.: Refutational theorem proving using term-rewriting systems. Artificial Intelligence, 25:255–300, 1985.Google Scholar
  17. 17.
    Jaffar, J., and Lassez, J.-L.: Constraint logic programming. In ACM Symp. on Principles of Progr. Languages '87. 1987.Google Scholar
  18. 18.
    Kamperman, J., and Walters, H. R.: Minimal term rewriting. In 11th Workshop on Abstract Data Types (this volume), 1996.Google Scholar
  19. 19.
    Kaplan, S., and Choppy, C.: Abstract rewriting with concrete operators. In Dershowitz, N., editor, Rewriting Techniques and Applications (LNCS 355). Springer-Verlag, 1989.Google Scholar
  20. 20.
    Kapur, D., and Musser, D. R.: Tecton: A framework for specifying and verifying generic system components. Technical Report 92-20, Rennselaer Polytechnic Institute, Troy, New York 12180-3590, 1992.Google Scholar
  21. 21.
    Kebschull, U., Schubert, E., and Rosenstiel, W: Multilevel logic synthesis based on functional decision diagrams. In Proc. EDAC 1992, 1992.Google Scholar
  22. 22.
    Kirchner, C., Kirchner, H., and Michaël, R.: Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3): 9–52, 1990.Google Scholar
  23. 23.
    Kirchner, C., and Viry, P.: Implementing parallel rewriting. In Fronhöfer, B., and Wrightson, G., editors, Parallelization in Inference Systems (LNCS 590). Springer-Verlag, 1990.Google Scholar
  24. 24.
    Knuth, D. E., and Bendix, P. B.: Simple word problems in universal algebra. In Leech, J., editor, Computational Problems in Abstract Algebra. Pergamon Press, 1970.Google Scholar
  25. 25.
    Küchlin, W.: Some reduction strategies for algebraic term rewriting. ACM SIGSAM Bull., 16(4): 13–23, Nov. 1982.Google Scholar
  26. 26.
    Küchlin, W.: Inductive completion by ground proof transformation. In Aït-Kaci, H., and Nivat, M., editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, chapter 7. Academic Press, 1989.Google Scholar
  27. 27.
    Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Pitman, London, 1986.Google Scholar
  28. 28.
    Marché, C.: Normalised rewriting and normalised completion. In Ninth Anual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.Google Scholar
  29. 29.
    Meinke, K., and Tucker, J. V.: Universal algebra. In Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., editors, Background: Mathematical Strcutures, volume 1 of Handbook of Logic in Computer Science, chapter 3. Oxford University Press, 1992.Google Scholar
  30. 30.
    Peterson, G., and Stickel, M.: Complete sets of reductions for some equational theories. J. ACM, 28:223–264, 1981.Google Scholar
  31. 31.
    Stone, M. H.: The theory of representations of Boolean algebras. Trans. American Math. Society, 40:37–111, 1936.Google Scholar
  32. 32.
    Walters, H. R.: Hybrid implementations of algebraic specifications. In Kirchner, H., and Wechler, W., editors, Algebraic and Logic Programming (LNCS 463). Springer-Verlag, 1990.Google Scholar
  33. 33.
    Walters, H. R. and Kamperman, J. Epic 1.0 (unconditional), an equational programming language. Technical Report CS-R9604, CWI, 1996.Google Scholar
  34. 34.
    Walters, H.R., and Zantema, H.: Rewrite systems for integer arithmetic. In Hsiang, J., editor, Rewriting Techniques and Applications (LNCS 914). Springer-Verlag, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Reinhard Bündgen
    • 1
  • Werner Lauterbach
    • 1
  1. 1.Wilhelm-Schickard-InstitutUniversität TübingenTübingen

Personalised recommendations