Induction and recursion on datatypes

  • Henk Doornbos
  • Roland Backhouse
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)


A new induction principle is introduced. The principle is based on a property of relations, called reductivity, that generalises the property of admitting induction to one relative to a given datatype. The principle is used to characterise a broad class of recursive equations that have a unique solution and is also related to standard techniques for proving termination of programs. Methods based on the structure of the given datatype for constructing reductive relations are discussed.

The principle is formulated in the point-free calculus of relations guaranteeing concision without loss of precision and thus ensuring its amenability to calculation.


Complete Lattice Domain Operator Identity Relator Recursive Call Galois Connection 
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.
    C.J. Aarts. Galois connections presented calculationally. Afstudeer verslag (Graduating Dissertation), Department of Computing Science, Eindhoven University of Technology, 1992.Google Scholar
  2. 2.
    C.J. Aarts, R.C. Backhouse, P. Hoogendijk, T.S. Voermans, and J. van der Woude. A relational theory of datatypes. Available via anonymous ftp from in directory pub/, September 1992.Google Scholar
  3. 3.
    R.C. Backhouse, P. de Bruin, P. Hoogendijk, G. Malcolm, T.S. Voermans, and J. van der Woude. Polynomial relators. In M. Nivat, C.S. Rattray, T. Rus, and G. Scollo, editors, Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST'91, pages 303–326. Springer-Verlag, Workshops in Computing, 1992.Google Scholar
  4. 4.
    R.C. Backhouse and J. van der Woude. Demonic operators and monotype factors. Mathematical Structures in Computer Science, 3(4):417–433, December 1993.Google Scholar
  5. 5.
    Richard S. Bird and Oege de Moor. The algebra of programming. Programming Research Group, Oxford University. Textbook in preparation.Google Scholar
  6. 6.
    Garrett Birkhoff. Lattice Theory, volume 25 of American Mathematical Society Colloquium Publications. American Mathematical Society, Providence, Rhode Island, 3rd edition, 1967.Google Scholar
  7. 7.
    B. A. Davey and H. A. Priestly. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, first edition, 1990.Google Scholar
  8. 8.
    Maarten M. Fokkinga. Law and Order in Algorithmics. PhD thesis, Universiteit Twente, The Netherlands, 1992.Google Scholar
  9. 9.
    Peter Freyd, Paul Hoogendijk, and Oege de Moor. Membership of datatypes. Unpublished draft.Google Scholar
  10. 10.
    P.J. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990.Google Scholar
  11. 11.
    G. Malcolm. Homomorphisms and promotability. In J.L.A. van de Snepscheut, editor, Conference on the Mathematics of Program Construction, pages 335–347. Springer-Verlag LNCS 375, 1989.Google Scholar
  12. 12.
    Eindhoven University of Technology Mathematics of Program Construction Group. Fixed point calculus. Information Processing Letters, 53(3):131–136, February 1995.Google Scholar
  13. 13.
    L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–424, 1992.Google Scholar
  14. 14.
    E. Meijer, M.M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA91: Functional Programming Languages and Computer Architecture, volume 523 of LNCS, pages 124–144. Springer-Verlag, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Henk Doornbos
    • 1
  • Roland Backhouse
    • 1
  1. 1.Department of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations