Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

On sufficient-completeness and related properties of term rewriting systems


The decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.

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


  1. 1.

    Book, R.: Confluent and Other Types of Thue Systems. J. Assoc. Comput. Mach. 29, 171–182 (1982)

  2. 2.

    Comon, H.: Sufficient Completeness, Term Rewriting Systems and “Anti-Unification”, to appear in the 8th International Conference on Automated Deduction, Oxford, England

  3. 3.

    Dershowitz, N.: Computing with Rewrite Systems. Inf. Control 65, 122–157 (1985) Earlier versions were available as Aerospace Corporation Technical Reports)

  4. 4.

    Goguen, J.: How to prove algebraic inductive hypotheses without induction. Proc. of the Fifth Conference on Automated Deduction 1980

  5. 5.

    Guttag, J.: The Specification and Application to Programming of Abstract Data Types. Department of Computer Science, Univ. of Toronto, Ph.D. Thesis, CSRG-59, 1975

  6. 6.

    Guttag, J., Horning, J.J.: The Algebraic Specification of Abstract Data Types, Acta Inf. 10, 27–52 (1978)

  7. 7.

    Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. JACM 27 (1980)

  8. 8.

    Huet, G., Hullot, J.M.: Proofs by Induction in Equational Theories with Constructors. J. Comput. Syst. Sci. 25, 239–266 (1982)

  9. 9.

    Huet, G., Oppen, D.C.: Equations and Rewrite Rules: A Survey. In: Formal Language Theory: Perspectives and Open Problems (R. Book, ed.), pp. 349–405 New York: Academic Press

  10. 10.

    Jouannaud, J.-P., Kounalis, E.: Proofs by Induction in Equational Theories Without Constructors, CRIN, University of Nancy, France, May 1985. (Also in the proceedings of the IEEE Symposium on Logic in Computer Science, pp. 358–366. Cambridge, Ma, 1986)

  11. 11.

    Kapur, D., Musser, D.R.: Proof by Consistency, Proc. of an NSF Workshop on the Rewrite Rule Laboratory, Sept. 4–6, 1983, Schenectady, G.E. R&D Center Report GEN84008, April 1984s (To appear in the Artif. Intell. J.)

  12. 12.

    Kapur, D., Narendran, P.: A Finite Thue System with Decidable Word Problem and without Equivalent Finite Canonical System. Theor. Comput. Sci. 35, 337–344 (1985)

  13. 13.

    Knuth, D., Bendix, P.: Simple Word Problems in Universal Algebras. In: Computational Problems in Abstract Algebra (J. Leech, ed.), pp. 263–297. Oxford: Pergamon Press 1970

  14. 14.

    Kounalis, E.: Completeness in Data Type Specifications. Proc. EUROCAL '85 LNCS 204 (Bob F. Caviness, ed.). pp. 348–362. Berlin, Heidelberg, New York: Springer 1985

  15. 15.

    Kounalis, E., Zhang, H.: A General Completeness Test for Equational Specifications. (Unpublished Manuscript, CRIN Nancy, France, November 1984)

  16. 16.

    Lankford, D.S.: A Simple Explanation of Inductionless Induction. Memo MTP-14, Dept. of Mathsematics, Louisiana Tech. University, Ruston, Louisiana, USA 1981

  17. 17.

    Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. Proc. 7th Principles of Programming Languages, Las Vegas USA, 1980

  18. 18.

    Narendran, P.: Church-Rosser and Related Thue Systems. Ph.D. Thesis, Department Mathematsics, RPI, Troy, NY, USA 1983, also G.E. R&D Center Report No. 84CRD176, July 1984

  19. 19.

    Narendran, P., Ó'Dúnlaing, C., Rolletschek, H.: Complexity of Certain Decision Problems about Congruential Languages. J Comput. Syst. Sci. 30, 343–358 (1985)

  20. 20.

    Nipkow, T.., Weikum G.: A Decidability Result about Sufficient-Completeness of Axiomatically Specified Abstract Data Types. Proc. of the 6th GI Conf. on Theoretical Computer Science, LNCS 145 (Cremers and Kreigel, eds.), pp. 257–268. Berlin, Heidelberg, New York: Springer (1983)

  21. 21.

    Otto, F.: Some Undecidability Results for Non-Monadic Church-Rosser Thue Systems, Theor. Comput. Sci. 33, p 261–278 (1984)

  22. 22.

    Plaisted, D.: Semantic Confluence Tests and Completion Methods. (Unpublished Manuscript, Univ. of Illinois, November 25, 1983)

  23. 23.

    Plaisted, D.: Semantic Confluence Tests and Completion Methods. Inf. Control 6b5, 182–215 (1985)

  24. 24.

    Thiel, J.J.: Stop Losing Sleep over Incomplete Data Type Specifications. Proc. Eleventh Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, Utah, 1984

Download references

Author information

Additional information

Partially supported by the National Science Foundation Grant no. DCR-8408461

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Kapur, D., Narendran, P. & Zhang, H. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24, 395–415 (1987). https://doi.org/10.1007/BF00292110

Download citation


  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory