Advertisement

A taste of rewrite systems

  • Nachum Dershowitz
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)

Abstract

This survey of the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the KnuthBendix completion procedure and its variations, as well as rewriting-based (functional and logic) programming and (equational, first-order, and inductive) theorem proving. Ordinary, associative-commutative, and conditional rewriting are covered. Current areas of research are summarized and an extensive bibliography is provided.

Keywords

Normal Form Function Symbol Critical Pair Horn Clause Orthogonal System 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Selected bibliography

1.Rewriting

  1. 1.
    Gorn, S.: Handling the growth by definition of mechanical languages. In: Spring Joint Computer Conference, Philadelphia, PA (1967) 213–224Google Scholar
  2. 2.
    Huet, G., Oppen, D. C.: Equations and rewrite rules: A survey. In: Book, R., ed., Formal Language Theory: Perspectives and Open Problems. Academic Press, New York (1980) 349–405Google Scholar
  3. 3.
    Musser, D. R., Kapur, D.: Rewrite rule theory and abstract data type analysis. In: Calmet, J., ed., Proc. of the European Computer Algebra Conference (Marseille, France), vol. 144 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1982) 77–90Google Scholar
  4. 4.
    Jouannaud, J.-P., Lescanne, P.: Rewriting systems. Technology and Science of Informatics 6 (1987) 181–199Google Scholar
  5. 5.
    Benninghofen, B., Kemmerich, S., Richter, M. M.: Systems of Reductions, vol. 277 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1987)Google Scholar
  6. 6.
    Jantzen, M.: Confluent String Rewriting, vol. 14 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin (1988)Google Scholar
  7. 7.
    Avenhaus, J., Madlener, K.: Term rewriting and equational reasoning. In: Banerji, R. B., ed., Formal Techniques in Artificial Intelligence: A Sourcebook. Elsevier, Amsterdam (1990) 1–41Google Scholar
  8. 8.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J., ed., Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics. North-Holland, Amsterdam (1990) 243–320Google Scholar
  9. 9.
    Wechler, W.: Reductions. In: Universal Algebra for Computer Scientists, vol. 25 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin (1991) 89–133Google Scholar
  10. 10.
    Klop, J. W.: Term rewriting systems. In: Abramsky, S., Gabbay, D. M., Maibaum, T. S. E., eds., Handbook of Logic in Computer Science, vol. 1. Oxford University Press, Oxford (1992) 1–117Google Scholar

2.Termination

  1. 11.
    Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proc. of the Third Hawaii International Conference on System Science, Honolulu, HI (1970) 789–792Google Scholar
  2. 12.
    Huet, G., Lankford, D. S.: On the uniform halting problem for term rewriting systems. Rapport laboria 283, Institut de Recherche en Informatique et en Automatique, Le Chesnay, France (1978)Google Scholar
  3. 13.
    Lankford, D. S.: On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA (1979)Google Scholar
  4. 14.
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22 (1979) 465–476Google Scholar
  5. 15.
    Kamin, S., Lévy, J.-J.: Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL (1980)Google Scholar
  6. 16.
    Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Comput. Sci. 17 (1982) 279–301Google Scholar
  7. 17.
    Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3 (1987) 69–115. Corrigendum: 4, 3 (1987), 409–410Google Scholar
  8. 18.
    Comon, H.: Solving inequations in term algebras (Preliminary version). In: Proc. of the Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA (1990) 62–69Google Scholar
  9. 19.
    Jouannaud, J.-P., Okada, M.: Satisfiability of systems of ordinal notations with the subterm property is decidable. In: Albert, J. L., Monien, B., Artalejo, M. R., eds., Proc. of the Eighteenth EATCS Colloquium on Automata, Languages and Programming (Madrid, Spain), vol. 510 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1991) 455–468Google Scholar
  10. 20.
    Dershowitz, N., Hoot, C.: Topics in termination. In: Kirchner, C., ed., Proc. of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, Canada), Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1993)Google Scholar

3.Confluence

  1. 21.
    Newman, M. H. A.: On theories with a combinatorial definition of ‘equivalence'. Annals of Math. 43 (1942) 223–243Google Scholar
  2. 22.
    Selman, A.: Completeness of calculii for axiomatically defined classes of algebras. Algebra Universalis 2 (1972) 20–32Google Scholar
  3. 23.
    Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. J. Assoc. Comput. Mach. 20 (1973) 160–187Google Scholar
  4. 24.
    Staples, J.: Church-Rosser theorem for replacement systems. In: Crossley, J., ed., Algebra and Logic, vol. 450 of Lect. Notes in Mathematics. Springer-Verlag, Berlin (1975) 291–307Google Scholar
  5. 25.
    Bergman, G. M.: The Diamond Lemma for ring theory. Advances in Mathematics 29 (1978) 178–218Google Scholar
  6. 26.
    Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. Assoc. Comput. Mach. 27 (1980) 797–821Google Scholar
  7. 27.
    Klop, J. W.: Combinatory Reduction Systems, vol. 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam (1980)Google Scholar
  8. 28.
    Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. J. Assoc. Comput. Mach. 34 (1987) 128–143Google Scholar

