Quine theory
As stated before, any Turing-complete language admits (at least) one quine.
The complete proof is quite long, but if we rely on some theorems, we can introduce a kind of short proof that would help us to understand how to code a quine, including a BF quine.
Definitions and theorems
Note: these definitions and theorems might not be the exact ones but a reduced version, enough to understand the proof
- A computable function N is a function that can be computed using a Turing-complete language. We will use functions with integer parameters (0 or more)
- Any computable function N can be related to an integer n in an injective way (one function : one integer; and one integer : at most one function)
- E.g. our source code can be considered as a set of chars, themselves a huge amount of bits, aka a number in its binary form
- The Universality theorem states that a computable function exists, named U, such that U(n) does the same job than N()
- This is what we called an interpreter.
- In other words, from a number, we can execute the corresponding program, if it exists (remember: injective way, so some integers may be invalid)
- The parameterization theorem, also called smn theorem states that a computable function S such that, for any integers n and m, s(n,m) does the same job than N(m)
- In this application, m is a fixed parameter of N
- Let's call H a computable function over (valid) integers, called transformation
- In other words, we transform a program identification number into another program's one
Let's start
Let's first prove there H admits a fixed point
- Consider a computable function N and its identification number n
- Consider S(n,n), the computable function obtained when executing N(n), N with a fixed parameter value which is its one identification number n
- Consider H(S(n,n)), the computable function obtained when transforming by H the computable function N(n)
- Let's have an integer m = H(S(n,n)). Such H(S(n,n)) is a computable function, with a single parameter n, and this function will be called M, identified by its number m
- Thanks to the universality theorem, if we know m, we can execute M
- Now, consider M(m)
- By definition, M(m) = S(m,m)
- By construction, M(m) = H(S(m,m))
- Conclusion : S(m,m) is a fixed point of computable function H
Apply to quine
Let's now say H is the function with a parameter n, that prints source code of program N.
We proved that there is at least one computable function, named quine that is a fixed point of H, so quine and H(quine) do the same job.
What does H(quine) does ? It displays quine source code. So quine does the same, and prints its own source code.
Quine construction
In order to get a quine, we saw that we need a function M, given by its value m. This means we needs in theory an interpreter to do that.
Actually, we can restrict this to an interpreter able to interpret m which is H(...). So our source code needs to be able to interpret H at least - other functions are not really mandatory.
And as our H is "Print source code of given program", then it's quite easy to implement.
- First, we need to declare a data part in our code
- Then a function H to print the data as data declaration
- Finally, print the data as contents
