Stream Productivity by Outermost Termination

Hans Zantema
(TU Eindhoven)
Matthias Raffelsieper
(TU Eindhoven)

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.

In Maribel Fernández: Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2009), Brasilia, Brazil, 28th June 2009, Electronic Proceedings in Theoretical Computer Science 15, pp. 83–95.
Published: 26th January 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.15.7 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org