Functional pearl: streams and unique fixed points

ABSTRACT

Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a fact that is not very widely appreciated. We show that this property gives rise to a simple and attractive proof technique essentially bringing equational reasoning to the coworld. In fact, we redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators building on the cornerstone of unique solutions. The development is constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. Finally, we rephrase the proof of uniqueness using generalised algebraic data types.

REFERENCES

• 1: Peter Aczel , Nax Paul Mendler, A Final Coalgebra Theorem, Category Theory and Computer Science, p.357-365, September 05-08, 1989
• 2: Thierry Coquand, Infinite objects in type theory, Proceedings of the international workshop on Types for proofs and programs, p.62-78, January 1994, Nijmegen, The Netherlands
• 3: Jeremy Gibbons , Graham Hutton, Proof Methods for Corecursive Programs, Fundamenta Informaticae, v.66 n.4, p.353-366, January 2005
• 4: Ronald L. Graham, Donald E. Knuth, and Oren Patashnik. Concrete mathematics. Addison-Wesley, 2nd edition, 1994.
• 5: Ralf Hinze. Fun with antom types. In Jeremy Gibbons and Oege de Moor, editors, The Fun of Programming, pages 245--262. Palgrave Macmillan, 2003. ISBN 1-4039-0772-2 hardback, ISBN 0-333-99285-7 paperback.
• 6: Ralf Hinze and Andres Löh. Guide2lhs2tex (for version 1.13), February 2008. http://people.cs.uu.nl/andres/lhs2tex/.
• 7: Jerzy Karczmarczuk, Generating power of lazy semantics, Theoretical Computer Science, v.187 n.1-2, p.203-219, Nov. 15, 1997 [doi>10.1016/S0304-3975(97)00065-0]
• 8: M. Douglas McIlroy, The music of streams, Information Processing Letters, v.77 n.2-4, p.189-195, Feb. 1, 2001 [doi>10.1016/S0020-0190(00)00201-5]
• 9: M. Douglas McIlroy, Power series, power serious, Journal of Functional Programming, v.9 n.3, p.325-337, May 1999 [doi>10.1017/S0956796899003299]
• 10: Simon Peyton Jones. Haskell 98 Language and Libraries. Cambridge University Press, 2003.
• 11: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 12: J. J. M. M. Rutten, Behavioural differential equations: a coinductive calculus of streams, automata, and power series, Theoretical Computer Science, v.308 n.1-3, p.1-53, 3 November 2003 [doi>10.1016/S0304-3975(02)00895-2]
• 13: J. J. M. M. Rutten, A coinductive calculus of streams, Mathematical Structures in Computer Science, v.15 n.1, p.93-147, February 2005 [doi>10.1017/S0960129504004517]
• 14: Neil J.A. Sloane. The on-line encyclopedia of integer sequences. http://www.research.att.com/ njas/sequences/.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Design, Languages, Theory, Verification

Keywords:
coinduction, finite calculus, generating functions, recurrences, streams, unique fixed points