Typical arguments for results like Kleene's Second Recursion Theorem and the existence of self-writing computer programs bear the fingerprints of equational reasoning and combinatory logic. In fact, the connection of combinatory logic and computability theory is very old, and this paper extends this connection in new ways. In one direction, we counter the main trend in both computability theory and combinatory logic of heading straight to undecidability. Instead, this paper proposes using several very small equational logics to examine results in computability theory itself. These logics are decidable via term rewriting. We argue that they have something interesting to say about computability theory. They are closely related to fragments of combinatory logic which are decidable, and so this paper contributes to the study of such fragments. The paper has a few surprising results such as a classification of quine programs (programs which output themselves) in two decidable fragments. The classification goes via examination of normal forms in term rewriting systems, hence the title of the paper. The classification is an explanation of why all quine programs (in any language) are "pretty much the same, except for inessential details." In addition, we study the relational structure whose objects are the programs with the relation "p expresses q" meaning that if the program p is run on nothing, then it eventually outputs the program q.
翻译:[translated abstract in Chinese]
关于克莱恩第二递归定理及自写入计算机程序存在性的典型论证,都带有等式推理和组合逻辑的痕迹。事实上,组合逻辑与可计算性理论的联系由来已久,本文以新的方式拓展了这一关联。一方面,我们反对可计算性理论与组合逻辑中直接迈向不可判定性的主流趋势,转而提出使用若干极小的等式逻辑系统来审视可计算性理论本身的结果。这些逻辑系统可通过项重写实现可判定性,并被认为能对可计算性理论提供富有洞见的阐释。由于它们与可判定的组合逻辑片段密切相关,本研究亦为这类片段的理论探索做出贡献。本文包含若干出人意料的结论,例如在两个可判定片段中对自指程序(输出自身的程序)的分类。该分类通过考察项重写系统中的范式结构完成,这也是论文标题的由来。分类结果揭示了为何所有自指程序(无论何种语言)本质上"除无关紧要的细节外大体相同"。此外,我们还研究了以程序为对象的关系结构,其中关系"p表达q"指:当程序p在无输入状态下运行,最终会输出程序q。