Enhancing expressivity of checked corecursive streams (extended version)

TL;DR

This paper introduces an enhanced approach to defining and manipulating streams, allowing for more expressive non-regular streams and ensuring well-defined access through runtime checks, extending previous techniques with new operators.

Contribution

It extends regular corecursion by adding operators and runtime checks, enabling the definition of more complex streams with guaranteed access safety.

Findings

Allows defining non-regular streams

Includes runtime checks for well-defined access

Adds an interleaving combinator with complex recursion

Abstract

We propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme.