As with my previous post, this post is another excerpt that will be included in my final Master’s thesis, but I decided it is interesting enough to post it on its own.
We start with a definition of diagonalization (or quotation), as discussed in The Gödelian Puzzle Book:
Definition 1: For an expression in which a variable occurs, we say that its diagonalization is the substitution of the variable with the quoted expression .
This definition allows us to represent self-referential expressions.
For example, let . Then, the diagonalization of it will be . In Lisp code:
> (define p (lambda (x) (list 'Boro 'is 'reading x))) > (p 'a-book) '(Boro is reading a-book) > (define d (lambda (p x) (p (list 'quote (p x))))) > (d p 'a-book) '(Boro is reading '(Boro is reading a-book))
As another example, let stand for “Boro is reading the diagonalization of x”, and let stand for `Boro is reading the diagonalization of “Boro is reading the diagonalization of x”`. That is, . But, the diagonalization of is simply , i.e. . So, refers to itself. In Lisp:
> (define q (lambda (x) (list 'Boro 'is 'reading (d identity x)))) > (define r (lambda (x) (d q x))) > (equal? (d q 'test) (r 'test)) #t
Based on these definitions, we will now show how to derive a Quine, which is a program that when evaluated returns its source code as an output – a metaprogram.
Note how we used
(d identity x) earlier, i.e. the diagonalization of x. This simply evaluates to
(list 'quote x).
Now, let’s consider the expression
(list x (list 'quote x)) which will return a list with two members:
x and its diagonalization:
> (define quine-1 (lambda (x) (list x (list 'quote x))))
What if we apply it to itself?
> (quine-1 quine-1) '(#<procedure:quine-1> '#<procedure:quine-1>)
Nothing useful. How about applying its quoted version?
> (quine-1 'quine-1) '(quine-1 'quine-1)
This is exactly why we picked the expression that contains a list of
x and its diagonalization. We wanted the evaluation of that expression to return the same expression.
It looks like we are on the right track. Finally, the Quine code that will reproduce itself is just taking the lambda and applying it to its quoted version:
((lambda (x) (list x (list 'quote x))) '(lambda (x) (list x (list 'quote x))))