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.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Book, R.: Confluent and Other Types of Thue Systems. J. Assoc. Comput. Mach. 29, 171–182 (1982)
Comon, H.: Sufficient Completeness, Term Rewriting Systems and “Anti-Unification”, to appear in the 8th International Conference on Automated Deduction, Oxford, England
Dershowitz, N.: Computing with Rewrite Systems. Inf. Control 65, 122–157 (1985) Earlier versions were available as Aerospace Corporation Technical Reports)
Goguen, J.: How to prove algebraic inductive hypotheses without induction. Proc. of the Fifth Conference on Automated Deduction 1980
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
Guttag, J., Horning, J.J.: The Algebraic Specification of Abstract Data Types, Acta Inf. 10, 27–52 (1978)
Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. JACM 27 (1980)
Huet, G., Hullot, J.M.: Proofs by Induction in Equational Theories with Constructors. J. Comput. Syst. Sci. 25, 239–266 (1982)
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
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)
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.)
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)
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
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
Kounalis, E., Zhang, H.: A General Completeness Test for Equational Specifications. (Unpublished Manuscript, CRIN Nancy, France, November 1984)
Lankford, D.S.: A Simple Explanation of Inductionless Induction. Memo MTP-14, Dept. of Mathsematics, Louisiana Tech. University, Ruston, Louisiana, USA 1981
Musser, D.R.: On Proving Inductive Properties of Abstract Data Types. Proc. 7th Principles of Programming Languages, Las Vegas USA, 1980
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
Narendran, P., Ó'Dúnlaing, C., Rolletschek, H.: Complexity of Certain Decision Problems about Congruential Languages. J Comput. Syst. Sci. 30, 343–358 (1985)
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)
Otto, F.: Some Undecidability Results for Non-Monadic Church-Rosser Thue Systems, Theor. Comput. Sci. 33, p 261–278 (1984)
Plaisted, D.: Semantic Confluence Tests and Completion Methods. (Unpublished Manuscript, Univ. of Illinois, November 25, 1983)
Plaisted, D.: Semantic Confluence Tests and Completion Methods. Inf. Control 6b5, 182–215 (1985)
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
Partially supported by the National Science Foundation Grant no. DCR-8408461
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
- Information System
- Operating System
- Data Structure
- Communication Network
- Information Theory