Streams and Unique Fixed Points
Ralf Hinze ( Computing Laboratory )
- 16:30 3rd June 2008 ( week 7, Trinity Term 2008 )Lecture Theatre A
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
is elegant and fun to use.
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
is elegant and fun to use.
Share this:
