Fractran和产能的复杂性
Complexity of Fractran and Productivity
摘要：
在函数式程序设计语言中，使用无限结构是常见的做法。对于处理无限结构的程序的完全正确性，必须保证结果的每个有限部分都可以在多个步骤中计算。这被称为生产力。对于具有无限结构的编程，生产率是定义良好的结果中的终止对于具有有限结构的编程的意义。Fractran是Conway发明的一种简单的图灵完备程序设计语言。我们证明了Fractran程序是否在所有正整数上停止的问题是Pi^0_2-完全的。在函数式编程中，生产率通常是相对于内置评估策略的单个术语的属性。通过将Fractran程序编码为无限列表的规范，我们建立了即使对于最简单的规范，这种生产率的概念也是Pi^0_2-完全的。因此，它比终止个别条款更难。此外，我们还在项重写的框架下探讨了生产力概念的可能的推广，并证明了它们的计算复杂性是Pi^1_1-完备的，从而超过了一阶逻辑的表达能力。
英文摘要：
In functional programming languages the use of infinite structures 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 termination 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 Pi^0_2-complete. In functional programming, productivity typically is a property of individual terms with respect to the inbuilt evaluation strategy. By encoding Fractran programs as specifications of infinite lists, we establish that this notion of productivity is Pi^0_2-complete even for the most simple specifications. Therefore it is harder than termination of individual terms. In addition, we explore possible generalisations of the notion of productivity in the framework of term rewriting, and prove that their computational complexity is Pi^1_1-complete, thus exceeding the expressive power of first-order logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
