zbMATH — the first resource for mathematics

Proofs by induction in equational theories with constructors. (English) Zbl 0532.68041
Summary: We show how to prove (and disprove) theorems in the initial algebra of an equational variety by a simple extension of the Knuth-Bendix completion algorithm. This allows us to prove by purely equational reasoning theorems whose proof usually requires induction. We show applications of this method to proofs of programs computing over data structures, and to proofs of algebraic-summation identities. This work extends and simplifies recent results of D. L. Musser [Proc. 7th. Ann. ACM Symp. Principles of Programming Languages, Las Vegas, 154-162 (1980)] and J. A. Goguen [Automated deduction, 5th Conf., Les Arcs/France 1980, Lect. Notes Comput. Sci. 87, 356-373 (1980; Zbl 0438.68043)].

68Q65 Abstract data types; algebraic specification
08B05 Equational logic, Mal’tsev conditions
68N01 General topics in the theory of software
08-04 Software, source code, etc. for problems pertaining to general algebraic systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Aubin, R., Mechanizing structural induction, () · Zbl 0423.68051
[2] Boyer, R.; Moore, J., Proving theorems about LISP functions, J. assoc. comput. Mach., 22, 129-144, (1975) · Zbl 0338.68014
[3] Boyer, R.; Moore, J., A computational logic, (1979), Academic Press New York · Zbl 0448.68020
[4] Burstall, R.M., Proving properties of programs by structural induction, Comput. J., 12, 41-48, (1969) · Zbl 0164.46202
[5] Dershowitz, N., Orderings for term-rewriting systems, (), 123-131, to appear
[6] Goguen, J.A., How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation, (), 356-373, No. 87 · Zbl 0438.68043
[7] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Initial algebras semantics and continuous algebras, J. assoc. comput. Mach., 24, 68-95, (1977) · Zbl 0359.68018
[8] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness, and implementation of abstract data types, (), 80-149
[9] Huet, G.; Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, (), J. assoc. comput. Mach., 27, 4, 797-821, (1980) · Zbl 0458.68007
[10] Huet, G., A complete proof of correctness of the Knuth-bendix completion algorithm, Rapport de recherche INRIA, No 25, (Juillet 1980)
[11] J. Comput. System Sci., to appear.
[12] Huet, G.; Oppen, D.; Huet, G.; Oppen, D., Equations and rewrite rules: A survey, ()
[13] Kamin, S.; Lévy, J.J., Two generalizations of the recursive path ordering, (February 1980), private communication
[14] Knuth, D.; Bendix, P., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902
[15] Lankford, D.S.; Ballantyne, A.M., Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions, () · Zbl 0449.20059
[16] Musser, D.L., On proving inductive properties of abstract data types, (), 154-162
[17] Peterson, G.E.; Stikel, M.E., Complete sets of reductions for equational theories with complete unification algorithms, (September 1977), Department of Computer Science, Univ. of Arizona Tucson, Technical Report
[18] Plaisted, D., A recursively defined ordering for proving termination of term rewriting systems, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.