Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algebra of Self-Replication

Lawrence S. Moss

TL;DR

The paper investigates decidable equational logics that capture diagonalization phenomena in computability, focusing on a diagonal operator and two proofs of Kleene's Second Recursion Theorem. It develops small, terminating and confluent term-rewriting fragments built from constants $e$, $d$ and binary operators $+$ and $\mathop{\mathrm{@}}$, later extending with $w$, and further with universal and $s^1_1$-style constants, to analyze normal forms, quines, and cycles. By constructing computable and non-computable models (interpreting $\mathop{\mathrm{@}}$ as Kleene application) and proving decidability of the word problem in the core fragments, the work reveals how quines are uniquely determined within these logics and how adding write operations or richer universals generates cycles and twin phenomena. The results highlight a trade-off between expressive power and tractability, illustrate connections between equational logics and fragments of combinatory logic, and raise open questions about extensionality and interpretation in broader programming languages. The methods provide a framework for analyzing self-reproduction and diagonalization in a controlled, computable setting with potential implications for understanding the foundations of self-referential computation.

Abstract

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.

Algebra of Self-Replication

TL;DR

The paper investigates decidable equational logics that capture diagonalization phenomena in computability, focusing on a diagonal operator and two proofs of Kleene's Second Recursion Theorem. It develops small, terminating and confluent term-rewriting fragments built from constants , and binary operators and , later extending with , and further with universal and -style constants, to analyze normal forms, quines, and cycles. By constructing computable and non-computable models (interpreting as Kleene application) and proving decidability of the word problem in the core fragments, the work reveals how quines are uniquely determined within these logics and how adding write operations or richer universals generates cycles and twin phenomena. The results highlight a trade-off between expressive power and tractability, illustrate connections between equational logics and fragments of combinatory logic, and raise open questions about extensionality and interpretation in broader programming languages. The methods provide a framework for analyzing self-reproduction and diagonalization in a controlled, computable setting with potential implications for understanding the foundations of self-referential computation.

Abstract

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.
Paper Structure (21 sections, 18 theorems, 45 equations, 3 figures)

This paper contains 21 sections, 18 theorems, 45 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Kleene's Second Recursion Theorem: two proofs
  3. Some problems about program "expression"
  4. Program expression
  5. Plan for the paper
  6. Background
  7. Equational logic, term rewriting, and computable algebras
  8. Combinatory algebras
  9. Related work
  10. Equational logic of diagonalization
  11. The idea behind the equations, in plain terms
  12. The quine program in this example
  13. A comment on the equations
  14. Rewriting system and normal forms
  15. Characterization of quines
  16. ...and 6 more sections

Key Result

theorem 1

Let $p$ be a program, consider as a function $[\![ p ]\!]$ of two arguments. There is a program $q^*$ so that for all $r$,

Figures (3)

  • Figure 1: The full set $E$ of equations used in this paper.
  • Figure 2: The set $E$ of equations for the language studied in Section \ref{['section-equation-d']}. The signature has constants $\hbox{\tt d}$ and $\hbox{\tt e}$, and function symbols $+$ and $\mathop{\mathrm{@}}\nolimits$.
  • Figure 3: The set $E$ of equations used for the language with constants $\hbox{\tt d}$, $\hbox{\tt e}$, and $\hbox{\tt w}$, and operations $+$ and $\mathop{\mathrm{@}}\nolimits$.

Theorems & Definitions (30)

  • theorem 1
  • proof
  • theorem 2: MeseguerGoguen, Theorem 51
  • theorem 3: Perkins Perkins
  • theorem 4: Combinatory Completeness
  • proposition 1
  • proposition 2
  • proof
  • proposition 3
  • proof
  • ...and 20 more