proof of existing quine
in [Logic]
|
Prev: Cruci Al, the O.R. Yemin, the R.M., o dyna, mics.
Next: The best way of writing FOL with identity and membership.
From: kelsar777 on 7 May 2010 04:33 How can we prove for given programming language that there exists or not a quine (program which produces its own code)?
From: Paul N on 7 May 2010 07:02 On 7 May, 09:33, kelsar777 <kelsar...(a)gmail.com> wrote: > How can we prove for given programming language that there exists or > not a quine (program which produces its own code)? For many languages, I would have thought that the easiest way to prove one exists is to write one. Since most languages can produce arbitrary output, with ways to calculate an output rather than having to specify it as part of the program, I would have thought it would be possible to write a quine in most languages. So proving that no quine exists in a particular language is likely to focus on some particular flaw of that particular language.
From: Ben Bacarisse on 7 May 2010 12:31
kelsar777 <kelsar777(a)gmail.com> writes: > How can we prove for given programming language that there exists or > not a quine (program which produces its own code)? A quine is a fixed-point of the function F defined by the compiler and the execution environment[1]. F takes a program text, p, and compiles and runs it to generate a string r = F(p). A fixed point of F is program text q = F(q): i.e. it is a quine. It is possible to prove that, under a reasonable set of conditions, all such F have a fixed point. The conditions exclude things like sounds compilers where the output domain is unrelated to the input domain. The proof has to be embedded in some theory of computation. For this purpose the simplest theory is probably that of the lambda-calculus. Search for things like "lambda-calculus fixed-point" and "Y combinator" and then ask yourself "is F likely to be expressible as a lambda expression?". [1] Interpreted languages have a null compiler! -- Ben. |