Complexity of Fractran and productivity

Abstract. In functional programming languages the use of infinite struc-tures is common practice. For total correctness of programs dealing with infinite structures one must guarantee that every finite part of the result can be evaluated in finitely many steps. This is known as productivity. For programming with infinite structures, productivity is what termina-tion in well-defined results is for programming with finite structures. Fractran is a simple Turing-complete programming language invented by Conway. We prove that the question whether a Fractran program halts on all positive integers is Π02-complete. In functional programming, pro-ductivity typically is a property of individual terms with respect to the inbuilt evaluation strategy. By encoding Fractran programs as specifi-cations of infinite lists, we establish that this notion of productivity is Π02-complete even for some of the most simple specifications. Therefore it is harder than termination of individual terms. In addition, we explore generalisations of the notion of productivity, and prove that their com-putational complexity is in the analytical hierarchy, thus exceeding the expressive power of first-order logic.