A program that computes on an infinite data structure, such as an infinite list or tree cannot be expected to terminate. But for it to behave properly, not only it must run forever, it also must compute arbitrarily precise approximations of the result in finite time. This property is known as productivity, and is the dual of termination. Productivity is well-known and has been studied in a deterministic setting. However, extending it to a probabilistic setting poses some formal challenges.

In this talk I will introduce a probabilistic extension of productivity , which we name Almost Sure Productivity (ASP). I will first look further into this duality between termination and productivity, which is essentially the duality between algebras and coalgebras, and present the theoretical background that will allow us to formalize the concept of ASP. Then I will define a core language for probabilistic computations on infinite lists and trees, and provide two methods for checking whether a program is ASP: an efficient but incomplete syntactic criterion, and a decision procedure based on model-checking probabilistic pushdown automata.