Open. Closed. Open.

  • Nachum Dershowitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


As a window into the subject, we recount some of the history (and geography) of two mature, challenging, partially open, partially closed problems in the theory of rewriting (numbers 13 and 21 from the original RTA List of Open Problems). One problem deals with (criteria for left-linear) confluence and the other with termination (of one linear or string rule), the two paradigmatic properties of interest for rewrite systems of any flavor. Both problems were formulated a relatively long time ago, have seen considerable progress, but remain open. We also venture to contemplate the future evolution and impact of these investigations.


Word Problem Turing Machine Symbolic Computation Critical Pair Combinatory Logic 
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.
    Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symbolic Computation 6(1), 1–18 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Aït-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol. 2, ch. 1, pp. 1–30. Academic Press, New York (1989)Google Scholar
  3. 3.
    Barendregt, H.: The Lambda Calculus, its Syntax and Semantics, 2nd edn. North-Holland, Amsterdam (1984)zbMATHGoogle Scholar
  4. 4.
    Bertrand, A.: Sur une conjecture d’YvesMétivier. Theoretical Computer Science 123(1), 21–30 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bezem, M., Coquand, T.: Newman’s Lemma – a case study in proof automation and geometric logic (Logic in Computer Science Column). Bulletin of the EATCS 79, 86–100 (2003)zbMATHMathSciNetGoogle Scholar
  6. 6.
    Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic (to appear)Google Scholar
  7. 7.
    Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993)zbMATHGoogle Scholar
  8. 8.
    de Bruijn, N.G.: A note on weak diamond properties. Memorandum 1978-08, Department of Mathematics, Eindhoven University of Technology, Eindhoven, The Netherlands (August 1978)Google Scholar
  9. 9.
    Caron, A.-C.: Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 74–89. Springer, Heidelberg (1991)Google Scholar
  10. 10.
    Church, A.: The Calculi of Lambda Conversion. Ann. Mathematics Studies, vol. 6. Princeton University Press, Princeton (1941)Google Scholar
  11. 11.
    Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society 39, 472–482 (1936)zbMATHMathSciNetCrossRefGoogle Scholar
  12. 12.
    Dauchet, M.: Simulation of Turing machines by a left-linear rewrite rule. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 109–120. Springer, Heidelberg (1989)Google Scholar
  13. 13.
    Dauchet, M.: Simulation of Turing machines by a regular rewrite rule. Theoretical Computer Science 103(2), 409–420 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Dershowitz, N.: A note on simplification orderings. Information Processing Letters 9(5), 212–215 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981)Google Scholar
  16. 16.
    Dershowitz, N.: Goal solving as operational semantics. In: Proceedings of the International Logic Programming Symposium, Portland, OR, pp. 3–17. MIT Press, Cambridge (1995)Google Scholar
  17. 17.
    Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science 142(2), 179–207 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol. B, ch. 6, pp. 243–320. North-Holland, Amsterdam (1990)Google Scholar
  19. 19.
    Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: Open problems in rewriting. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 445–456. Springer, Heidelberg (1991)Google Scholar
  20. 20.
    Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: More problems in rewriting. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 468–487. Springer, Heidelberg (1993)Google Scholar
  21. 21.
    Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: Problems in rewriting III. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 457–471. Springer, Heidelberg (1995)Google Scholar
  22. 22.
    Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science (to appear)Google Scholar
  23. 23.
    Dershowitz, N., Treinen, R.: An on-line problem database. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 332–342. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  24. 24.
    Evans, T.: On multiplicative systems defined by generators and relations, I. Proceedings of the Cambridge Philosophical Society 47, 637–649 (1951)zbMATHCrossRefGoogle Scholar
  25. 25.
    Geser, A.: A solution to Zantema’s problem. Technical Report MIP-9314, Fakultät für Mathematik und Informatik, Universität Passau (1993)Google Scholar
  26. 26.
    Geser, A.: Termination of one-rule string rewriting systems _ → r where |r| ≤ 9. Technical report, Wilhelm-Schickard-Institut, Universität Tübingen, Germany (January 1998)Google Scholar
  27. 27.
    Geser, A.: Note on normalizing, non-terminating one-rule string rewriting systems. Theoretical Computer Science 243, 489–498 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    Geser, A.: Decidability of termination of grid string rewriting rules. SIAM J. Comput. 31(4), 1156–1168 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Geser, A.: Is Termination Decidable for String Rewriting with Only One Rule? Habilitation thesis, Universität Tübingen, Germany (January 2002)Google Scholar
  30. 30.
    Geser, A.: Termination of string rewriting rules that have one pair of overlaps. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 410–423. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  31. 31.
    Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. J. Automat. Reason (to appear)Google Scholar
  32. 32.
    Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in the termination hierarchy of single rewrite rules. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 237–248. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  33. 33.
    Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in term rewriting, Part I: The termination hierarchy. Inform. and Computation 178(1), 101–131 (2002)zbMATHMathSciNetGoogle Scholar
  34. 34.
    Geser, A., Zantema, H.: Non-looping string rewriting. Theoret. Informatics Appl. 33(3), 279–301 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 85–96. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  36. 36.
    Gorn, S.: On the conclusive validation of symbol manipulation processes (how do you know it has to work?). J. of the Franklin Institute 296(6), 499–518 (1973)CrossRefGoogle Scholar
  37. 37.
    Gorn, S.: Handling the growth by definition of mechanical languages. In: Proceedings of the Spring Joint Computer Conference, Philadelphia, PA, Spring, pp. 213–224 (1967)Google Scholar
  38. 38.
    Gramlich, B.: Relating innermost, weak, uniform and modular termination of term rewriting systems. SEKI-Report SR-93-09, Fachbereich Informatik, Universität Kaiserslautern, Kaiserslautern, West Germany (1993)Google Scholar
  39. 39.
    Gramlich, B.: Confluence without termination via parallel critical pairs. In: Colloquium on Trees in Algebra and Programming, pp. 211–225 (1996)Google Scholar
  40. 40.
    Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society (3), 2(7), 326–336 (1952)zbMATHCrossRefMathSciNetGoogle Scholar
  41. 41.
    Roger Hindley, J.: The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne (1964)Google Scholar
  42. 42.
    Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. Theoretical Computer Science (to appear)Google Scholar
  43. 43.
    Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 54–71. Springer, Heidelberg (1987)Google Scholar
  44. 44.
    Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery 27(4), 797–821 (1980)zbMATHMathSciNetGoogle Scholar
  45. 45.
    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 (March 1978)Google Scholar
  46. 46.
    Huet, G., Lévy, J.-J.: Call by need computations in non-ambiguous linear term rewriting systems. Rapport Laboria 359, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France (August 1979)Google Scholar
  47. 47.
    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, pp. 395–443. The MIT Press, Cambridge (1991); This is a revision of [46]Google Scholar
  48. 48.
    Jouannaud, J.-P., Kirchner, H.: Construction d’un plus petit ordre de simplification. RAIRO Theoretical Informatics 18(3), 191–207 (1984)zbMATHMathSciNetGoogle Scholar
  49. 49.
    Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered for the Knuth-Bendix procedure. J. Symbolic Computation 4, 19–36 (1988)CrossRefMathSciNetGoogle Scholar
  50. 50.
    Katsura, M., Kobayashi, Y., Otto, F.: Undecidable properties of monoids with word problem solvable in linear time. Part II– Cross sections and homological and homotopical finiteness conditions. Theoretical Computer Science 301(1–3), 79–101 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  51. 51.
    Klop, J.W.: Combinatory Reduction Systems, Mathematisch Centrum, Amsterdam. Mathematical Centre Tracts, vol. 127 (1980)Google Scholar
  52. 52.
    Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970); Reprinted in Automation of Reasoning 2, pp. 342–376. Springer, Berlin (1983)Google Scholar
  53. 53.
    Kobayashi, Y., Katsura, M., Shikishima-Tsuji, K.: Termination and derivational complexity of confluent one-rule string rewriting systems. Theoretical Computer Science 262(1/2), 583–632 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  54. 54.
    Küchlin, W.: A confluence criterion based on the generalized Newman Lemma. In: Caviness, B.F. (ed.) ISSAC 1985 and EUROCAL 1985. LNCS, vol. 204, pp. 390–399. Springer, Heidelberg (1985)Google Scholar
  55. 55.
    Kurth, W.: Termination und Konfluenz von Semi-Thue-Systems mit nur einer Regel. PhD thesis, Technische Universitat Clausthal, Clausthal, Germany (1990) (in German)Google Scholar
  56. 56.
    Kurth, W.: One-rule semi-Thue systems with loops of length one, two, or three. Inform. Theéor. Appl. 30, 355–268 (1996)Google Scholar
  57. 57.
    Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (December 1975)Google Scholar
  58. 58.
    Lankford, D.S., Musser, D.R.: A finite termination criterion (May 1978)Google Scholar
  59. 59.
    Lescanne, P.: On termination of one rule rewrite systems. Theoretical Computer Science 132(1-2), 395–401 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  60. 60.
    Lipton, R., Snyder, L.: On the halting of tree replacement systems. In: Proceedings of the Conference on Theoretical Computer Science, Waterloo, Canada, August 1977, pp. 43–46 (1977)Google Scholar
  61. 61.
    McNaughton, R.: The uniform halting problem for one-rule semi-Thue systems. Technical Report 94-18, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (August 1994); Correction (August 1996)Google Scholar
  62. 62.
    McNaughton, R.: Well-behaved derivations in one-rule semi-Thue systems. Technical Report 95-15, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (November 1995); Correction (July 1996)Google Scholar
  63. 63.
    McNaughton, R.: Contributions of Ronald V. Book to the theory of stringrewriting systems. Theor. Comput. Sci. 207(1), 13–23 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  64. 64.
    McNaughton, R.: Semi-Thue systems with an inhibitor. Journal of Automated Reasoning 26(4), 409–431 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  65. 65.
    Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, Honolulu, HI, January 1970, pp. 789–792 (1970)Google Scholar
  66. 66.
    Markov, A.A.: Theory of Algorithms. Moscow (1954)Google Scholar
  67. 67.
    Matiyasevich, J.V.: Simple examples of undecidable associative calculi. Soviet Mathematics (Dokladi) 8(2), 555–557 (1967)zbMATHGoogle Scholar
  68. 68.
    Matiyasevich, Y., Sénizergues, G.: Decision problems for semi-Thue systems with a few rules. In: Clarke, E. (ed.) Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, July 1996, pp. 523–531. IEEE Computer Society Press, Los Alamitos (1996)CrossRefGoogle Scholar
  69. 69.
    Matsumoto, T.: On confluence conditions of left-linear term rewriting systems. Master’s thesis, School of Information Science, Japan Advanced Institute of Science and Technology (February 2000) (in Japanese), English abstract is available at,
  70. 70.
    Métivier, Y.: Calcul de longueurs de chaînes de réécriture dans le monoïde libre. Theoretical Computer Science 35(1), 71–87 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  71. 71.
    Middeldorp, A., Gramlich, B.: Simple termination is difficult. Applied Algebra on Engineering, Communication and Computer Science 6(2), 115–128 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  72. 72.
    Moczydłowski Jr., W., Geser, A.: Termination of single-threaded onerule semi-Thue systems. In: Proc. of the Sixteenth International Conf. on Rewriting Techniques and Applications, Nara, Japan, April 2005. LNCS, Springer, Heidelberg (2005)Google Scholar
  73. 73.
    Herman, M., Newman, A.: On theories with a combinatorial definition of ‘equivalence’. Annals of Mathematics 43(2), 223–243 (1942)CrossRefMathSciNetGoogle Scholar
  74. 74.
    Okui, S.: Simultaneous critical pairs and Church-Rosser property. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 2–16. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  75. 75.
    van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science 126(2), 259–280 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  76. 76.
    van Oostrom, V.: Development closed critical pairs. In: Dowek, G., Heering, J., Meinke, K., Möller, B. (eds.) HOA 1995. LNCS, vol. 1074, pp. 185–200. Springer, Heidelberg (1996)Google Scholar
  77. 77.
    Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 187–201. Springer, Heidelberg (1997)Google Scholar
  78. 78.
    Oyamaguchi, M., Ohta, Y.: On the open problems concerning Church-Rosser of left-linear term rewriting systems. Trans. of IEICE E87- D(2), 290–298 (2004)Google Scholar
  79. 79.
    Plaisted, D.A., Sattler-Klein, A.: Proof lengths for equational completion. Information and Computation 125(2), 154–170 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  80. 80.
    Alan Robinson, J.: A machine-oriented logic based on the resolution principle. J. of the Association for Computing Machinery 12(1), 23–41 (1965)Google Scholar
  81. 81.
    Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. J. of the Association for Computing Machinery 20(1), 160–187 (1973)zbMATHGoogle Scholar
  82. 82.
    Sénizergues, G.: On the termination problem for one-rule semi-Thue systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 302–316. Springer, Heidelberg (1996)Google Scholar
  83. 83.
    Shikishima-Tsuji, K., Katsura, M., Kobayashi, Y.: On termination of confluent one-rule string-rewriting systems. Inf. Process. Lett. 61(2), 91–96 (1997)CrossRefMathSciNetGoogle Scholar
  84. 84.
    Socher-Ambrosius, R.: On the Church-Rosser property in left-linear systems. Technical Report TR 91/17, SUNY at Stony Brook (1991)Google Scholar
  85. 85.
    Steinby, M., Thomas, W.: Trees and term rewriting in 1910: On a paper by Axel Thue. Bulletin of the European Association for Theoretical Computer Science 72, 256–269 (2000)MathSciNetGoogle Scholar
  86. 86.
    Bittar, E.T.: Complexité linéaire du problème de Zantema. Comptes Rendus de l’Académie des Sciences, Paris 323, 1201–1206 (1996)zbMATHGoogle Scholar
  87. 87.
    Takahashi, M.: Parallel reductions in λ-calculus. Information and Computation 118(1), 120–127 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  88. 88.
    Bezem, M., Klop, J.W., de Vrijer, R. (eds.): “Terese” Term Rewriting Systems. Cambridge University Press, Cambridge (2002)Google Scholar
  89. 89.
    Thue, A.: Die Lösung eines Spezialfalles eines generellen logischen Problems. Kra. Videnskabs-Selskabets Skrifter I. Mat. Nat. Kl. (8) (1910)Google Scholar
  90. 90.
    Thue, A.: Probleme über Veranderungen von Zeichenreihen nach gegeben Regeln. Skr. Vid. Kristianaia I. Mat. Naturv. Klasse, 10/34 (1914) Google Scholar
  91. 91.
    Toyama, Y.: On the Church-Rosser property of term rewriting systems. ECL Technical Report 17672, NTT (December 1981)(In Japanese); English précis, “On parallel critical pairs” (November 1995)Google Scholar
  92. 92.
    Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393–407. North-Holland, Amsterdam (1988)Google Scholar
  93. 93.
    Winkler, F., Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proceedings of the Colloquium on Algebra, Combinatorics and Logic in Computer Science, Györ, Hungary (September 1983)Google Scholar
  94. 94.
    Wrathall, C.: Confluence of one-rule Thue systems. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 237–246. Springer, Heidelberg (1992)Google Scholar
  95. 95.
    Yasuhara, A.: Recursive Function Theory and Logic. Academic Press, London (1971)zbMATHGoogle Scholar
  96. 96.
    Zantema, H.: Total termination of term rewriting is undecidable. Journal of Symbolic Computation 20(1), 43–60 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  97. 97.
    Zantema, H., Geser, A.: A complete characterization of termination of 0p1q → 1r0s. Applicable Algebra in Engineering, Communication, and Computing 11(1), 1–25 (2000)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Nachum Dershowitz
    • 1
  1. 1.School of Computer ScienceTel Aviv UniversityRamat AvivIsrael

Personalised recommendations