4.Completion

  1. 29.
    Knuth, D. E., Bendix, P. B.: Simple word problems in universal algebras. In: Leech, J., ed., Computational Problems in Abstract Algebra. Pergamon Press, Oxford, U. K. (1970) 263–297Google Scholar
  2. 30.
    Métivier, Y.: About the rewriting systems produced by the Knuth-Bendix completion algorithm. Inf. Process. Lett. 16 (1983) 31–34Google Scholar
  3. 31.
    Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Pitman-Wiley, London (1985)Google Scholar
  4. 32.
    Buchberger, B.: History and basic features of the critical-pair/completion procedure. J. Symb. Comput. 3 (1987) 3–38Google Scholar
  5. 33.
    Kapur, D., Musser, D. R., Narendran, P.: Only prime superpositions need be considered for the Knuth-Bendix procedure. J. Symb. Comput. 4 (1988) 19–36Google Scholar
  6. 34.
    Bachmair, L., Dershowitz, N., Plaisted, D. A.: Completion without failure. In: Aït-Kaci, H., Nivat, M., eds., Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques. Academic Press, New York (1989) 1–30Google Scholar
  7. 35.
    Dershowitz, N.: Completion and its applications. In: Aït-Kaci, H., Nivat, M., eds., Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques. Academic Press, New York (1989) 31–86Google Scholar
  8. 36.
    Lescanne, P.: Completion procedures as transition rules + control. In: Diaz, M., Orejas, F., eds., Proc. of the Conference on Theory and Practice of Software Development, vol. 351 of Lect. Notes in Computer Science. Springer-Verlag, Berlin (1989) 28–41Google Scholar
  9. 37.
    Dick, A. J. J.: An introduction to Knuth-Bendix completion. Comput. J. 34 (1991) 2–15Google Scholar
  10. 38.
    Bachmair, L.: Canonical Equational Proofs. Birkhäuser, Boston (1991)Google Scholar
  11. 39.
    Duffy, D. A.: Knuth-Bendix Completion. In: Principles of Automated Theorem Proving. Wiley, Chichester (1991) 147–175Google Scholar
  12. 40.
    Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. Assoc. Comput. Mach. (to appear)Google Scholar

5.Validity

  1. 41.
    Evans, T.: On multiplicative systems defined by generators and relations, I. Proc. of the Cambridge Philosophical Society 47 (1951) 637–649Google Scholar
  2. 42.
    Slagle, J. R.: Automated theorem-proving for theories with simplifiers, commutativity, and associativity. J. Assoc. Comput. Mach. 21 (1974) 622–642Google Scholar
  3. 43.
    Huet, G.: A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Computer and System Sciences 23 (1981) 11–21Google Scholar
  4. 44.
    Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T., ed., Proc. of the Fourteenth EATCS International Conference on Automata, Languages and Programming (Karlsruhe, West Germany), vol. 267 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1987) 54–71Google Scholar
  5. 45.
    Martin, U., Nipkow, T.: Ordered completion. In: Stickel, M., ed., Proc. of the Tenth International Conference on Automated Deduction (Kaiserslautern, West Germany), vol. 449 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1990) 366–380Google Scholar
  6. 46.
    Peterson, G. E.: Solving term inequalities. In: Proc. of the Eighth National Conference on Artificial Intelligence, Boston, MA (1990) 258–263Google Scholar

6.Satisfiability

  1. 47.
    Fay, M.: First-order unification in an equational theory. In: Proc. of the Fourth Workshop on Automated Deduction, Austin, TX (1979) 161–167Google Scholar
  2. 48.
    Hullot, J.-M.: Canonical forms and unification. In: Kowalski, R., ed., Proc. of the Fifth International Conference on Automated Deduction (Les Arcs, France), vol. 87 of Lect. Notes in Computer Science. Springer-Verlag, Berlin (1980) 318–334Google Scholar
  3. 49.
    Dershowitz, N., Sivakumar, G.: Solving goals in equational languages. In: Kaplan, S., Jouannaud, J.-P., eds., Proc. of the First International Workshop on Conditional Term Rewriting Systems (Orsay, France), vol. 308 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1987) 45–55Google Scholar
  4. 50.
    Nutt, W., Réty, P., Smolka, G.: Basic narrowing revisited. J. Symb. Comput. 7 (1989) 295–318Google Scholar
  5. 51.
    Bockmayr, A., Krischer, S., Werner, A.: An optimal narrowing strategy for general canonical systems. In: Rusinowitch, M., ed., Proc. of the Third International Workshop on Conditional Rewriting Systems (Pont-a-Mousson, France, July 1992), vol. 656 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1993)Google Scholar

