Proofs by induction in equational theories with constructors
- 1 October 1980
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 96-107
- https://doi.org/10.1109/sfcs.1980.37
Abstract
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 Musser15 and Goguen6.Keywords
This publication has 7 references indexed in Scilit:
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- On proving inductive properties of abstract data typesPublished by Association for Computing Machinery (ACM) ,1980
- Orderings for term-rewriting systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Initial Algebra Semantics and Continuous AlgebrasJournal of the ACM, 1977
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- Simple Word Problems in Universal Algebras††The work reported in this paper was supported in part by the U.S. Office of Naval Research.Published by Elsevier ,1970
- Proving Properties of Programs by Structural InductionThe Computer Journal, 1969