On the productivity of recursive list definitions

Abstract

Several related notions of the productivity are presented for functional languages with lazy evaluation. The notion of productivity captures the idea of computability, of progress of infinite-list programs. If an infinite-list program is productive , then every element of the list can be computed in finite “time.” These notions are used to study recursive list definitions, that is, lists defined by l where l = fl . Sufficient conditions are given in terms of the function f that either guarantee the productivity of the list or its unproductivity. Furthermore, a calculus is developed that can be used in verifying that lists defined by l where l = f I are productive. The power and the usefulness of our theory are demonstrated by several nontrivial examples. Several observations are given in conclusion.