Abstract
This paper states the connection between hierarchical construction of equational specifications and completion of equational term rewriting systems. A general inductive completion algorithm is given, which turns out to be a well-suited tool to build up specifications by successive enrichments. Moreover, the same algorithm allows verifying consistency of a specification or proving theorems in its initial algebra without using explicit induction.
This research has been supported by GRECO de Progrsmmation and by Agence pour le Developpement de l’Informatique, under contract no 82/767
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
EHRIG H., KREOWSKY H.J., PADAJITZ P.: “Stepwise specification and implementation of abstract data types” Proc. 5th Int. Colloquium on Automata, Languages and Programming, Udine (1978)
GOGUEN J.A.: “How to prove algebraic inductive hypotheses without induction, with application to the correctness of data types implementation” Proc. 5th CADE, Les Arcs (1980)
GOGUEN J.A., THATCHER J.W., AGNER E.G.: “An initial algebra approach to the specification, correctness and implementation of abstrast data types” in “Current trends in programming methodology”, vol. 4, pp 80–149, Ed. Yeh R., Prentice-Hall (1978)
HUET G., HULLOT J.M.: “Proofs by induction in equational theories with constructors” Proc. 21th FOCS (1980) and JCSS 25-2 (1982)
HUETT G., OPPEN D.: “Equations and rewrite rules: a survey” in “Formal languages: perspectives and open problems” Ed. Book R., Academic Press (1980)
JOUANNAUD J.P., KIRCHNER H.: “Completion of a set of rulas modulo a set of equations” Proc of POPL (1984).
JOUANNAUD J.P.: “Confluent and coherent sets of reductions with equations. Application to proofs in data types.” Proc. 8th Colloquium on Trees in Algebra and Programming (1983)
KIRCHNER H.: “A general completion algorithm for equational term rewriting systems and its proof of correctness” Rep. CRIN, Nancy (1983)
KIRCHNER C., KIRCHNER H.: “Unification dans les theories equationnelles” Proc. Jouznees GROSSEM-82, Marseille and RCP Algorithmique, Limoges (1982)
LANKFORD D.S.: “A simple explanation of inductionless induction” Louisiana Tech. University, Math. Dep., Rep. MTP-14 (1981)
LESCANNE P.: “Computer experiments with the REVE term rewriting system generator” Proc. 10th POPL Conference (1983)
MUSSER D.R.: “On proving inductive properties of abstract data types” Proc. 7th POPL Conference, Las Vegas (1980)
PAUL E.: “Preuve par induction dans les theories equationnelles en presence de relations entre las conetructeurs” Proc of 9th Colloquium on trees in Algebra and Programming (1984)
PETERSON G.E., STICKEL M.E.: “Complete sets of reductions for equational theories with complete unification algorithms” J.ACM 28, no. 2, pp 233–264 (1981)
REMY J.L.: “Etude des systemes de reecriture conditionnels et application aux types abstraits algebriques” These d’Etat, Nancy (1982)
THIEL J.J.: “Un algorithme interactif pour l’obtention de definitions completes” Proc of POPL (1984).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kirchner, H. (1984). A General Inductive Completion Algorithm and Application to Abstract Data Types. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_17
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_17
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive