Enhanced Regular Corecursion for Data Streams

TL;DR

This paper introduces a calculus for data streams that combines regular corecursion with a set of equations, enabling expressive and decidable stream processing with guaranteed termination for element access.

Contribution

It presents a novel calculus that integrates regular corecursion with equation-based stream definitions, ensuring decidability and unique solutions.

Findings

The calculus allows defining infinite data streams with guaranteed termination.

An algorithm verifies well-formedness and unique solutions of stream equations.

The approach balances expressive power with decidability in stream processing.

Abstract

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-formed set of equations which actually admits a unique solution, hence access to an arbitrary element of the returned stream will never diverge.