5
$\begingroup$

A quine is a program that outputs its own source code without taking in any input. An example would be this (taken from here)

public class Quine {
    public static void main(String[] args) {
        char quote = 34;
        String[] code = {
"public class Quine {",
"    public static void main(String[] args) {",
"        char quote = 34;",
"        String[] code = {",
"        };",
"        for(int i=0; i<4; i++){",
"            System.out.println(code[i]);",
"        }",
"        for(int i=0; i<code.length; i++){",
"            System.out.println(quote + code[i] + quote + ',');",
"        }",
"        for(int i=4; i<code.length; i++){",
"            System.out.println(code[i]);",
"        }",
"    }",
"}",
        };
        for(int i=0; i<4; i++){
            System.out.println(code[i]);
        }
        for(int i=0; i<code.length; i++){
            System.out.println(quote + code[i] + quote + ',');
        }
        for(int i=4; i<code.length; i++){
            System.out.println(code[i]);
        }
    }
}

Running this produces exactly the same output as the source code. I've heard that the fixed point theorem applies, meaning that any turing-complete programming language will contain a quine. However, the more I thought about this the less it made sense.

The rules for the fixed point theorem in mathematics are that it must be continuous, bounded surface with no holes or 'cutting and gluing'. This seems to make no sense in terms of programming languages.

The first rule can be broken by the nature of characters as not continuous, for example there is no inbetween 'a' and 'b' in terms of ASCII encoding.

The second rule can be broken by stating that there can be infinitely many programs all equally valid, for example you could have System.out.println("");, System.out.println("a");, System.out.println("aa");...System.out.println("aaaaaaaaaaaaaaaaaaaaa");.