7.AC-completion

  1. 52.
    Peterson, G. E., Stickel, M. E.: Complete sets of reductions for some equational theories. J. Assoc. Comput. Mach. 28 (1981) 233–264Google Scholar
  2. 53.
    Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15 (1986) 1155–1194Google Scholar
  3. 54.
    Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theoretical Comput. Sci. 67 (1989)Google Scholar
  4. 55.
    Zhang, H., Kapur, D.: Unnecessary inferences in associative-commutative completion procedures. Mathematical Systems Theory 23 (1990) 175–206Google Scholar

8.Conditional rewriting

  1. 56.
    Bergstra, J. A., Klop, J. W.: Conditional rewrite rules: Confluency and termination. J. Comput. System Sciences 32 (1986) 323–362Google Scholar
  2. 57.
    Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination and confluence. J. Symb. Comput. 4 (1987) 295–334Google Scholar
  3. 58.
    Padawitz, P.: Computing in Horn Clause Theories, vol. 16 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin (1988)Google Scholar
  4. 59.
    Dershowitz, N., Okada, M., Sivakumar, G.: Canonical conditional rewrite systems. In: Proc. of the Ninth Conference on Automated Deduction (Argonne, IL), vol. 310 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1988) 538–549Google Scholar
  5. 60.
    Kaplan, S., Rémy, J.-L.: Completion algorithms for conditional rewriting systems. In: Aït-Kaci, H., Nivat, M., eds., Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques. Academic Press, Boston (1989) 141–170Google Scholar
  6. 61.
    Klop, J. W., de Vrijer, R. C.: Extended term rewriting systems. In: Kaplan, S., Okada, M., eds., Proc. of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada, June 1990), vol. 516 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1991) 26–50Google Scholar
  7. 62.
    Padawitz, P.: Reduction and narrowing for Horn clause theories. Comput. J. 34 (1991) 42–51Google Scholar
  8. 63.
    Ganzinger, H.: A completion procedure for conditional equations. J. Symb. Comput. 11 (1991) 51–81Google Scholar

9.Programming

  1. 64.
    O'Donnell, M. J.: Computing in systems described by equations, vol. 58 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1977)Google Scholar
  2. 65.
    Guttag, J. V., Horowitz, E., Musser, D. R.: Abstract data types and software validation. Commun. ACM 21 (1978) 1048–1064Google Scholar
  3. 66.
    Futatsugi, K., Goguen, J. A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Reid, B., ed., Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, New Orleans, LA (1985) 52–66Google Scholar
  4. 67.
    Dershowitz, N.: Computing with rewrite systems. Information and Control 64 (1985) 122–157Google Scholar
  5. 68.
    O'Donnell, M. J.: Equational Logic as a Programming Language. MIT Press, Cambridge, MA (1985)Google Scholar
  6. 69.
    Reddy, U. S.: On the relationship between logic and functional languages. In: DeGroot, D., Lindstrom, G., eds., Logic Programming: Functions, Relations, and Equations. Prentice-Hall, Englewood Cliffs, NJ (1986) 3–36Google Scholar
  7. 70.
    Goguen, J. A., Meseguer, J.: Eqlog: Equality, types, and generic modules for logic programming. In: DeGroot, D., Lindstrom, G., eds., Logic Programming: Functions, Relations, and Equations. Prentice-Hall, Englewood Cliffs, NJ (1986) 295–363Google Scholar
  8. 71.
    Dershowitz, N., Plaisted, D. A.: Equational programming. In: Hayes, J. E., Michie, D., Richards, J., eds., Machine Intelligence 11: The logic and acquisition of knowledge. Oxford Press, Oxford (1988) 21–56Google Scholar
  9. 72.
    Hölldobler, S.: Foundations of Equational Logic Programming, vol. 353 of Lect. Notes in Artificial Intelligence. Springer-Verlag, Berlin (1989)Google Scholar
  10. 73.
    Dershowitz, N., Okada, M.: A rationale for conditional equational programming. Theoretical Comput. Sci. 75 (1990) 111–138Google Scholar
  11. 74.
    Huet, G., Lévy, J.-J.: Computations in orthogonal rewriting systems, I and II. In: Lassez, J.-L., Plotkin, G., eds., Computational Logic: Essays in Honor of Alan Robinson. MIT Press, Cambridge, MA (1991) 395–443Google Scholar

