Automatic program transformation viewed as theorem proving

  • Ernesto J. F. Costa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 137)


We identify the problem of automatic recursion removal using the unfold/fold methodology (2) to the problem of finding a ɛ-pattern-matcher σ for two terms t and s, that σt=ɛs. We propose a new method to solve this equation based on a technique of dynamic completion of a term rewriting system for the property \(t = _\varepsilon s \Rightarrow t\mathop \to \limits^* _R s\). This method presentssome advantages because it enables us to work with incomplete theories and limits the number of superpositions we must do during the process of completion.


Theorem Prove Equational Theory Program Transformation Automate Deduction 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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (1).
    J. Arsac and Y. Kodratoff: "Some methods for transforming recursive procedures into iterative ones", to appear ACM ToPLaS.Google Scholar
  2. (2).
    R. Burstall and J. Darlington: 1977, "A transformation system for developping recursive programs", J.ACM,vol.24,no.1.Google Scholar
  3. (3).
    E. Costa: 1981, "Dérecursivation automatique en utilisant des systèmes de réécriture de termes", thèse de 3ème cycle,Univ. de Paris VI.Google Scholar
  4. (4).
    J. Darlington: 1981, "The synthesis of implementations for abstract data types", Nato Summer School on Automatic Program Construction, Bonas,France.Google Scholar
  5. (5).
    M. Fay: 1979, "First-order unification in an equational theory", Proc. of the 4th Workshop on Automated Deduction,Austin,Texas.Google Scholar
  6. (6).
    P. Gloess and J.-P. Laurent: 1980,"Adding dynamic paramodulation to rewrite algorithms",Proc. of the 5th Conference on Automated Deduction,Les Arcs,France.Google Scholar
  7. (7).
    G. Huet and D. Oppen: 1980,"Equations and rewrite rules.a survey",SRI International Technical Report CSL-111.Google Scholar
  8. (8).
    J. Hullot. 1980,"Compilation des formes canoniques dans des théories équationnelles", thèse de 3ème cycle,Univ. de Paris-Sud.Google Scholar
  9. (9).
    D. Knuth and P. Bendix: 1970,"Simple word problems in universal algebras", in "Computational problems in abstract algebra",ed. J. Leech,Pergamon Press.Google Scholar
  10. (10).
    Z. Manna,S. Ness and J. Vuillemin: 1973,"Inductive methods for proving properties of programs",C. ACM,vol.16,no.8.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1982

Authors and Affiliations

  • Ernesto J. F. Costa
    • 1
  1. 1.Dept. Engenharia ElectrotécnicaUniversidade de CoimbraCoimbraPortugal

Personalised recommendations