期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2009
卷号：15
页码：83-95
DOI：10.4204/EPTCS.15.7
出版社：Open Publishing Association
摘要：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.
