LISP Interpreter Run
 
[godel.l]
 
[Show that a formal system of lisp complexity H_lisp (FAS) = N]
[cannot enable us to exhibit an elegant S-expression of]
[size greater than N + 419.]
[An elegant lisp expression is one with the property that no]
[smaller S-expression has the same value.]
[Setting: formal axiomatic system is never-ending lisp expression]
[that displays elegant S-expressions.]
 
[Idea is to have a program P search for something X that can be proved]
[to be more complex than P is, and therefore P can never find X.]
[I.e., idea is to show that if this program halts we get a contradiction,]
[and therefore the program doesn't halt.]
 
define (size-it-and-run-it exp)
    cadr cons display size display exp
         cons eval exp
              nil
 
define      size-it-and-run-it
value       (lambda (exp) (car (cdr (cons (display (size (disp
            lay exp))) (cons (eval exp) nil)))))
 
 
(size-it-and-run-it'
+ 5 15
)
 
expression  (size-it-and-run-it (' (+ 5 15)))
display     (+ 5 15)
display     8
value       20
 
 
(size-it-and-run-it'
 
[Examine list x for element that is more than n characters in size.]
[If not found returns false.]
let (examine x n)
    if atom x  false
[]
[   if < n size car x  car x     <=== Change This So Something Interesting Will Happen!]
[]
    if < 1 size car x  car x
    (examine cdr x n)
 
[Here we are given the formal axiomatic system FAS.]
let fas 'display elegant-expression   [Insert FAS here preceeded by "'".]
 
[N = the number of characters in this program including the FAS.]
let n display + 419 size display fas  [N = 419 + |FAS|.]
 
[Loop running the formal axiomatic system.]
let (loop t)                          []
  let v display try display t fas nil [Run the formal system for T time steps.]
  let s (examine caddr v n)           [Did it output an elegant s-exp larger than this program?]
  if s eval s                         [If found elegant s-exp bigger than this program,]
                                      [run it so that its output is our output. Contradiction!]
  if = failure car v (loop + t 1)     [If not, keep looping,]
  failure                             [or halt if formal system halted.]
                                      []
(loop 0)                              [Start loop running with T = 0.]
                                      []
) [end size-it-and-run-it]
 
expression  (size-it-and-run-it (' ((' (lambda (examine) ((' (
            lambda (fas) ((' (lambda (n) ((' (lambda (loop) (l
            oop 0))) (' (lambda (t) ((' (lambda (v) ((' (lambd
            a (s) (if s (eval s) (if (= failure (car v)) (loop
             (+ t 1)) failure)))) (examine (car (cdr (cdr v)))
             n)))) (display (try (display t) fas nil)))))))) (
            display (+ 419 (size (display fas))))))) (' (displ
            ay elegant-expression))))) (' (lambda (x n) (if (a
            tom x) false (if (< 1 (size (car x))) (car x) (exa
            mine (cdr x) n))))))))
display     ((' (lambda (examine) ((' (lambda (fas) ((' (lambd
            a (n) ((' (lambda (loop) (loop 0))) (' (lambda (t)
             ((' (lambda (v) ((' (lambda (s) (if s (eval s) (i
            f (= failure (car v)) (loop (+ t 1)) failure)))) (
            examine (car (cdr (cdr v))) n)))) (display (try (d
            isplay t) fas nil)))))))) (display (+ 419 (size (d
            isplay fas))))))) (' (display elegant-expression))
            ))) (' (lambda (x n) (if (atom x) false (if (< 1 (
            size (car x))) (car x) (examine (cdr x) n))))))
display     447
display     (display elegant-expression)
display     447
display     0
display     (success elegant-expression (elegant-expression))
value       elegant-expression
 
End of LISP Run
 
Elapsed time is 0 seconds.