Skip to main content
SpringerLink
Log in

Term rewriting systems from Church-Rosser to Knuth-Bendix and beyond

  • Conference paper
  • First Online:
Book cover Automata, Languages and Programming (ICALP 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 443))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • BARENDREGT, H.P. (1984). The Lambda Calculus, its Syntax and Semantics. 2nd ed. North-Holland 1984.

    Google Scholar 

  • BARENDREGT, H.P. (1989). Functional programming and lambda calculus. In: Handbook of Theoretical Computer Science (ed. J. van Leeuwen), North-Holland, Amsterdam.

    Google Scholar 

  • 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.

    Google Scholar 

  • BERGSTRA, J.A. & KLOP, J.W. (1986). Conditional rewrite rules: confluence and termination. JCSS 32 (3), 323–362.

    Google Scholar 

  • BIRKHOFF, G. (1935). On the structure of abstract algebras. In: Proc. of the Cambridge Philosophical Society 31, 433–454.

    Google Scholar 

  • DE BRUIJN, N.G. (1978). A note on weak diamond properties. Memorandum 78-08, Eindhoven Univ. of Technology, 1978.

    Google Scholar 

  • CURIEN, P.-L. (1986). Categorical combinators, sequential algorithms and functional programming. Research Notes in Theoretical Computer Science, Pitman, London 1986.

    Google Scholar 

  • 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.

    Google Scholar 

  • DERSHOWITZ, N. (1987). Terminationof rewriting. J. of Symbolic Computation 3 (1&2), 69–115, 1987. Corrigendum: Vol.4, No.3, 409–410.

    Google Scholar 

  • 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.)

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • HINDLEY, J.R. & SELDIN, J.P. (1986). Introduction to Combinators and λ-Calculus. London Mathematical Society Student Texts, Nr.1, Cambridge University Press 1986.

    Google Scholar 

  • HÖLLDOBLER, S. (1989). Foundations of Equational Logic Programming. Springer Lecture Notes in A.I. 353.

    Google Scholar 

  • HSIANG, J. (1985). Refutational Theorem Proving using Term-Rewriting Systems. Artificial Intelligence, 25, Vol.3, 1985.

    Google Scholar 

  • HUET, G. (1980). Confluent reductions: Abstract properties and applications to term rewriting systems. JACM, Vol.27, No.4 (1980), 797–821.

    Google Scholar 

  • HUET, G. & LANKFORD, D.S. (1978). On the uniform halting problem for term rewriting systems. Rep. 283, IRIA.

    Google Scholar 

  • HUET, G. & LÉVY, J.-J. (1979). Call-by-need computations in non-ambiguous linear term rewriting systems. Rapport INRIA nr.359.

    Google Scholar 

  • 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.

    Google Scholar 

  • KAPLAN, S. (1984). Conditional Rewrite Rules. TCS 33(2,3), 1984.

    Google Scholar 

  • 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.

    Google Scholar 

  • KENNAWAY, J.R. (1989). Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43 (1989) 31–56.

    Google Scholar 

  • KLOP, J.W. (1980). Combinatory Reduction Systems. Mathematical Centre Tracts Nr.127, CWI, Amsterdam.

    Google Scholar 

  • 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.

    Google Scholar 

  • KLOP, J.W. & DE VRIJER, R.C. (1989). Unique Normal Forms for Lambda Calculus with Surjective Pairing. Information and Computation 80 (2), 97–113.

    Google Scholar 

  • 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.

    Google Scholar 

  • KRUSKAL, J.B. (1960). Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture. Trans. AMS 95, 210–225.

    Google Scholar 

  • KURIHARA, M. & KAJI, I. (1988). Modular Term Rewriting Systems: Termination, Confluence and Strategies. Report, Hokkaido University.

    Google Scholar 

  • KURIHARA, M. & OHUCHI, A. (1989) Modularity of Simple Termination of Term Rewriting Systems. Report 89-SF-31, Hokkaido University, Sapporo, 1989.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • MIDDELDORP, A. (1989c). Confluence of the Disjoint Union of Conditional Term Rewriting Systems. Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam 1989.

    Google Scholar 

  • NEWMAN, M.H.A. (1942). On theories with a combinatorial definition of “equivalence”. Annals of Math. 43 (2), 223–243.

    Google Scholar 

  • O'DONNELL, M.J. (1977). Computing in systems described by equations. Springer LNCS 58.

    Google Scholar 

  • O'DONNELL, M.J. (1985). Equational logic as a programming language. The MIT Press, Cambridge MA, 1985.

    Google Scholar 

  • OYAMAGUCHI, M. (1987). The Church-Rosser property for ground term rewriting systems is decidable. Theoretical Computer Science 49 (1).

    Google Scholar 

  • PEYTON JONES, S.L. (1987). The Implementation of Functional Programming Languages. Prentice-Hall 1987.

    Google Scholar 

  • ROSEN, B.K. (1973). Tree-manipulating systems and Church-Rosser theorems. JACM, Vol.20 (1973), 160–187.

    Google Scholar 

  • RUSINOWITCH, M. (1987). On termination of the direct sum of term rewriting systems IPL 26, 65–70.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

  • STAPLES, J. (1975). Church-Rosser theorems for replacement systems. In: Algebra and Logic (ed. J. Crosley), Springer Lecture Notes in Mathematics 450, 291–307.

    Google Scholar 

  • TOYAMA, Y. (1987a). Counterexamples to termination for the direct sum of Term Rewriting Systems. Information Processing Letters 25, 141–143.

    Google Scholar 

  • TOYAMA, Y. (1987b). On the Church-Rosser property for the direct sum of term rewriting systems. JACM, Vol.34, No.1, 1987, 128–143.

    Google Scholar 

  • 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.

    Google Scholar 

  • TURNER, D.A. (1979). A new implementation technique for applicative languages. Software Practice and Experience, Vol.9, 1979, 31–49.

    Google Scholar 

  • 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.

    Google Scholar 

  • 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Mathematics and Computer Science, Kruislaan 413, 1098 SJ, Amsterdam

    Jan Willem Klop

  2. Department of Mathematics and Computer Science, Free University, de Boelelaan 1081, 1081 HV, Amsterdam

    Jan Willem Klop

Authors
  1. Jan Willem Klop
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael S. Paterson

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation