Recall that the size of an S-expression is defined to be the number of characters needed to write it in standard form, i.e., with a single blank separating successive elements of each list.
So I'll measure the LISP complexity H(X) of an S-expression X by the size in characters |Y| of the smallest expression Y with value X. Given an S-expression X, I'll use X* to denote a minimal-size LISP expression for X, i.e., one with the property that its value is X and its size |X*| is the complexity H(X) of X.
And, as I said in Chapter I, we call a LISP expression elegant if it has the property that no smaller expression has the same value. Thus the size of an elegant expression is precisely equal to the complexity of its value.
Okay, here are two exercises for you to think about. The answers are at the end of this chapter.
First exercise. First of all, I'd like you to show that the complexity H((X Y)) of a pair (X Y) of objects is bounded by a constant c added to the sum H(X) + H(Y) of the individual complexities. In other words, try to see why
and how big c is.
Hint. If you are given elegant expressions for X and Y, how can you combine them into an expression for the pair (X Y)? And how will the sizes of these three expressions compare with each other? In other words, how many characters c do you need to add to stitch elegant expressions for X and Y together into an expression for the pair (X Y)?
Second exercise. For the second exercise, I'd like you to think about the complexity of an elegant LISP expression E. Can you show that its complexity is nearly equal to its size in characters? I.e., can you bound the absolute value of the difference between the size of E, |E|, and the complexity of E, H(E)?
Okay, if you can do these two warm-up exercises, I hope you begin to have some feeling for why elegant expressions are interesting. We can now go ahead and see why a formal axiomatic system A can't prove that a LISP expression E is elegant if E is substantially larger than the LISP implementation of the proof-checking algorithm for the formal axiomatic system A.
What's the proof-checking algorithm for A? Recall that it's defined in Chapter III to be a LISP function (valid-proof? X) that returns nil if X is not a valid proof and that returns the theorem that was demonstrated if X is a valid proof. And the idea of my proof is that I will construct an expression B (for Berry) that searches through all possible proofs X until X proves an assertion (is-elegant E) in which E's size is larger than B's size. Then B returns E's value as B's value, which, if it actually happened, would contradict the definition of elegance. Why? Because B is too small to produce E's value because E is an elegant expression that's larger than B.
Okay, that's the idea. But to simplify matters, let's imagine that all possible proofs X are in a numbered list, so there's a first S-expression X, a second one, etc. And let's give the proof-checking algorithm valid-proof? the number for the proof X instead of giving it X directly. So in this chapter our formal axiomatic system A is implemented in LISP as a one-argument function (fas N) that returns nil if the Nth proof is invalid, and that returns the theorem that was demonstrated if the Nth proof is valid. Let's also allow the formal axiomatic system to give up and stop running by returning ``stop'', which means that there are no more valid proofs. I.e., there are no valid proofs for larger N. Okay?
So now we can think of our formal axiomatic system abstractly as a numbered list of theorems, that may either be finite or infinite, and in which there may be blanks, i.e., places in the list with no theorem. And we'll just look at (fas 1), (fas 2), etc. searching for a theorem of the form (is-elegant E) in which E is larger than the size of the LISP expression B that is doing the search. If B finds such an elegant expression E, then B stops searching and returns the value of E. (Of course, this should never happen, not if E is really elegant!).
So here is the Berry paradox expression B that does this:
define expression
let (fas n) if = n 1 '(is-elegant x)
if = n 2 nil
if = n 3 '(is-elegant yyy)
[else] stop
let (loop n)
let theorem [be] display (fas n)
if = nil theorem [then] (loop + n 1)
if = stop theorem [then] fas-has-stopped
if = is-elegant car theorem
if > display size cadr theorem
display + 356 size fas
[return] eval cadr theorem
[else] (loop + n 1)
[else] (loop + n 1)
(loop 1)
And I've put a simple formal axiomatic system in it, one that
``proves'' that x and yyy are elegant, and then stops. The constant
356 that enables B to know its own size
was inserted in B by hand, because it turns out that
B is exactly 356 characters larger than the
lambda expression for the one-argument
function fas.
I.e., the size of B is exactly 356 more than the complexity of
our formal axiomatic system.
You can easily check that 356 is correct. Because as B
loops through (fas 1), (fas 2), etc., it displays each
theorem that it finds, and if the theorem is of the form (is-elegant
E), B also displays the size of E and the size of B.
So you frequently get to see what B thinks its own size is.
After displaying these two numbers, B compares them.
If the size of E is less than or equal to the
size of B, then B keeps looping. Otherwise, B evaluates E and
returns that value as its own.
Note that the way you do a loop in LISP is by having a function (loop N) which takes care of the Nth iteration of the loop. So during the Nth go round, to continue looping you just call (loop + N 1), which starts the N+1st iteration of the loop.
Now we'll run the proof of my incompleteness theorem on each of four different formal axiomatic systems. In each case the drill is like this. First we (re)define ``expression'' to be the paradoxical Berry expression B. B contains a list of theorems given by fas of N. Then we size the expression B so that we can see if it knows its own size. Then we evaluate the expression B, i.e., we run my proof. B will loop through all the theorems, displaying them and examining those of the form (is-elegant E). And either B will eventually run out of theorems and stop, or it will find an elegant expression E larger than B, and will return the value of E.
So there are four runs to show how this works. In the first run, the expressions that are proved to be elegant are very small, much too small to matter.
In the second run, we use exponentiation to construct a large ``elegant'' expression E = 1000... that's a number that is exactly one character bigger than B. Of course, that's a lie, E's not really elegant! But B doesn't know that.
In the third run, we use exponentiation again, but this time to construct a large ``elegant'' expression E = 1000... that's exactly the same size as B. This is to show that B knows what it's doing. This time the elegant expression E is not large enough.
And in the fourth run, we have an ``elegant'' expression E = (− 1000... 1) with 600 0's. So B thinks that E's big enough, B evaluates E, and B returns 999... as B's value. (And this proves that E was not really elegant.)
So you see my proof in action four times. You actually see the machinery working!
LISP Interpreter Run
[[[[[
Show that a formal axiomatic system (fas) can only prove
that finitely many LISP expressions are elegant.
(An expression is elegant if no smaller expression has
the same value.)
More precisely, show that a fas of LISP complexity N can't
prove that a LISP expression X is elegant if X's size is
greater than N + 356.
(fas N) returns the theorem proved by the Nth proof
(Nth S-expression) in the fas, or nil if the proof is
invalid, or stop to stop everything.
]]]]]
[
This expression searches for an elegant expression
that is larger than it is and returns the value of
that expression as its own value.
]
define expression [Formal Axiomatic System #1]
let (fas n) if = n 1 '(is-elegant x)
if = n 2 nil
if = n 3 '(is-elegant yyy)
[else] stop
let (loop n)
let theorem [be] display (fas n)
if = nil theorem [then] (loop + n 1)
if = stop theorem [then] fas-has-stopped
if = is-elegant car theorem
if > display size cadr theorem
display + 356 size fas
[return] eval cadr theorem
[else] (loop + n 1)
[else] (loop + n 1)
(loop 1)
define expression
value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) ('
(lambda (n) ((' (lambda (theorem) (if (= nil theo
rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s
topped (if (= is-elegant (car theorem)) (if (> (di
splay (size (car (cdr theorem)))) (display (+ 356
(size fas)))) (eval (car (cdr theorem))) (loop (+
n 1))) (loop (+ n 1))))))) (display (fas n))))))))
(' (lambda (n) (if (= n 1) (' (is-elegant x)) (if
(= n 2) nil (if (= n 3) (' (is-elegant yyy)) stop
))))))
[Show that this expression knows its own size.]
size expression
expression (size expression)
value 456
[
Run #1.
Here it doesn't find an elegant expression
larger than it is:
]
eval expression
expression (eval expression)
display (is-elegant x)
display 1
display 456
display ()
display (is-elegant yyy)
display 3
display 456
display stop
value fas-has-stopped
define expression [Formal Axiomatic System #2]
let (fas n) if = n 1 '(is-elegant x)
if = n 2 nil
if = n 3 '(is-elegant yyy)
if = n 4 cons is-elegant
cons ^ 10 509 [<=====]
nil
[else] stop
let (loop n)
let theorem [be] display (fas n)
if = nil theorem [then] (loop + n 1)
if = stop theorem [then] fas-has-stopped
if = is-elegant car theorem
if > display size cadr theorem
display + 356 size fas
[return] eval cadr theorem
[else] (loop + n 1)
[else] (loop + n 1)
(loop 1)
define expression
value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) ('
(lambda (n) ((' (lambda (theorem) (if (= nil theo
rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s
topped (if (= is-elegant (car theorem)) (if (> (di
splay (size (car (cdr theorem)))) (display (+ 356
(size fas)))) (eval (car (cdr theorem))) (loop (+
n 1))) (loop (+ n 1))))))) (display (fas n))))))))
(' (lambda (n) (if (= n 1) (' (is-elegant x)) (if
(= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if
(= n 4) (cons is-elegant (cons (^ 10 509) nil)) st
op)))))))
[Show that this expression knows its own size.]
size expression
expression (size expression)
value 509
[
Run #2.
Here it finds an elegant expression
exactly one character larger than it is:
]
eval expression
expression (eval expression)
display (is-elegant x)
display 1
display 509
display ()
display (is-elegant yyy)
display 3
display 509
display (is-elegant 10000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
0000000000000000000000)
display 510
display 509
value 10000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
0000000000
define expression [Formal Axiomatic System #3]
let (fas n) if = n 1 '(is-elegant x)
if = n 2 nil
if = n 3 '(is-elegant yyy)
if = n 4 cons is-elegant
cons ^ 10 508 [<=====]
nil
[else] stop
let (loop n)
let theorem [be] display (fas n)
if = nil theorem [then] (loop + n 1)
if = stop theorem [then] fas-has-stopped
if = is-elegant car theorem
if > display size cadr theorem
display + 356 size fas
[return] eval cadr theorem
[else] (loop + n 1)
[else] (loop + n 1)
(loop 1)
define expression
value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) ('
(lambda (n) ((' (lambda (theorem) (if (= nil theo
rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s
topped (if (= is-elegant (car theorem)) (if (> (di
splay (size (car (cdr theorem)))) (display (+ 356
(size fas)))) (eval (car (cdr theorem))) (loop (+
n 1))) (loop (+ n 1))))))) (display (fas n))))))))
(' (lambda (n) (if (= n 1) (' (is-elegant x)) (if
(= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if
(= n 4) (cons is-elegant (cons (^ 10 508) nil)) st
op)))))))
[Show that this expression knows its own size.]
size expression
expression (size expression)
value 509
[
Run #3.
Here it finds an elegant expression
exactly the same size as it is:
]
eval expression
expression (eval expression)
display (is-elegant x)
display 1
display 509
display ()
display (is-elegant yyy)
display 3
display 509
display (is-elegant 10000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
000000000000000000000)
display 509
display 509
display stop
value fas-has-stopped
define expression [Formal Axiomatic System #4]
let (fas n) if = n 1 '(is-elegant x)
if = n 2 nil
if = n 3 '(is-elegant yyy)
if = n 4 cons is-elegant
cons cons "-
cons ^ 10 600 [<=====]
cons 1
nil
nil
[else] stop
let (loop n)
let theorem [be] display (fas n)
if = nil theorem [then] (loop + n 1)
if = stop theorem [then] fas-has-stopped
if = is-elegant car theorem
if > display size cadr theorem
display + 356 size fas
[return] eval cadr theorem
[else] (loop + n 1)
[else] (loop + n 1)
(loop 1)
define expression
value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) ('
(lambda (n) ((' (lambda (theorem) (if (= nil theo
rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s
topped (if (= is-elegant (car theorem)) (if (> (di
splay (size (car (cdr theorem)))) (display (+ 356
(size fas)))) (eval (car (cdr theorem))) (loop (+
n 1))) (loop (+ n 1))))))) (display (fas n))))))))
(' (lambda (n) (if (= n 1) (' (is-elegant x)) (if
(= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if
(= n 4) (cons is-elegant (cons (cons - (cons (^ 10
600) (cons 1 nil))) nil)) stop)))))))
[Show that this expression knows its own size.]
size expression
expression (size expression)
value 538
[
Run #4.
Here it finds an elegant expression
much larger than it is, and evaluates it:
]
eval expression
expression (eval expression)
display (is-elegant x)
display 1
display 538
display ()
display (is-elegant yyy)
display 3
display 538
display (is-elegant (- 10000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
0000000000000000 1))
display 607
display 538
value 99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
99999999999999999999999999999999999999999999999999
End of LISP Run
Elapsed time is 0 seconds.
Proof: Consider this S-expression
Here X* is an elegant expression for X, and Y* is an elegant expression for Y. The size of the above S-expression is H(X) + H(Y) + 19 and its value is the pair (X Y). Crucial point: in my LISP there are no side-effects! So the evaluations of X* and Y* cannot interfere with each other. Hence the values of X* and Y* in this expression are exactly the same as if they were evaluated stand-alone, i.e., separately.
Proof: (' E) has value E, therefore H(E) ≤ |E| + 4. On the other hand, consider an elegant expression E* for E. By definition, the value of E* is E and |E*| = H(E). Then (eval E*) yields the value of E, so |(eval E*)| = 7 + H(E) ≥ |E|, and therefore H(E) ≥ |E| − 7. Thus |H(E) − |E|| ≤ 7.