10.Theorem proving

  1. 75.
    Lankford, D. S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (1975)Google Scholar
  2. 76.
    Lankford, D. S., Ballantyne, A. M.: The refutation completeness of blocked permutative narrowing and resolution. In: Proc. of the Fourth Workshop on Automated Deduction, Austin, TX (1979) 53–59Google Scholar
  3. 77.
    Musser, D. R.: On proving inductive properties of abstract data types. In: Proc. of the Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV (1980) 154–162Google Scholar
  4. 78.
    Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. J. Comput. System Sciences 25 (1982) 239–266Google Scholar
  5. 79.
    Peterson, G. E.: A technique for establishing completeness results in theorem proving with equality. SIAM J. Comput. 12 (1983) 82–100Google Scholar
  6. 80.
    Plaisted, D. A.: Semantic confluence tests and completion methods. Information and Control 65 (1985) 182–215Google Scholar
  7. 81.
    Hsiang, J.: Refutational theorem proving using term-rewriting systems. Artif. Intell. 25 (1985) 255–300Google Scholar
  8. 82.
    Paul, E.: Equational methods in first order predicate calculus. J. Symb. Comput. 1 (1985) 7–29Google Scholar
  9. 83.
    Kapur, D., Musser, D. R.: Proof by consistency. Artif. Intell. 31 (1987) 125–157Google Scholar
  10. 84.
    Kapur, D., Narendran, P., Zhang, H.: On sufficient completeness and related properties of term rewriting systems. Acta Inf. 24 (1987) 395–415Google Scholar
  11. 85.
    Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. Info. and Comput. 81 (1989) 1–33Google Scholar
  12. 86.
    Küchlin, W.: Inductive completion by ground proof transformation. In: Aït-Kaci, H., Nivat, M., eds., Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques. Academic Press, New York (1989) 211–244Google Scholar
  13. 87.
    Comon, H., Lescanne, P.: Equational problems and disunification. J. Symb. Comput. 7 (1989) 371–425Google Scholar
  14. 88.
    Fribourg, L.: A strong restriction of the inductive completion procedure. J. Symb. Comput. 8 (1989) 253–276Google Scholar
  15. 89.
    Reddy, U. S.: Term rewriting induction. In: Stickel, M., ed., Proc. of the Tenth International Conference on Automated Deduction (Kaiserslautern, West Germany), vol. 449 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1990)Google Scholar
  16. 90.
    Dershowitz, N., Pinchover, E.: Inductive synthesis of equational programs. In: Proc. of the Eighth National Conference on Artificial Intelligence. AAAI, Boston, MA (1990) 234–239Google Scholar
  17. 91.
    Dershowitz, N.: Ordering-based strategies for Horn clauses. In: Proc. of the Twelfth International Joint Conference on Artificial Intelligence, Sydney, Australia (1991) 118–124Google Scholar
  18. 92.
    Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. J. Symb. Comput. 11 (1991) 83–112Google Scholar

Future research

  1. 93.
    Goguen, J. A., Kirchner, C., Meseguer, J.: Concurrent term rewriting as a model of computation. In: Keller, R., Fasel, J., eds., Proc. of Graph Reduction Workshop (Santa Fe, NM), vol. 279 of Lect. Notes in Computer Sci. Springer-Verlag (1987) 53–93Google Scholar
  2. 94.
    Toyama, Y., Klop, J. W., Barendregt, H. P.: Termination for the direct sum of left-linear term rewriting systems. In: Dershowitz, N., ed., Proc. of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill), vol. 355 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1989) 477–491Google Scholar
  3. 95.
    Dick, A. J. J., Watson, P.: Order-sorted term rewriting. Comput. J. 34 (1991) 16–19Google Scholar
  4. 96.
    Dershowitz, N., Kaplan, S., Plaisted, D. A.: Rewrite, rewrite, rewrite, rewrite, rewrite,.... Theoretical Comput. Sci. 83 (1991) 71–96Google Scholar
  5. 97.
    Dershowitz, N., Jouannaud, J.-P., Klop, J. W.: Open problems in rewriting. In: Book, R., ed., Proc. of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), vol. 488 of Lect. Notes in Computer Sci. Springer-Verlag, Berlin (1991) 445–456Google Scholar
  6. 98.
    Jouannaud, J.-P., Okada, M.: Executable higher-order algebraic specification languages. In: Proc. of the Sixth IEEE Symposium on Logic in Computer Science (1991)Google Scholar
  7. 99.
    Bachmair, L.: Associative-commutative reduction orderings. Inf. Process. Lett. 43 (1992) 21–27Google Scholar
  8. 100.
    Hsiang, J., Kirchner, H., Lescanne, P., Rusinowitch, M.: Automated theorem proving in the presence of equalities. J. Autom. Reas. 14 (1992) 71–100Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Nachum Dershowitz
    • 1
  1. 1.Department of Computer ScienceUniversity of IllinoisUrbanaUSA

Personalised recommendations