Enhanced Regular Corecursion for Data Streams

We propose a simple calculus for processing data streams (infinite flows of data series), represented by finite sets of equations built on stream operators. Furthermore, functions defining streams are regularly corecursive, that is, cyclic calls are detected, avoiding non-termination as happens with ordinary recursion in the call-by-value evaluation strategy. As we illustrate by several examples, the combination of such two mechanisms provides a good compromise between expressive power and decidability. Notably, we provide an algorithm to check that the stream returned by a function call is represented by a well-defined set of equations which actually admits a unique solution, hence access to an arbitrary element of the returned stream will never diverge.