# Has the notion of “non-cheating” quines been formalised?

Informally, it is often said that some quines "cheat", such as those that read their own source code from memory, or the case where a program consisting of the empty string happens to output the empty string.

Quines that are considerd to be "non-cheating" always seem to have the same structure. There is some data structure (usually, but not always, a string) which contains some representation of the source code. This structure is read twice, once to reformat it into the code part of the final output, and a second time where it's copied verbatim to reproduce the data part. For example, the following Python example (which I just invented) has this structure:

x = """x = {0}{1}{0}
print x.format(chr(34)*3,x)"""
print x.format(chr(34)*3,x)


The string 'x' is referred to twice in the last line, once to reformat it, and a second time to paste it verbatim into the reformatted string.

My question is whether this notion of "cheating" or "non-cheating" quines has been, or can be, formalised. That is to say, if we are given a formal specification of a language and its semantics, and we are also given an example of a quine in that language, is there a well-defined way to say, in principle, whether that quine is "cheating" or not? Or is this notion of "cheating" inherently too vague to admit a formal definition?

If this notion can be formally defined, is it possible to have a language that only admits "non-cheating" quines, and is an example of such a language known?

• I wonder if a quines tag would be useful? If it would, could someone with the necessary rep create it and apply it to my question? – Nathaniel Aug 20 '16 at 8:12

Most formal semantics for programing languages tend to keep things simple, in particular, it's pretty rare to have the ability to express "grabbing your own source code" in a formal semantics.

This has the somewhat dubious advantage of disallowing some kinds of "cheating" by construction: the "cheat" is simply not part of the language semantics. In particular, a simple lambda calculus with simple string concatenation and printing primitives cannot implement many (any?) of the "cheats" you have in mind. In such a language, a quine might be a program which prints the exact string representation of it's own code. You can even avoid the print primitive if you allow returning the string rather than printing it. In that case, you only need string literals and concatenation.

It's a useful exercise to figure out various properties of quines in such a language. It's pretty easy to see that some variable will need to be repeated twice: there are no "linear" quines. However the statement

This structure is read twice, once to reformat it into the code part of the final output, and a second time where it's copied verbatim to reproduce the data part.

is a bit vague, and I'm not sure it's true in general, depending on the precise meaning of "copied verbatim".

• I can think of several ways that "cheating" could exist in such a language. In particular, depending on the details of the formalism, I would expect the empty string to output the empty string. – Nathaniel Aug 22 '16 at 0:30
• I'm aware that the concept I'm getting at is vague, but then, if it were precise I would have no need to ask a question about how to formalise it. To my mind, my second question (can we define a language with no cheating quines?) can only be answered after my first question (can we turn this vague concept of 'cheating' into a formal one?). – Nathaniel Aug 22 '16 at 0:35
• I think you can exclude the first case by definition: a quine needs to be a function definition $q:\mathrm{String}\rightarrow\mathrm{String}$ that prints it's own code. This prevents the "empty" loophole. For the "reads it's own code" loophole, I think this simply isn't possible in the simple language I outlined. Of course, other forms of cheating might exist (depending on the judge), but I feel this excludes the ones mentioned at least. – cody Aug 27 '16 at 1:52