The third rule can be broken by saying that not all programs are valid, for example abstract System out.println(23");" is not valid, however the build output could be used as the output, ie

Main.java:2: error: class, interface, or enum expected
  public static void main(String[] args) {abstract System out.println(23");"
                                                   ^
Main.java:2: error: ')' expected
  public static void main(String[] args) {abstract System out.println(23");"
                                                                        ^
2 errors

If all but one of the rules are broken, then why does the fixed point theorem still apply?

$\endgroup$
  • 1
    $\begingroup$ There are many different theorems known by the name of 'fixed point theorem'. The one you found indeed doesn't appear to be relevant for the existence of a quine. Perhaps Tarski's fixpoint theorem or Kleene's fixpoint theorem could be used instead. $\endgroup$ – Discrete lizard May 30 '18 at 21:31
  • $\begingroup$ @Discretelizard That would make sense. Should I delete this post or leave it? $\endgroup$ – Nathan Wood May 30 '18 at 21:32
  • $\begingroup$ Well, I did explain a flaw in your reasoning, but the question "Why Does the Fixed Point Theorem Apply to Quines?" doesn't seem to be answered yet. There's no harm in leaving this question be as it is certainly possible to answer it. $\endgroup$ – Discrete lizard May 30 '18 at 21:35
5
$\begingroup$

The fixed point theorem you are mentioning is the Brouwer fixed-point theorem. It is possible that there is some way to give a topology to computer programs and use homotopy theory to derive the existence of a fixed point, but a way to do this does not immediately spring to mind. Your objections do not completely make sense in the language of topology:

  1. A topological space is not described as continuous, but rather connected or path connected. It is possible for a two-point space to be path connected even though there are no "in between" points along the path.
  2. The interval $[0,1]$ has infinitely many points yet is bounded. It is not clear that infinitely many programs with the same output is an issue.
  3. Invalid programs can be considered valid by giving them well-defined output. For example, the compiler error message. Or we restrict to the subspace of valid programs.

Out of my own interest for understanding how Quines follow from a fixed-point theorem, I'm going to outline a proof. This is derived from this webpage.

Let $S$ be the set of all finite strings from some alphabet, say ASCII, and let $P\subset S$ be the subset of all valid programs for some specific Turing-complete programming language. Let $I:P\times S\to S\cup\{\bot\}$ be the function where $I(p,s)$ is the output from running program $p$ with input $s$, else $\bot$ if the program does not halt (think of $I$ as an interpreter). Define tuple functions like ${\times}:S\times S\to S$ by $x\times y = ``\mathrm{(}"+x+``\mathrm{,}"+y+``\mathrm{)}"$. We define them in such a way that you can recover $x$ and $y$, for the purpose of changing the number of arguments to a function.

The programming language is universal, meaning there is some program $i\in P$ such that $I(p,s)=I(i,p\times s)$ for all $p\in P$ and $s\in S$. This can be interpreted as saying that $I$ can be implemented in itself as $i$.

There is a partial evaluation function $\pi:P\times S\to P$ with the property that $I(\pi(p,s),t)=I(p,s\times t)$ for all $p\in P$ and $s,t\in S$. In fact, there is a program $p_\pi$ implementing it in the sense that $\pi(p,s)=I(p_\pi,p,s)$ for all $p\in P$ and $s\in S$. In Java, this can correspond to pasting in $s$ as a string literal.

Fixed-point theorem. If $F:P\to P$ is a computable function, then there is a program $p\in P$ such that for all $s\in S$, $I(p,s)=I(F(p),s)$.

Proof. Let $\Delta:P\to P\times P$ be the computable function $\Delta(p)=p\times p$. The composition $F\circ \pi\circ\Delta$ is the computable function $q\mapsto F(\pi(q,q))$, where $\pi(q,q)$ is the program from giving $q$ to itself as one of its inputs. Let $m\in P$ be the program for the composition $F\circ\pi\circ\Delta$, so $I(m,q\times s)=I(F(\pi(q,q)),s)$ for all $s\in S$ (*). Let $p=\pi(m,m)$. Then, $$I(p,s)=I(\pi(m,m),s)=I(m,m\times s)=I(F(\pi(m,m)),s)=I(F(p),s)$$ where the third equality uses $q=m$ in (*). QED

Now to prove that there is a Quine. Let $\eta:P\to P$ be a computable function such that $I(\eta(p),\emptyset)=p$ for all $p\in P$. That is, $\eta$ wraps a program text up in a print statement. Applying the fixed point theorem, there is a program $p\in P$ such that $I(p,\emptyset)=I(\eta(p),\emptyset)$. That is, $I(p,\emptyset)=p$, so $p$ is a Quine.

This is all very much constructive, so you can use it to create (inefficient) Quines.

$\endgroup$
6
$\begingroup$

As Discrete Lizard points out, there exist more than one "fixed point theorem." The one you're mentioning makes sense in terms of topology and geometry, but you're right to realize that it does not apply to programming languages.

It turns out, though, that a more general notion of continuity, called Scott Continuity, can give you something that is applicable, namely the Kleene fixed-point theorem:

Any Scott-continuous function over a directed-complete partial order has a least fixed point.

An earlier, and easier to understand, version of this is given by Knaster-Tarski:

Any monotone function over a complete lattice has a fixed-point. In fact, the fixed points of such a function form a complete lattice.

$\endgroup$
  • 1
    $\begingroup$ Thanks! The person who said it originally just said 'fixed point theorem' with no other words, so I assumed that there was only one. $\endgroup$ – Nathan Wood May 30 '18 at 21:55
  • $\begingroup$ @NathanWood There is in fact only one fixed point theorem. But applying the concept of fixed-pointedness to different scenarios requires different interpretations of the rules for the function. It does not however change the result of the theorem - that all functions have one input that generates an output identical to that input. $\endgroup$ – slebetman May 31 '18 at 4:51
  • $\begingroup$ @slebetman I wouldn't call that being "the same theorem," but anyway it seems many of these fixed-point theorems are instances of Lawvere's fixed-point theorem (although the folks at mathoverflow didn't seem to think the Brouwer fixed-point theorem was a consequence of it). $\endgroup$ – Kyle Miller Jun 2 '18 at 0:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.