Abstract
Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. Coinduction is often considered a rather low-level proof method, in particular, as it departs quite radically from equational reasoning. Corecursive programs are conveniently defined using recursion equations. Suitably restricted, these equations possess unique solutions. Uniqueness gives rise to a simple and attractive proof technique, which essentially brings equational reasoning to the coworld. We illustrate the approach using two major examples: streams and infinite binary trees. Both coinductive types exhibit a rich structure: they are applicative functors or idioms, and they can be seen as memo-tables or tabulations. We show that definitions and calculations benefit immensely from this additional structure.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aczel, P., Mendler, N.: A final coalgebra theorem. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 357–365. Springer, Heidelberg (1989)
Altenkirch, T.: Representations of first order function types as terminal coalgebras. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 62–78. Springer, Heidelberg (2001)
Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall Europe, London (1997)
Bird, R.: An introduction to the theory of lists. In: Broy, M. (ed.) Proceedings of the NATO Advanced Study Institute on Logic of programming and calculi of discrete design, Marktoberdorf, Germany, pp. 5–42. Springer, Heidelberg (1987)
Connelly, R.H., Morris, F.L.: A generalization of the trie data structure. Mathematical Structures in Computer Science 5(3), 381–418 (1995)
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)
Curry, H., Feys, R.: Combinatory Logic, vol. 1. North-Holland, Amsterdam (1958)
Danvy, O.: An extensional characterization of lambda-lifting and lambda-dropping. In: Middeldorp, A. (ed.) FLOPS 1999. LNCS, vol. 1722, pp. 241–250. Springer, Heidelberg (1999)
Dijkstra, E.W.: EWD570: An exercise for Dr.R.M.Burstall (May 1976), the manuscript was published as Dijkstra, E.W.: Selected Writings on Computing: A Personal Perspective, pp. 215–216. Springer, Heidelberg (1982) ISBN 0-387-90652-5
Dijkstra, E.W.: EWD578: More about the function “fusc” (a sequel to EWD570) (May 1976), the manuscript was published as Dijkstra, E.W.: Selected Writings on Computing: A Personal Perspective, pp. 230–232. Springer, Heidelberg (1982)
Fokkinga, M.M.: Law and Order in Algorithmics. Ph.D. thesis, University of Twente (February 1992)
Fokkinga, M.M., Meijer, E.: Program calculation properties of continuous algebras. Tech. Rep. CS-R9104, Centre of Mathematics and Computer Science, CWI, Amsterdam (January 1991)
Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundamenta Informaticae (XX), 1–14 (2005)
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete mathematics, 2nd edn. Addison-Wesley Publishing Company, Reading (1994)
Henglein, F.: Generic discrimination: Sorting and partitioning unshared data in linear time. In: Thiemann, P. (ed.) Proceedings of the 13th ACM Sigplan International Conference on Functional Programming (ICFP 2008), Victoria, BC, Canada, September 22–24, pp. 91–102. ACM, New York (2008)
Hinze, R.: Generalizing generalized tries. Journal of Functional Programming 10(4), 327–351 (2000)
Hinze, R.: Memo functions, polytypically! In: Jeuring, J. (ed.) Proceedings of the 2nd Workshop on Generic Programming, Ponte de Lima, Portugal, pp. 17–32 (July 2000), The proceedings appeared as a technical report of Universiteit Utrecht, UU-CS-2000-19
Hinze, R.: Functional Pearl: Streams and unique fixed points. In: Thiemann, P. (ed.) Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), pp. 189–200. ACM Press, New York (2008)
Hinze, R.: Functional Pearl: The Bird tree. J. Functional Programming 19(5), 491–508 (2009)
Hinze, R.: Scans and convolutions—a calculational proof of Moessners theorem. In: Scholz, S.B. (ed.) Post-proceedings of the 20th International Symposium on the Implementation and Application of Functional Languages (IFL 2008), University of Hertfordshire, UK,September 10–12. LNCS, vol. 5836, Springer, Heidelberg (2009)
Hinze, R.: Lifting operators and laws (2010), http://www.comlab.ox.ac.uk/ralf.hinze/Lifting.pdf
Hinze, R., Löh, A.: Guide2lhs2tex (for version 1.13) (February 2008), http://people.cs.uu.nl/andres/lhs2tex/
Hutton, G., Meijer, E.: Functional Pearl:Back to basics: Deriving representation changers functionally. J. Functional Programming 6(1), 181–188 (1996)
Karczmarczuk, J.: Generating power of lazy semantics. Theoretical Computer Science 187, 203–219 (1997)
Knuth, D.E.: The Art of Computer Programming, Sorting and Searching, 2nd edn., vol. 3. Addison-Wesley Publishing Company, Reading (1998)
Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, 2nd edn. Springer, Heidelberg (1998)
McBride, C., Paterson, R.: Functional Pearl: Applicative programming with effects. Journal of Functional Programming 18(1), 1–13 (2008)
McIlroy, M.D.: Power series, power serious. J. Functional Programming 3(9), 325–337 (1999)
McIlroy, M.D.: The music of streams. Information Processing Letters 77, 189–195 (2001)
Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall International, Englewood Cliffs (1989)
Peyton Jones, S.: Haskell 98 Language and Libraries. Cambridge University Press, Cambridge (2003)
Rutten, J.: Fundamental study: Behavioural differential equations: A coinductive calculus of streams, automata, and power series. Theoretical Computer Science 308, 1–53 (2003)
Rutten, J.: A coinductive calculus of streams. Math. Struct. in Comp. Science 15, 93–147 (2005)
Röjemo, N.: Garbage collection, and memory efficiency, in lazy functional languages. Ph.D. thesis, Chalmers University of Technology (1995)
Sloane, N.J.A.: The on-line encyclopedia of integer sequences (2009), http://www.research.att.com/~njas/sequences/
Thue, A.: Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen. Skrifter udgivne af Videnskaps-Selskabet i Christiania, Mathematisk-Naturvidenskabelig Klasse 1, 1–67 (1912), reprinted in Thue’s Selected Mathematical Papers (Oslo: Universitetsforlaget, 413–477 (1977)
Turner, D.: A new implementation technique for applicative languages. Software - Practice and Experience 9, 31–49 (1979)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hinze, R. (2010). Reasoning about Codata. In: Horváth, Z., Plasmeijer, R., Zsók, V. (eds) Central European Functional Programming School. CEFP 2009. Lecture Notes in Computer Science, vol 6299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17685-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-17685-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17684-5
Online ISBN: 978-3-642-17685-2
eBook Packages: Computer ScienceComputer Science (R0)