Induction and recursion on datatypes
- 173 Downloads
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.
KeywordsComplete Lattice Domain Operator Identity Relator Recursive Call Galois Connection
Unable to display preview. Download preview PDF.
- 1.C.J. Aarts. Galois connections presented calculationally. Afstudeer verslag (Graduating Dissertation), Department of Computing Science, Eindhoven University of Technology, 1992.Google Scholar
- 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 ftp.win.tue.nl in directory pub/math.prog.construction, September 1992.Google Scholar
- 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.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.Richard S. Bird and Oege de Moor. The algebra of programming. Programming Research Group, Oxford University. Textbook in preparation.Google Scholar
- 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.B. A. Davey and H. A. Priestly. Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press, first edition, 1990.Google Scholar
- 8.Maarten M. Fokkinga. Law and Order in Algorithmics. PhD thesis, Universiteit Twente, The Netherlands, 1992.Google Scholar
- 9.Peter Freyd, Paul Hoogendijk, and Oege de Moor. Membership of datatypes. Unpublished draft.Google Scholar
- 10.P.J. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990.Google Scholar
- 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.Eindhoven University of Technology Mathematics of Program Construction Group. Fixed point calculus. Information Processing Letters, 53(3):131–136, February 1995.Google Scholar
- 13.L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–424, 1992.Google Scholar
- 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