Ralf Hinze
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.
Supplemental Material
Available for Download
Slides from the presentation
Supplemental material for: Functional pearl: streams and unique fixed points
- P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, and A. Poigné, editors, Category Theory and Computer Science (Manchester), LNCS 389, pages 357--365, 1989. Springer. Google Scholar
Digital Library
- Thierry Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, LNCS 806, pages 62--78, 1994. Springer. Google ScholarDigital Library
- Jeremy Gibbons and Graham Hutton. Proof methods for corecursive programs. Fundamenta Informaticae, (XX): 1--14, 2005. Google ScholarDigital Library
- Ronald L. Graham, Donald E. Knuth, and Oren Patashnik. Concrete mathematics. Addison-Wesley, 2nd edition, 1994.Google Scholar
- 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.Google ScholarCross Ref
- Ralf Hinze and Andres Löh. Guide2lhs2tex (for version 1.13), February 2008. http://people.cs.uu.nl/andres/lhs2tex/.Google Scholar
- Jerzy Karczmarczuk. Generating power of lazy semantics. Theoretical Computer Science, (187): 203--219, 1997. Google ScholarDigital Library
- M. Douglas McIlroy. The music of streams. Information Processing Letters, (77): 189--195, 2001. Google ScholarDigital Library
- M. Douglas McIlroy. Power series, power serious. J. Functional Programming, 3 (9): 325--337, May 1999. Google ScholarDigital Library
- Simon Peyton Jones. Haskell 98 Language and Libraries. Cambridge University Press, 2003.Google Scholar
- S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In J. Lawall, editor, Proceedings of the 11th ACM SIGPLAN international conference on Functional programming, Portland, 2006, pages 50--61. ACM Press, 2006. Google ScholarDigital Library
- J.J.M.M. Rutten. Fundamental study - Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science, (308): 1--53, 2003. Google ScholarDigital Library
- J.J.M.M. Rutten. A coinductive calculus of streams. Math. Struct. in Comp. Science, (15): 93--147, 2005. Google ScholarDigital Library
- Neil J.A. Sloane. The on-line encyclopedia of integer sequences. http://www.research.att.com/ njas/sequences/.Google Scholar
Index Terms
- Functional pearl: streams and unique fixed points
Recommendations
Functional pearl: streams and unique fixed points
ICFP '08Streams, 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 ...
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2
Higman's lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman's Lemma in the ACL2 theorem prover. Our formalization is based on a ...
Pure type systems with corecursion on streams: from finite to infinitary normalisation
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingIn this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is ...
Reviews
Wolfgang Schreiner
Streams, infinite sequences of elements, play an important role in various areas of mathematics and computer science. On the one hand, they represent a fundamental concept of discrete mathematics, where infinite integer sequences are investigated, for example, for solving recurrences. On the other hand, they serve an operational purpose as data types in lazy functional programming languages, such as Haskell, where mutually recursive function definitions can give rise to programs operating on streams-with lazy evaluation, only finite prefixes of the streams are actually computed. This paper combines the constructive with the fundamental aspects, by introducing a calculus whose basic elements-streams and stream operators-are implemented in Haskell and used to reformulate various mathematical theories. The core idea is a new technique for proving the equality of two streams. Hinze shows that a recursive stream equation, provided that it satisfies some syntactic constraints, has a unique solution; thus, to prove that two streams, s and t , are equal, it suffices to unfold their definitions to forms s = X s and t = X t for the same function X . The calculus is applied to numerous examples in discrete mathematics: streams used to capture recurrences, finite calculus (difference equations and summations), and generating functions (handling of power series). The presentation is lively and fun to read; by casting the formal concepts into the Haskell framework-for example, the proof of uniqueness uses Haskell's generalized algebraic data types-the results may become accessible to a wider audience. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments