Streams

A stream is an infinite sequence of data elements

Theory

We specify a stream by means of a set of equations. We developed techniques for automatically proving that streams are well-defined and/or productive and/or equal.

Well-definedness of Streams by Termination, appeared at RTA 2009
Well-definedness of Streams by Transformation and Termination, extended version of RTA 2009 paper, appeared in LMCS
A tool for applying the technique from the above papers together with several examples
A Tool proving Well-definedness of Streams using Termination Tools, description of the above mentioned tool, appeared at CALCO 2009
Proving Productivity in Infinite Data Structures, appeared at RTA 2010
Proving Equality of Streams Automatically, accepted for RTA 2011

Visualization

Boolean streams can be visualized by turtle visualization. Fix a stream, a number N and two angles a0 and a1. Then the elements of the stream are traversed: if the symbol 0 is read then the drawing direction is moved a0 degrees to the right; if the symbol 1 is read then the drawing direction is moved a1 degrees to the left. In both cases after doing so a line of unit length is drawn. This is repeated N times.

The Fibonacci stream FIB, defined by
FIB = f(FIB)
for the stream function f defined by
f(0:s) = 0:1:f(s)
f(1:s) = 0:f(s)
The stream Q, defined by
Q = 1:f(Q)
for the stream function f defined by
f(0:s) = 1:0:f(s)
f(1:s) = 0:0:1:f(s)
A paper on Turtle graphics of morphic streams was written, giving criteria for turtles to be finite, fractal or space filling, and including many examples.
This theory on turtle graphics and many other issues around infinity has been elaborated to a book Spelen met oneindigheid: verrassende figuren en patronen in Dutch, for a wider audience.