Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Functional pearl: streams and unique fixed points
Hinze R. ACM SIGPLAN Notices43 (9):189-200,2008.Type:Article
Date Reviewed: Jun 11 2009

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 = Xs and t = Xt 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.

Reviewer:  Wolfgang Schreiner Review #: CR136944 (1002-0166)
Bookmark and Share
  Featured Reviewer  
 
Correctness Proofs (D.2.4 ... )
 
 
Applicative (Functional) Languages (D.3.2 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Specification Techniques (F.3.1 ... )
 
 
Applicative (Functional) Programming (D.1.1 )
 
 
Language Classifications (D.3.2 )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Correctness Proofs": Date
Using symbolic execution for verification of Ada tasking programs
Dillon L. (ed) ACM Transactions on Programming Languages and Systems 22(6): 643-669, 2000. Type: Article
Jul 1 1991
Reasoning about programs (videotape)
Dijkstra E. (ed), University Video Communications, Stanford, CA, 1990. Type: Book
Dec 1 1992
Error-free software
Baber R., John Wiley & Sons, Inc., New York, NY, 1991. Type: Book (9780471930167)
May 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy