Stream Productivity by Outermost Termination

TL;DR

This paper establishes a formal link between stream productivity and outermost termination in term rewriting systems, enabling automatic proofs of productivity for certain stream specifications.

Contribution

It introduces a novel characterization of stream productivity as outermost termination, allowing existing termination tools to automatically verify productivity.

Findings

Productivity is equivalent to outermost termination with an added rule.

For non-branching stream specifications, balancedness is automatic.

Existing termination tools can be used to automatically prove productivity.

Abstract

Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. A core property is productivity: unfolding the equations produces the intended stream in the limit. In this paper we show that productivity is equivalent to termination with respect to the balanced outermost strategy of a TRS obtained by adding an additional rule. For specifications not involving branching symbols balancedness is obtained for free, by which tools for proving outermost termination can be used to prove productivity fully automatically.