Stream productivity by outermost termination

H. Zantema, M. Raffelsieper

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)
2 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming (WRS'09, Brasilia, Brazil, June 28, 2009)
EditorsM. Fernández
Pages83-95
DOIs
Publication statusPublished - 2010

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume15
ISSN (Print)2075-2180

Fingerprint

Dive into the research topics of 'Stream productivity by outermost termination'. Together they form a unique fingerprint.

Cite this