Computer experiments with the REVE term rewriting system generator

ABSTRACT

A term rewriting system generator called REVE is described. REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis is placed on mechanization of termination proof. Indeed, REVE is one of the few such systems which can actually be called automatic because termination is fully integrated into the algorithms. REVE uses an incremental termination method based on recursive decomposition ordering which constructs the termination proof step by step from the presentation of the set of equations and which requires little knowledge of termination methods from the user. All examples from this paper are taken from abstract data type specifications.

REFERENCES

• 1: Dershowitz N., "Orderings for Term Rewriting Systems," Proc. 20th Symposium on Foundations of Computer Science, (1979), 123-131. Also, Theoretical Computer Science 17 (1982), 279-301.
• 2: Evans T., "On Multiplicative Systems Defined by Generators and Relations, I. Normal Form Theorems," Proc. Cambridge Philos. Soc. 47 (1951), 637-649.
• 3: Joseph A. Goguen, How to Prove Algebraic Inductive Hypotheses Without Induction, Proceedings of the 5th Conference on Automated Deduction, p.356-373, July 08-11, 1980
• 4: Higman G., Neumann B. H., "Groups as Groupoids with One Law," Publ. Math. Debrecen. 2 (1952), 215-221.
• 5: Huet G., "A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm," J.Comp. Sys. Sc., 23 (1981), 11-21.
• 6: Huet G., Lankford D., "On the Uniform Halting Problem for Term Rewriting Systems," Rapport Laboria 283 (mars 1978).
• 7: Huet G., Hullot J., "Proofs by Induction in Equational Theories with Constructors," Proc. 21st Symposium on Foundations of Computer Science (1980).
• 8: Huet G., Oppen D. C., "Equations and Rewrite Rules: A Survey," in Formal Languages: Perspectives and Open Problems, Ed. Book R., Academic Press (1980). Also, Technical Report CSL-11, SRI International (Jan. 1980).
• 9: Jouannaud J. P., Lescanne P., Reinig F., "Recursive Decomposition Ordering," Conf. on Formal Description of Programming Concepts, Garmisch, (1982).
• 10: Kamin S., Lévy J. J., "Attempts for Generalizing the Recursive Path Ordering," (Feb. 1980).
• 11: Knuth D. E., Bendix P. B., "Simple Word Problems in Universal Algebras," in Computational Problems in Abstract Algebra, Ed. Leech J., Pergamon Press (1969), 263-297.
• 12: Lankford D., "Research in Applied Equational Logic," Louisiana Tech. Univ., Math. Dept., report MTP-15, (Dec. 1980).
• 13: Lankford D., "A Simple Explanation of Inductionless Induction," Louisiana Tech. Univ., Math. Dept., report MTP-14, (August 1981).
• 14: Lipton R., Snyder L., "On the Halting Problem for Term Replacement Systems," Proc. Conf. on Theoretical Comp. Sci., Univ. of Waterloo, (july 1977), 43-46,
• 15: David R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-162, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567461]
• 16: Novikov P., "The Algorithm Unsolvability of the World Problem for Group Theory," Tr. Mat. Inst. Steklov. 44 (AMS Translations Series 2 9 (1955) 1-124).
• 17: Plaisted D., "A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems," Dept. of Computer Science, Report 78-943, Univ. of Illinois at Urbana-Champaign, (sept. 1978).
• 18: Post E., "Recursive Unsolvability of a Problem of Thue," J. Symb. Logic 12 (1947), 1-11.
• 19: Taussky O., "Zur Axiomatik der Gruppen", Ergebnisse eines Math. Kolloquiums Wien 4 (1963), 2-3.
• 20: Jouannaud J. P., Kirchner C., Kirchner H., "Incremental Unification in Equational Theories." Proc. 20th Allerton Conf. on Communication, Control and Computing, (oct. 1982)

INDEX TERMS

Keywords:
abstract data types, equational theories, induction, program verifier, term rewriting systems, termination, theorem prover, word problem