Skip to main content
SpringerLink
Log in

Reasoning about Codata

  • Chapter
Central European Functional Programming School (CEFP 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6299))

Included in the following conference series:

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 to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. 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)

    Google Scholar 

  3. Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall Europe, London (1997)

    MATH  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Connelly, R.H., Morris, F.L.: A generalization of the trie data structure. Mathematical Structures in Computer Science 5(3), 381–418 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  6. Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  7. Curry, H., Feys, R.: Combinatory Logic, vol. 1. North-Holland, Amsterdam (1958)

    MATH  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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

    Book  MATH  Google Scholar 

  10. 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)

    Book  MATH  Google Scholar 

  11. Fokkinga, M.M.: Law and Order in Algorithmics. Ph.D. thesis, University of Twente (February 1992)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundamenta Informaticae (XX), 1–14 (2005)

    MathSciNet  MATH  Google Scholar 

  14. Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete mathematics, 2nd edn. Addison-Wesley Publishing Company, Reading (1994)

    MATH  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Hinze, R.: Generalizing generalized tries. Journal of Functional Programming 10(4), 327–351 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  17. 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

    Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Hinze, R.: Functional Pearl: The Bird tree. J. Functional Programming 19(5), 491–508 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  20. 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)

    Google Scholar 

  21. Hinze, R.: Lifting operators and laws (2010), http://www.comlab.ox.ac.uk/ralf.hinze/Lifting.pdf

  22. Hinze, R., Löh, A.: Guide2lhs2tex (for version 1.13) (February 2008), http://people.cs.uu.nl/andres/lhs2tex/

  23. Hutton, G., Meijer, E.: Functional Pearl:Back to basics: Deriving representation changers functionally. J. Functional Programming 6(1), 181–188 (1996)

    Article  Google Scholar 

  24. Karczmarczuk, J.: Generating power of lazy semantics. Theoretical Computer Science 187, 203–219 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  25. Knuth, D.E.: The Art of Computer Programming, Sorting and Searching, 2nd edn., vol. 3. Addison-Wesley Publishing Company, Reading (1998)

    MATH  Google Scholar 

  26. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, 2nd edn. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  27. McBride, C., Paterson, R.: Functional Pearl: Applicative programming with effects. Journal of Functional Programming 18(1), 1–13 (2008)

    Article  MATH  Google Scholar 

  28. McIlroy, M.D.: Power series, power serious. J. Functional Programming 3(9), 325–337 (1999)

    Article  MATH  Google Scholar 

  29. McIlroy, M.D.: The music of streams. Information Processing Letters 77, 189–195 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  30. Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall International, Englewood Cliffs (1989)

    MATH  Google Scholar 

  31. Peyton Jones, S.: Haskell 98 Language and Libraries. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  32. Rutten, J.: Fundamental study: Behavioural differential equations: A coinductive calculus of streams, automata, and power series. Theoretical Computer Science 308, 1–53 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  33. Rutten, J.: A coinductive calculus of streams. Math. Struct. in Comp. Science 15, 93–147 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  34. Röjemo, N.: Garbage collection, and memory efficiency, in lazy functional languages. Ph.D. thesis, Chalmers University of Technology (1995)

    Google Scholar 

  35. Sloane, N.J.A.: The on-line encyclopedia of integer sequences (2009), http://www.research.att.com/~njas/sequences/

  36. 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)

    MATH  Google Scholar 

  37. Turner, D.: A new implementation technique for applicative languages. Software - Practice and Experience 9, 31–49 (1979)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, England

    Ralf Hinze

Authors
  1. Ralf Hinze
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Department of Programming Languages and Compilers, Eötvös Loránd University, Pázmány Péter Sétány 1/C, 1117, Budapest, Hungary

    Zoltán Horváth  & Viktória Zsók  & 

  2. Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500, Nijmegen, GL, The Netherlands

    Rinus Plasmeijer

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation