Abstract
Term rewriting systems are important for computability theory of abstract data types, for automatic theorem proving, and for the foundations of functional programming. In this short survey we present, starting from first principles, several of the basic notions and facts in the area of term rewriting. Our treatment, which often will be informal, covers abstract rewriting, Combinatory Logic, orthogonal systems, strategies, critical pair completion, and some extended rewriting formats.
Note: Research partially supported by ESPRIT projects 3020: Integration and 3074: Semagraph.
Preview
Unable to display preview. Download preview PDF.
References
BACHMAIR, L. (1988). Proof by consistency in equational theories. In: Proc. 3rd Symp. on Logic in Computer Science, Edinburgh. 228–233.
BACHMAIR, L., DERSHOWITZ, N. & HSIANG, J. (1986). Orderings for equational proofs. In: Proc. of the IEEE Symp. on Logic in Computer Science, Cambridge, Massachusetts, 346–357.
BAETEN, J.C.M., BERGSTRA, J.A., KLOP, J.W. & W.P. Weijland. (1988). Term rewriting systems with rule priorities. TCS 67 (1989) 283–301.
BARENDREGT, H.P. (1984). The Lambda Calculus, its Syntax and Semantics. 2nd ed. North-Holland 1984.
BARENDREGT, H.P. (1989). Functional programming and lambda calculus. In: Handbook of Theoretical Computer Science (ed. J. van Leeuwen), North-Holland, Amsterdam.
BARENDREGT, H.P., VAN EEKELEN, M.C.J.D., GLAUERT, J.R.W., KENNAWAY, J.R., PLASMEIJER, M.J. & SLEEP, M.R. (1987). Term graph rewriting. In: Proc. PARLE Conf., Springer LNCS 259, 141–158.
BERGSTRA, J.A. & KLOP, J.W. (1986). Conditional rewrite rules: confluence and termination. JCSS 32 (3), 323–362.
BIRKHOFF, G. (1935). On the structure of abstract algebras. In: Proc. of the Cambridge Philosophical Society 31, 433–454.
DE BRUIJN, N.G. (1978). A note on weak diamond properties. Memorandum 78-08, Eindhoven Univ. of Technology, 1978.
CURIEN, P.-L. (1986). Categorical combinators, sequential algorithms and functional programming. Research Notes in Theoretical Computer Science, Pitman, London 1986.
DAUCHET, M., TISON, S., HEUILLARD, T. & LESCANNE, P. (1987). Decidability of the confluence of ground term rewriting systems. In: Proc. of the 2nd Symp. on Logic in Computer Science, Ithaca, NY, 1987, 353–359.
DERSHOWITZ, N. (1987). Terminationof rewriting. J. of Symbolic Computation 3 (1&2), 69–115, 1987. Corrigendum: Vol.4, No.3, 409–410.
DERSHOWITZ, N. & JOUANNAUD, J.-P. (1989). Rewrite systems. To appear as Chapter 15 of Vol.B of “Handbook of Theoretical Computer Science”, North-Holland, 1989. (Rapport de Récherche no.478, Unité Associée au CNRS UA 410: AL KHOWARIZMI, Avril 1989.)
DERSHOWITZ, N., OKADA, M. & SIVAKUMAR, G. (1987). Confluence of Conditional Rewrite Systems. In: Proc. of the 1st International Workshop on Conditional Term Rewrite Systems, Orsay, Springer LNCS 308, 31–44.
DERSHOWITZ, N., OKADA, M. & SIVAKUMAR, G. (1988). Canonical Conditional Rewrite Systems. In: Proc. of 9th Conf. on Automated Deduction, Argonne, Springer LNCS 310, 538–549.
DERSHOWITZ, N. & PLAISTED, D.A. (1987). Equational Programming. In: Machine Intelligence 11 (eds. J.E. Hayes, D. Michie and J. Richards), Oxford University Press, 21–56.
GANZINGER, H. (1987). A completion procedure for conditional equations. In: Proc of the 1st Intern. Workshop on Conditional Term Rewriting Systems, Orsay 1987, Springer LNCS 308, 1988, 62–83.
GOGUEN, J.A. & MESEGUER, J. (1985). Initiality, induction, and computability. In: Algebraic methods in semantics (eds. M. Nivat and J.C. Reynolds), Cambridge University Press 1985, 459–542.
HARDIN, T. (1989). Confluence results for the pure Strong Categorical Logic CCL. λ-calculi as subsystems of CCL. Theor. Comput Sci. Fundamental Studies, Vol.65, Nr.3, 1989, 291–342.
HINDLEY, J.R. & SELDIN, J.P. (1986). Introduction to Combinators and λ-Calculus. London Mathematical Society Student Texts, Nr.1, Cambridge University Press 1986.
HÖLLDOBLER, S. (1989). Foundations of Equational Logic Programming. Springer Lecture Notes in A.I. 353.
HSIANG, J. (1985). Refutational Theorem Proving using Term-Rewriting Systems. Artificial Intelligence, 25, Vol.3, 1985.
HUET, G. (1980). Confluent reductions: Abstract properties and applications to term rewriting systems. JACM, Vol.27, No.4 (1980), 797–821.
HUET, G. & LANKFORD, D.S. (1978). On the uniform halting problem for term rewriting systems. Rep. 283, IRIA.
HUET, G. & LÉVY, J.-J. (1979). Call-by-need computations in non-ambiguous linear term rewriting systems. Rapport INRIA nr.359.
HUET, G. & OPPEN, D.C. (1980). Equations and rewrite rules: A survey. In: Formal Language Theory: Perspectives and Open Problems (ed. R. Book), Academic Press, 1980, 349–405.
KAPLAN, S. (1984). Conditional Rewrite Rules. TCS 33(2,3), 1984.
KAPLAN, S. (1985). Fair conditional term rewriting systems: Unification, termination and confluence, Recent Trends in Data Type Specification (ed. H.-J. Kreowski), Informatik-Fachberichte 116, Springer-Verlag, Berlin, 1985.
KENNAWAY, J.R. (1989). Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43 (1989) 31–56.
KLOP, J.W. (1980). Combinatory Reduction Systems. Mathematical Centre Tracts Nr.127, CWI, Amsterdam.
KLOP, J.W. (1990). Term Rewriting Systems, in: Handbook of Logic in Computer Science (eds. S. Abramsky, D. Gabbay and T. Maibaum) Vol.1, Chapter 6, Oxford University Press, to appear.
KLOP, J.W. & DE VRIJER, R.C. (1989). Unique Normal Forms for Lambda Calculus with Surjective Pairing. Information and Computation 80 (2), 97–113.
KNUTH, D.E. & BENDIX, P.B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra (ed. J. Leech), Pergamon Press, 1970, 263–297.
KRUSKAL, J.B. (1960). Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture. Trans. AMS 95, 210–225.
KURIHARA, M. & KAJI, I. (1988). Modular Term Rewriting Systems: Termination, Confluence and Strategies. Report, Hokkaido University.
KURIHARA, M. & OHUCHI, A. (1989) Modularity of Simple Termination of Term Rewriting Systems. Report 89-SF-31, Hokkaido University, Sapporo, 1989.
MIDDELDORP, A. (1989a). Modular aspects of properties of term rewriting systems related to normal forms. In: Proc. of 3rd Intern. Conf. on Rewriting Techniques and Applications, Chapel Hill, Springer LNCS 355, 263–277.
MIDDELDORP, A. (1989b). A sufficient condition for the termination of the direct sum of term rewriting systems. In: Proc. of 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, 396–401.
MIDDELDORP, A. (1989c). Confluence of the Disjoint Union of Conditional Term Rewriting Systems. Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam 1989.
NEWMAN, M.H.A. (1942). On theories with a combinatorial definition of “equivalence”. Annals of Math. 43 (2), 223–243.
O'DONNELL, M.J. (1977). Computing in systems described by equations. Springer LNCS 58.
O'DONNELL, M.J. (1985). Equational logic as a programming language. The MIT Press, Cambridge MA, 1985.
OYAMAGUCHI, M. (1987). The Church-Rosser property for ground term rewriting systems is decidable. Theoretical Computer Science 49 (1).
PEYTON JONES, S.L. (1987). The Implementation of Functional Programming Languages. Prentice-Hall 1987.
ROSEN, B.K. (1973). Tree-manipulating systems and Church-Rosser theorems. JACM, Vol.20 (1973), 160–187.
RUSINOWITCH, M. (1987). On termination of the direct sum of term rewriting systems IPL 26, 65–70.
SCHÖNFINKEL, M. (1924). Über die Bausteine der mathematischen Logik. Math. Annalen 92, 305–316. Translated as: On the building blocks of mathematical logic, in From Frege to Gödel, ed. J. van Heyenoort, Harvard Un. Press, 1967, 355–366.
SCOTT, D.S. (1975). Some philosophical issues concerning theories of combinators. In: Proc. of Symposium ‘λ-calculus and Computer Science Theory', (ed. C. Böhm), Rome 1975, Springer LNCS 37, 346–366.
STAPLES, J. (1975). Church-Rosser theorems for replacement systems. In: Algebra and Logic (ed. J. Crosley), Springer Lecture Notes in Mathematics 450, 291–307.
TOYAMA, Y. (1987a). Counterexamples to termination for the direct sum of Term Rewriting Systems. Information Processing Letters 25, 141–143.
TOYAMA, Y. (1987b). On the Church-Rosser property for the direct sum of term rewriting systems. JACM, Vol.34, No.1, 1987, 128–143.
TOYAMA, Y., KLOP, J.W. & BARENDREGT, H.P. (1989). Termination for the direct sum of left-linear term rewriting systems. In: Proc. of 3rd Intern. Conf. on Rewriting Techniques and Applications, Springer LNCS 355, 477–491.
TURNER, D.A. (1979). A new implementation technique for applicative languages. Software Practice and Experience, Vol.9, 1979, 31–49.
TURNER, D.A., (1985). Miranda: a non-strict functional language with polymorphic types. In: Proc. of the IFIP Intern. Conf. on Functional Programming Languages and Computer Architecture, Nancy. Springer LNCS 201, 1985.
WINKLER, F. & BUCHBERGER, B. (1983). A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proc. of the Coll. on Algebra, Combinatorics and Logic in Computer Science, Györ, Hungary, Sept. 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klop, J.W. (1990). Term rewriting systems from Church-Rosser to Knuth-Bendix and beyond. In: Paterson, M.S. (eds) Automata, Languages and Programming. ICALP 1990. Lecture Notes in Computer Science, vol 443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032044
Download citation
DOI: https://doi.org/10.1007/BFb0032044
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52826-5
Online ISBN: 978-3-540-47159-2
eBook Packages: Springer Book Archive