  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.
