Advertisement

A General Inductive Completion Algorithm and Application to Abstract Data Types

  • Helene Kirchner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

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.

Keywords

Function Symbol Equational Theory Ground Term Equational Term Abstract Data Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. [EKP,78]
    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)Google Scholar
  2. [GOG, 80]
    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)Google Scholar
  3. [GTW, 78]
    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)Google Scholar
  4. [H&H, 80]
    HUET G., HULLOT J.M.: “Proofs by induction in equational theories with constructors” Proc. 21th FOCS (1980) and JCSS 25-2 (1982)Google Scholar
  5. [H&O, 80]
    HUETT G., OPPEN D.: “Equations and rewrite rules: a survey” in “Formal languages: perspectives and open problems” Ed. Book R., Academic Press (1980)Google Scholar
  6. [J&K, 84]
    JOUANNAUD J.P., KIRCHNER H.: “Completion of a set of rulas modulo a set of equations” Proc of POPL (1984).Google Scholar
  7. [JOU, 83]
    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)Google Scholar
  8. [KIR, 83]
    KIRCHNER H.: “A general completion algorithm for equational term rewriting systems and its proof of correctness” Rep. CRIN, Nancy (1983)Google Scholar
  9. [K&K, 82]
    KIRCHNER C., KIRCHNER H.: “Unification dans les theories equationnelles” Proc. Jouznees GROSSEM-82, Marseille and RCP Algorithmique, Limoges (1982)Google Scholar
  10. [LAN, 81]
    LANKFORD D.S.: “A simple explanation of inductionless induction” Louisiana Tech. University, Math. Dep., Rep. MTP-14 (1981)Google Scholar
  11. [LES, 83]
    LESCANNE P.: “Computer experiments with the REVE term rewriting system generator” Proc. 10th POPL Conference (1983)Google Scholar
  12. [MUS, 80]
    MUSSER D.R.: “On proving inductive properties of abstract data types” Proc. 7th POPL Conference, Las Vegas (1980)Google Scholar
  13. [PAU, 84]
    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)Google Scholar
  14. [P&S, 81]
    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)CrossRefzbMATHGoogle Scholar
  15. [REM, 82]
    REMY J.L.: “Etude des systemes de reecriture conditionnels et application aux types abstraits algebriques” These d’Etat, Nancy (1982)Google Scholar
  16. [THI, 83]
    THIEL J.J.: “Un algorithme interactif pour l’obtention de definitions completes” Proc of POPL (1984).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Helene Kirchner
    • 1
  1. 1.Centre de Recherche en Informatique de NancyVandoeuvre-les-Nancy CedexFrance

Personalised recommendations