The Limits of Mathematics
G. J. Chaitin
IBM Research Division, P. O. Box 704, Yorktown Heights, NY 10598,
email:chaitin@watson.ibm.com
1 Introduction
In a remarkable development, I have constructed a new definition for a
selfdelimiting universal Turing machine (UTM) that is easy to
program and runs very quickly. This provides a new foundation for
algorithmic information theory (AIT), which is the theory of the size
in bits of programs for selfdelimiting UTM's. Previously, AIT had an
abstract mathematical quality. Now it is possible to write down
executable programs that embody the constructions in the proofs of
theorems. So AIT goes from dealing with remote idealized mythical
objects to being a theory about practical downtoearth gadgets that
one can actually play with and use. This new selfdelimiting UTM is implemented via software written in a
new version of LISP that I invented especially for this purpose. This
LISP was designed by writing an interpreter for it in Mathematica that
was then translated into C. I have tested this software by running it
on IBM RS/6000 workstations with the AIX version of UNIX. Using this new software and the latest theoretical ideas, it is now
possible to give a selfcontained "hands on" minicourse presenting
very concretely my latest proofs of my two fundamental
informationtheoretic incompleteness theorems. The first of these
theorems states that an Nbit formal axiomatic system cannot enable
one to exhibit any specific object with programsize complexity
greater than N + c. The second of these theorems states that an Nbit
formal axiomatic system cannot enable one to determine more than N +
scattered bits of the halting probability Most people believe that anything that is true is true for a
reason. These theorems show that some things are true for no reason at
all, i.e., accidentally, or at random. As is shown in this course, the algorithms considered in the proofs of
these two theorems are now easy to program and run, and by looking at
the size in bits of these programs one can actually, for the first
time, determine exact values for the constants c and I used this approach and software in an intensive short course on the
limits of mathematics that I gave at the University of Maine in Orono
in the summer of 1994. I also lectured on this material during a stay
at the Santa Fe Institute in the spring of 1995, and at a meeting at
the Black Sea University in Romania in the summer of 1995. A summary
of the approach that I used on these three occasions will appear under
the title "A new version of algorithmic information theory" in a
*1 C. Calude (ed.). The Finite, the Unbounded and the Infinite,
Proceedings of the Summer School "Chaitin Complexity and
Applications, Mangalia, Romania, 27 June  6 July, 1995.Page 270
forthcoming issue of the new magazine Complexity, which has just been
launched by the Santa Fe Institute and John Wiley and Sons. A less
technical discussion of the basic ideas that are involved "How to run
algorithmic information theory on a computer" will also appear in
Complexity. After presenting this material at these three different places, it
became obvious to me that it is extremely difficult to understand it
in its original form. So next time, at the Rovaniemi Institute of
Technology in the spring of 1996, I am going to use the new, more
understandable software in this report; everything has been redone in
an attempt to make it as easy to understand as possible. For their stimulating invitations, I thank Prof. George Markowsky of
the University of Maine, Prof. Cristian Calude of the University of
Auckland, Prof. John Casti of the Santa Fe Institute, and
Prof. Veikko Keränen of the Rovaniemi Institute of Technology. And I
am grateful to IBM for supporting my research for almost thirty years,
and to my current management chain at the IBM Research Division, Dan
Prener, Christos Georgiou, Eric Kronstadt, Jeff Jaffe, and Jim
McGroddy. This report includes the LISP runs *.r used to present the
informationtheoretic incompleteness theorems of algorithmic
information theory. This report does not include the software used to
produce these LISP runs. To obtain the software for this course via
email, please send requests to chaitin@watson.ibm.com.
2 The New Idea
Here is a quick summary of this new LISP, in which atoms can now
either be words or unsigned decimal integers. First of all, comments
are written like this: [comment]. Each LISP primitive function has a
fixed number of arguments. ' is QUOTE, = is EQ, and atom, car, cdr,
cadr, caddr, cons are provided with their usual meaning. We also have
lambda, define, let, if and display and eval. The notation " indicates
that an Sexpression with explicit parentheses follows, not what is
usually the case in this LISP, an Mexpression, in which the
parentheses for each primitive function are implicit. nil denotes the
empty list (), and the logical truth values are true and false. For
dealing with unsigned decimal integers we have +, , *, <, >,
<=, >=, base10to2, base2to10. So far this is fairly standard. The new idea is this. We define our
standard selfdelimiting universal Turing machine as follows. Its
program is in binary, and appears on a tape in the following
form. First comes a LISP expression, written in ASCII with 8 bits per
character, and terminated by an endofline character '\n'. The TM
reads in this LISP expression, and then evaluates it. As it does this,
two new primitive functions readbit and readexp with no arguments
may be used to read more from the TM tape. Both of these functions
explode if the tape is exhausted, killing the computation. readbit
reads a single bit from the tape. readexp reads in an entire LISP
expression, in 8bit character chunks, until it reaches an endofline
character '\n'. This is the only way that information on the TM tape may be accessed,
which forces it to be used in a selfdelimiting fashion. This is
because no algorithm can search for the end of the tape and then use
the length of the tape as data in the Page 271
computation. If an algorithm attempts to read a bit that is not on the
tape, the algorithm aborts. How is information placed on the TM tape in the first place? Well, in
the starting environment, the tape is empty and any attempt to read it
will give an error message. To place information on the tape, one must
use the primitive function try which tries to see if an expression can
be evaluated. Consider the three arguments and of try. The meaning of the
first argument is as follows. If is notimelimit, then there is no
depth limit. Otherwise must be an unsigned decimal integer, and
gives the depth limit (limit on the nesting depth of function calls
and reevaluations). The second argument of try is the expression
to be evaluated as long as the depth limit is not exceeded. And the
third argument of try is a list of bits to be used as the TM tape. The value returned by the
primitive function try is a triple. The first element of is success if the evaluation of
was completed
successfully, and the first element of is failure if this was not the
case. The second element of is outofdata if the evaluation of aborted because an attempt was
made to read a nonexistent bit from the TM tape. The second element
of is outoftime if
evaluation of aborted
because the depth limit was exceeded. These are the only possible
error flags, because this LISP is designed with maximally permissive
semantics. If the computation terminated normally instead of aborting, the
second element of will be
the result produced by the computation , i.e., its value. That's the second element of
the list produced by the
try primitive function. The third element of the value is a list of all the arguments to the
primitive function display that were encountered during the evaluation
of . More precisely, if display was called N times during the
evaluation of , then will be a list of N elements. The N arguments of
display appear in in chronological order. Thus try can not only be
used to determine if a computation reads too much tape or goes on
too long (i.e., to greater depth than ), but try can also be used to
capture all the output that displayed as it went along, whether the
computation aborted or not. In summary, all that one has to do to simulate a selfdelimiting
universal Turing machine U(p) running on the binary program p is to
write try notimelimit 'eval readexp p
This is an Mexpression with parentheses omitted from primitive
functions. (Recall that all primitive functions have a fixed number of
arguments.) With the parentheses supplied, it becomes the Sexpression (try notimelimit ('(eval(readexp))) p)
This says that one is to read a complete LISP Sexpression from the TM
tape p and then evaluate it without any time limit and using whatever
is left on the tape p. Some more primitive functions have also been added. The 2argument
function append denotes list concatenation, and the 1argument
function bits converts an Sexpression into the list of the bits in
its ASCII character string representation. These are used for
constructing the bit strings that are then put on the TM tape using
try's third argument . We also provide the 1argument Page 272
functions size and length that respectively give the number of
characters in an Sexpression, and the number of elements in a
list. Note that the functions append, size and length could be programmed rather than included as
builtin primitive functions, but it is extremely convenient and much
much faster to provide them built in. Finally a new 1argument identity function debug with the sideeffect
of outputting its argument is provided for debugging. Output produced
by debug is invisible to the "official" display and try output
mechanism. debug is needed because try suppresses all output
produced within its depthcontrolled evaluation of . Instead try
collects all output from within for inclusion in the final value
that try returns, namely = (success/failure, value of ).
3 Course Outline
The course begins by explaining with examples my new LISP. See
examples.r. Then the theory of LISP programsize complexity is developed a little
bit. LISP programsize complexity is extremely simple and concrete. In
particular, it is easy to show that it is impossible to prove that a
selfcontained LISP expression is elegant, i.e., that no smaller
expression has the same value. To prove that an Ncharacter LISP
expression is elegant requires a formal axiomatic system that itself
has at least LISP complexity N  410.
See godel.r. Next we define our standard selfdelimiting universal Turing machine
U(p) using cadr try notimelimit 'eval readexp p
as explained in the previous chapter. Next we show that
with c = 432: Here denotes the size in bits of the smallest program that
makes our standard universal Turing machine compute Thus this inequality
states that the information needed to compute the pair (x; y) is bounded by
a constant c plus the sum of the information needed to compute x and the
information needed to compute y. Consider cons eval readexp
cons eval readexp
nil
This is an Mexpression with parentheses omitted from primitive
functions. With all the parentheses supplied, it becomes the
Sexpression (cons (eval (readexp))
(cons (eval (readexp))
nil))
c = 432 is just 8 bits plus 8 times the size in characters of this
LISP Sexpression. See utm.r. Page 273
Consider a binary string x whose size is x bits. In utm.r we also show that
and
with c = 1106 and = 1024. As before, the programs for doing this
are exhibited and run. Next we turn to the selfdelimiting programsize complexity H(X) for
infinite r.e. sets X . This is defined to be the size in bits of the
smallest LISP expression that executes forever without halting and
outputs the members of the r.e. set X using the LISP primitive
display, which is an identity function with the sideeffect of
outputting the value of its argument. Note that this LISP expression is allowed to read additional bits or expressions from the TM tape
using the primitive functions readbit and readexp if so desires. But
of course is charged for this; this adds to program size. It is in order to deal with such unending expressions that the LISP
primitive function for timelimited evaluation try captures all output
from display within its second argument Now consider a formal axiomatic system A of complexity N , i.e., with
a set of theorems that considered as an r.e. set as above has
selfdelimiting programsize complexity = N . We show that A
cannot enable us to exhibit a specific Sexpression s with
selfdelimiting complexity H(s) greater than N + c. Here c =
4872. See godel2.r. Next we show two different ways to calculate the halting probability
of our standard selfdelimiting universal Turing machine in the
limit from below. See omega.r and omega2.r. The first way of doing
this, omega.r, is straight forward. The second way to calculate
, omega2.r, uses a more clever method. Using the clever method
as a subroutine, we show that if is the first N bits of the
fractional part of the basetwo real number , then
with c = 8000. Again this is done with a program that can actually be
run and whose size gives us a value for c. See omega3.r. Consider again the formal axiomatic system A with complexity N , i.e.,
with selfdelimiting programsize complexity = N . Using the
lower bound of N on established in omega3.r, we show that A cannot
enable us to determine more than the first bits of Here = 15328. In
fact, we show that A cannot enable us to determine more than N + bits
of even if they are scattered and we leave gaps. See godel3.r. Last but not least, the philosophical implications of all this should
be discussed, especially the extent to which it tends to justify
experimental mathematics. This would be along the lines of the
discussion in my talk transcript "Randomness in arithmetic and the
decline and fall of reductionism in pure mathematics." This concludes our "handson" minicourse on the informationtheoretic
limits of mathematics. Page 274
References
Here is a useful collection of handouts for this course:
[1] G. J. Chaitin, "Randomness in arithmetic and the decline and fall
of reductionism in pure mathematics," in J. Cornwell, Nature's
Imagination, Oxford University Press, 1995, pp. 2744.
[2] G. J. Chaitin, "The Berry paradox," Complexity 1 (1995),
pp. 260.
[3] G. J. Chaitin, "A new version of algorithmic information theory,"
Complexity, to appear.
[4] G. J. Chaitin, "How to run algorithmic information theory on a
computer," Complexity, to appear.
examples.r
LISP Interpreter Run
[ Test new lisp & show how it works ]
aa [ initially all atoms eval to self ]
expression aa
value aa
nil [ except nil = the empty list ]
expression nil
value ()
'aa [ quote = literally ]
expression (' aa)
value aa
'(aa bb cc) [ delimiters are ' " ( ) [ ] blank \n]
expression (' (aa bb cc))
value (aa bb cc)
(aa bb cc) [ what if quote omitted?! ]
expression (aa bb cc)
value aa
'car '(aa bb cc) [ here effect is different ]
expression (' (car (' (aa bb cc))))
value (car (' (aa bb cc)))
car '(aa bb cc) [ car = first element of list ]
expression (car (' (aa bb cc)))
value aa
Page 275
car '((a b)c d)
expression (car (' ((a b) c d)))
value (a b)
car '(aa)
expression (car (' (aa)))
value aa
car aa [ ignore error ]
expression (car aa)
value aa
cdr '(aa bb cc) [ cdr = rest of list ]
expression (cdr (' (aa bb cc)))
value (bb cc)
cdr '((a b)c d)
expression (cdr (' ((a b) c d)))
value (c d)
cdr '(aa)
expression (cdr (' (aa)))
value ()
cdr aa [ ignore error ]
expression (cdr aa)
value aa
cadr '(aa bb cc) [ combinations of car & cdr ]
expression (car (cdr (' (aa bb cc))))
value bb
caddr '(aa bb cc)
expression (car (cdr (cdr (' (aa bb cc)))))
value cc
cons 'aa '(bb cc) [ cons = inverse of car & cdr ]
expression (cons (' aa) (' (bb cc)))
value (aa bb cc)
cons'(a b)'(c d)
expression (cons (' (a b)) (' (c d)))
value ((a b) c d)
Page 276
cons aa nil
expression (cons aa nil)
value (aa)
cons aa ()
expression (cons aa ())
value (aa)
cons aa bb [ ignore error ]
expression (cons aa bb)
value aa
("cons aa) [ supply nil for missing arguments ]
expression (cons aa)
value (aa)
("cons '(aa) '(bb) '(cc)) [ ignore extra arguments ]
expression (cons (' (aa)) (' (bb)) (' (cc)))
value ((aa) bb)
atom ' aa [ isatomic? predicate ]
expression (atom (' aa))
value true
atom '(aa)
expression (atom (' (aa)))
value false
atom '( )
expression (atom (' ()))
value true
= aa bb [ areequalSexpressions? predicate ]
expression (= aa bb)
value false
= aa aa
expression (= aa aa)
value true
= '(a b)'(a b)
expression (= (' (a b)) (' (a b)))
value true
Page 277
= '(a b)'(a x)
expression (= (' (a b)) (' (a x)))
value false
if true x y [ if ... then ... else ... ]
expression (if true x y)
value x
if false x y
expression (if false x y)
value y
if xxx x y [ anything not false is true ]
expression (if xxx x y)
value x
[ display intermediate results ]
cdr display cdr display cdr display '( a b c d e )
expression (cdr (display (cdr (display (cdr (display (' (a b
c d e))))))))
display (a b c d e)
display (b c d e)
display (c d e)
value (d e)
('lambda(x y)x 1 2) [ lambda expression ]
expression ((' (lambda (x y) x)) 1 2)
value 1
('lambda(x y)y 1 2)
expression ((' (lambda (x y) y)) 1 2)
value 2
('lambda(x y)cons y cons x nil 1 2)
expression ((' (lambda (x y) (cons y (cons x nil)))) 1 2)
value (2 1)
(if true "car "cdr '(a b c)) [ function expressions ]
expression ((if true car cdr) (' (a b c)))
value a
(if false "car "cdr '(a b c))
expression ((if false car cdr) (' (a b c)))
value (b c)
Page 278
('lambda()cons x cons y nil) [ function with no arguments ]
expression ((' (lambda () (cons x (cons y nil)))))
value (x y)
[ Here is a way to create an expression and then
evaluate it in the current environment. EVAL (see
below) does this using a clean environment instead. ]
(display
cons "lambda cons nil cons display 'cons x cons y nil nil)
expression ((display (cons lambda (cons nil (cons (display ('
(cons x (cons y nil)))) nil)))))
display (cons x (cons y nil))
display (lambda () (cons x (cons y nil)))
value (x y)
[ let ... be ... in ... ]
let x a cons x cons x nil [ first case, let x be ... in ... ]
expression ((' (lambda (x) (cons x (cons x nil)))) a)
value (a a)
x
expression x
value x
[ second case, let (f x) be ... in ... ]
let (f x) if atom display x x (f car x)
(f '(((a)b)c))
expression ((' (lambda (f) (f (' (((a) b) c))))) (' (lambda (
x) (if (atom (display x)) x (f (car x))))))
display (((a) b) c)
display ((a) b)
display (a)
display a
value a
f
expression f
value f
append '(a b c) '(d e f) [ concatenatelist primitive ]
expression (append (' (a b c)) (' (d e f)))
value (a b c d e f)
[ define "by hand" temporarily ]
Page 279
let (cat x y) if atom x y cons car x (cat cdr x y)
(cat '(a b c) '(d e f))
expression ((' (lambda (cat) (cat (' (a b c)) (' (d e f)))))
(' (lambda (x y) (if (atom x) y (cons (car x) (cat
(cdr x) y))))))
value (a b c d e f)+
cat
expression cat
value cat
[ define "by hand" permanently ]
define (cat x y) if atom x y cons car x (cat cdr x y)
define cat
value (lambda (x y) (if (atom x) y (cons (car x) (cat (c
dr x) y))))
cat
expression cat
value (lambda (x y) (if (atom x) y (cons (car x) (cat (c
dr x) y))))
(cat '(a b c) '(d e f))
expression (cat (' (a b c)) (' (d e f)))
value (a b c d e f)
define x (a b c) [ define atom, not function ]
define x
value (a b c)
cons x nil
expression (cons x nil)
value ((a b c))
define x (d e f)
define x
value (d e f)
cons x nil
expression (cons x nil)
value ((d e f))
size abc [ size of Sexpression in characters ]
expression (size abc)
Page 280
value 3
size ' ( a b c )
expression (size (' (a b c)))
value 7
length ' ( a b c ) [ number of elements in list ]
expression (length (' (a b c)))
value 3
length display bits ' a [ Sexpression > bits ]
expression (length (display (bits (' a))))
display (0 1 1 0 0 0 0 1 0 0 0 0 1 0 1 0)
value 16
length display bits ' abc [ extra character is \n ]
expression (length (display (bits (' abc))))
display (0 1 1 0 0 0 0 1 0 1 1 0 0 0 1 0 0 1 1 0 0 0 1 1 0
0 0 0 1 0 1 0)
value 32
length display bits nil
expression (length (display (bits nil)))
display (0 0 1 0 1 0 0 0 0 0 1 0 1 0 0 1 0 0 0 0 1 0 1 0)
value 24
length display bits ' (a)
expression (length (display (bits (' (a)))))
display (0 0 1 0 1 0 0 0 0 1 1 0 0 0 0 1 0 0 1 0 1 0 0 1 0
0 0 0 1 0 1 0)
value 32
[ plus ]
+ abc 15 [ not number > 0 ]
expression (+ abc 15)
value 15
+ '(abc) 15
expression (+ (' (abc)) 15)
value 15
+ 10 15
expression (+ 10 15)
value 25
 10 15 [ nonnegative minus ]
Page 281
expression ( 10 15)
value 0
 15 10
expression ( 15 10)
value 5
* 10 15 [ times ]
expression (* 10 15)
value 150
[ power ]
expression
value 1000000000000000
< 10 15 [ less than ]
expression (< 10 15)
value true
< 10 10
expression (< 10 10)
value false
> 15 10 [ greater than ]
expression (> 15 10)
value true
> 10 10
expression (> 10 10)
value false
<= 15 10 [ less than or equal ]
expression ( <= 15 10)
value false
<= 10 10
expression (<= 10 10)
value true
>= 10 15 [ greater than or equal ]
expression (>= 10 15)
value false
>= 10 10
Page 282
expression (>= 10 10)
value true
= 10 15 [ equal ]
expression (= 10 15)
value false
= 10 10
expression (= 10 10)
value true
[ here not number isn't considered zero ]
= abc 0
expression (= abc 0)
value false
= 0003 3 [ other ways numbers are funny ]
expression (= 3 3)
value true
000099 [ leading zeros removed ]
expression 99
value 99
[ and numbers are constants ]
let x b cons x cons x nil
expression ((' (lambda (x) (cons x (cons x nil)))) b)
value (b b)
let 99 45 cons 99 cons 99 nil
expression ((' (lambda (99) (cons 99 (cons 99 nil)))) 45)
value (99 99)
define 99 45
define 99
value 45
cons 99 cons 99 nil
expression (cons 99 (cons 99 nil))
value (99 99)
[ decimal<>binary conversions ]
base10to2 255
Page 283
expression (base10to2 255)
value (1 1 1 1 1 1 1 1)
base10to2 256
expression (base10to2 256)
value (1 0 0 0 0 0 0 0 0)
base10to2 257
expression (base10to2 257)
value (1 0 0 0 0 0 0 0 1)
base2to10 '(1 1 1 1)
expression (base2to10 (' (1 1 1 1)))
value 15
base2to10 '(1 0 0 0 0)
expression (base2to10 (' (1 0 0 0 0)))
value 16
base2to10 '(1 0 0 0 1)
expression (base2to10 (' (1 0 0 0 1)))
value 17
[ illustrate eval & try ]
eval display '+ display 5 display 15
expression (eval (display (' (+ (display 5) (display 15)))))
display (+ (display 5) (display 15))
display 5
display 15
value 20
try 0 display '+ display 5 display 15 nil
expression (try 0 (display (' (+ (display 5) (display 15))))
nil)
display (+ (display 5) (display 15))
value (success 20 (5 15))
try 0 display '+ debug 5 debug 15 nil
expression (try 0 (display (' (+ (debug 5) (debug 15)))) nil)
display (+ (debug 5) (debug 15))
debug 5
debug 15
value (success 20 ())
[ eval & try use initial variable bindings ]
Page 284
cons x nil
expression (cons x nil)
value ((d e f))
eval 'cons x nil
expression (eval (' (cons x nil)))
value (x)
try 0 'cons x nil nil
expression (try 0 (' (cons x nil)) nil)
value (success (x) ())
define five! [ to illustrate time limits ]
let (f x) if = display x 0 1 * x (f  x 1)
(f 5)
define five!
value ((' (lambda (f) (f 5))) (' (lambda (x) (if (= (dis
play x) 0) 1 (* x (f ( x 1)))))))
eval five!
expression (eval five!)
display 5
display 4
display 3
display 2
display 1
display 0
value 120
[ by the way, numbers can be big: ]
let (f x) if = x 0 1 * x (f  x 1)
(f 100) [ one hundred factorial! ]
expression ((' (lambda (f) (f 100))) (' (lambda (x) (if (= x
0) 1 (* x (f ( x 1)))))))
value 93326215443944152681699238856266700490715968264381
62146859296389521759999322991560894146397615651828
62536979208272237582511852109168640000000000000000
00000000
[ time limit is nesting depth of reevaluations
due to function calls & eval & try ]
try 0 five! nil
expression (try 0 five! nil)
value (failure outoftime ())
try 1 five! nil
Page 285
expression (try 1 five! nil)
value (failure outoftime ())
try 2 five! nil
expression (try 2 five! nil)
value (failure outoftime (5))
try 3 five! nil
expression (try 3 five! nil)
value (failure outoftime (5 4))
try 4 five! nil
expression (try 4 five! nil)
value (failure outoftime (5 4 3))
try 5 five! nil
expression (try 5 five! nil)
value (failure outoftime (5 4 3 2))
try 6 five! nil
expression (try 6 five! nil)
value (failure outoftime (5 4 3 2 1))
try 7 five! nil
expression (try 7 five! nil)
value (success 120 (5 4 3 2 1 0))
try notimelimit five! nil
expression (try notimelimit five! nil)
value (success 120 (5 4 3 2 1 0))
define two* [ to illustrate running out of data ]
let (f x) if = 0 x nil
cons * 2 display readbit (f  x 1)
(f 5)
define two*
value ((' (lambda (f) (f 5))) (' (lambda (x) (if (= 0 x)
nil (cons (* 2 (display (readbit))) (f ( x 1)))
))))
try 6 two* '(1 0 1 0 1)
expression (try 6 two* (' (1 0 1 0 1)))
value (failure outoftime (1 0 1 0 1))
try 7 two* '(1 0 1 0 1)
Page 286
expression (try 7 two* (' (1 0 1 0 1)))
value (success (2 0 2 0 2) (1 0 1 0 1))
try 7 two* '(1 0 1)
expression (try 7 two* (' (1 0 1)))
value (failure outofdata (1 0 1))
try notimelimit two* '(1 0 1)
expression (try notimelimit two* (' (1 0 1)))
value (failure outofdata (1 0 1))
try 18
'let (f x) if = 0 x nil
cons * 2 display readbit (f  x 1)
(f 16)
bits 'a
expression (try 18 (' ((' (lambda (f) (f 16))) (' (lambda (x)
(if (= 0 x) nil (cons (* 2 (display (readbit)))
(f ( x 1)))))))) (bits (' a)))
value (success (0 2 2 0 0 0 0 2 0 0 0 0 2 0 2 0) (0 1 1
0 0 0 0 1 0 0 0 0 1 0 1 0))
[ illustrate nested try's ]
[ most constraining limit wins ]
try 20
'cons abcdef try 10
'let (f n) (f display + n 1) (f 0) [infinite loop]
nil nil
expression (try 20 (' (cons abcdef (try 10 (' ((' (lambda (f)
(f 0))) (' (lambda (n) (f (display (+ n 1)))))))
nil))) nil)
value (success (abcdef failure outoftime (1 2 3 4 5 6
7 8 9)) ())
try 10
'cons abcdef try 20
'let (f n) (f display + n 1) (f 0) [infinite loop]
nil nil
expression (try 10 (' (cons abcdef (try 20 (' ((' (lambda (f)
(f 0))) (' (lambda (n) (f (display (+ n 1)))))))
nil))) nil)
value (failure outoftime ())
try 10
'cons abcdef try 20
'let (f n) (f debug + n 1) (f 0) [infinite loop]
nil nil
expression (try 10 (' (cons abcdef (try 20 (' ((' (lambda (f)
Page 287
(f 0))) (' (lambda (n) (f (debug (+ n 1))))))) ni
l))) nil)
debug 1
debug 2
debug 3
debug 4
debug 5
debug 6
debug 7
debug 8
value (failure outoftime ())
try notimelimit
'cons abcdef try 20
'let (f n) (f display + n 1) (f 0) [infinite loop]
nil nil
expression (try notimelimit (' (cons abcdef (try 20 (' (('
(lambda (f) (f 0))) (' (lambda (n) (f (display (+
n 1))))))) nil))) nil)
value (success (abcdef failure outoftime (1 2 3 4 5 6
7 8 9 10 11 12 13 14 15 16 17 18 19)) ())
try 10
'cons abcdef try notimelimit
'let (f n) (f display + n 1) (f 0) [infinite loop]
nil nil
expression (try 10 (' (cons abcdef (try notimelimit (' (('
(lambda (f) (f 0))) (' (lambda (n) (f (display (+
n 1))))))) nil))) nil)
value (failure outoftime ())
[ illustrate readbit & readexp ]
readbit
expression (readbit)
value outofdata
readexp
expression (readexp)
value outofdata
try 0 'readbit nil
expression (try 0 (' (readbit)) nil)
value (failure outofdata ())
try 0 'readexp nil
expression (try 0 (' (readexp)) nil)
value (failure outofdata ())
Page 288
try 0 'readexp bits 'abc
expression (try 0 (' (readexp)) (bits (' abc)))
value (success abc ())
try 0 'readexp bits '(abc def)
expression (try 0 (' (readexp)) (bits (' (abc def))))
value (success (abc def) ())
try 0 'readexp bits '(abc(def ghi)jkl)
expression (try 0 (' (readexp)) (bits (' (abc (def ghi) jkl)
)))
value (success (abc (def ghi) jkl) ())
try 0 'cons readexp cons readbit nil bits 'abc
expression (try 0 (' (cons (readexp) (cons (readbit) nil)))
(bits (' abc)))
value (failure outofdata ())
try 0 'cons readexp cons readbit nil append bits 'abc '(0)
expression (try 0 (' (cons (readexp) (cons (readbit) nil)))
(append (bits (' abc)) (' (0))))
value (success (abc 0) ())
try 0 'cons readexp cons readbit nil append bits 'abc '(1)
expression (try 0 (' (cons (readexp) (cons (readbit) nil)))
(append (bits (' abc)) (' (1))))
value (success (abc 1) ())
try 0 'readexp bits '(a b c)
expression (try 0 (' (readexp)) (bits (' (a b c))))
value (success (a b c) ())
try 0 'cons readexp cons readexp nil bits '(a b c)
expression (try 0 (' (cons (readexp) (cons (readexp) nil)))
(bits (' (a b c))))
value (failure outofdata ())
try 0 'cons readexp cons readexp nil
append bits '(a b c) bits '(d e f)
expression (try 0 (' (cons (readexp) (cons (readexp) nil)))
(append (bits (' (a b c))) (bits (' (d e f)))))
value (success ((a b c) (d e f)) ())
bits 'a [ to get characters codes ]
expression (bits (' a))
Page 289
value (0 1 1 0 0 0 0 1 0 0 0 0 1 0 1 0)
try 0 'readexp '(0 1 1 0 0 0 0 1) ['a' but no \n character]
expression (try 0 (' (readexp)) (' (0 1 1 0 0 0 0 1)))
value (failure outofdata ())
try 0 'readexp '(0 1 1 0 0 0 0 1 0 0 0 0 1 0 1)[0 missing]
expression (try 0 (' (readexp)) (' (0 1 1 0 0 0 0 1 0 0 0 0
1 0 1)))
value (failure outofdata ())
try 0 'readexp '(0 1 1 0 0 0 0 1 0 0 0 0 1 0 1 0) [okay]
expression (try 0 (' (readexp)) (' (0 1 1 0 0 0 0 1 0 0 0 0
1 0 1 0)))
value (success a ())
[ if we get to \n reading 8 bits at a time,
we will always interpret as a valid Sexpression ]
try 0 'readexp
'(0 0 0 0 1 0 1 0) [nothing in record; only \n]
expression (try 0 (' (readexp)) (' (0 0 0 0 1 0 1 0)))
value (success () ())
try 0 'readexp '(1 1 1 1 1 1 1 1 [unprintable character]
0 0 0 0 1 0 1 0) [is deleted]
expression (try 0 (' (readexp)) (' (1 1 1 1 1 1 1 1 0 0 0 0
1 0 1 0)))
value (success () ())
bits () [ to get characters codes ]
expression (bits ())
value (0 0 1 0 1 0 0 0 0 0 1 0 1 0 0 1 0 0 0 0 1 0 1 0)
[ three left parentheses==>three right parentheses supplied ]
try 0 'readexp '(0 0 1 0 1 0 0 0 0 0 1 0 1 0 0 0
0 0 1 0 1 0 0 0 0 0 0 0 1 0 1 0)
expression (try 0 (' (readexp)) (' (0 0 1 0 1 0 0 0 0 0 1 0
1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 1 0 1 0)))
value (success ((())) ())
[ right parenthesis 'a'==>left parenthesis supplied ]
try 0 'readexp '(0 0 1 0 1 0 0 1 0 1 1 0 0 0 0 1
0 0 0 0 1 0 1 0) [ & extra 'a' ignored ]
expression (try 0 (' (readexp)) (' (0 0 1 0 1 0 0 1 0 1 1 0
0 0 0 1 0 0 0 0 1 0 1 0)))
value (success () ())
Page 290
[ 'a' right parenthesis==>'a' is seen & parenthesis ]
try 0 'readexp '(0 1 1 0 0 0 0 1 0 0 1 0 1 0 0 1
0 0 0 0 1 0 1 0) [ is ignored ]
expression (try 0 (' (readexp)) (' (0 1 1 0 0 0 0 1 0 0 1 0
1 0 0 1 0 0 0 0 1 0 1 0)))
value (success a ())
End of LISP Run
Elapsed time is 16 seconds.
godel.r
LISP Interpreter Run
[[[
Show that a formal system of lisp complexity
H_lisp (FAS) = N cannot enable us to exhibit
an elegant Sexpression of size greater than N + 410.
An elegant lisp expression is one with the property
that no smaller Sexpression has the same value.
Setting: formal axiomatic system is neverending
lisp expression that displays elegant Sexpressions.
]]]
[Here is the key expression.]
define expression
let (examine x)
if atom x false
if < n size car x car x
(examine cdr x)
let fas 'display 430 [insert FAS here preceeded by ']
let n + 410 size fas
let t 0
let (loop)
let v try t fas nil
let s (examine caddr v)
if s eval s
if = success car v failure
let t + t 1
(loop)
(loop)
define expression
value ((' (lambda (examine) ((' (lambda (fas) ((' (lambd
a (n) ((' (lambda (t) ((' (lambda (loop) (loop)))
Page 291
(' (lambda () ((' (lambda (v) ((' (lambda (s) (if
s (eval s) (if (= success (car v)) failure ((' (la
mbda (t) (loop))) (+ t 1)))))) (examine (car (cdr
(cdr v))))))) (try t fas nil))))))) 0))) (+ 410 (s
ize fas))))) (' (display ( 430)))))) (' (lambd
a (x) (if (atom x) false (if (< n (size (car x)))
(car x) (examine (cdr x)))))))
[Size expression.]
size expression
expression (size expression)
value 430
[Run expression & show that it knows its own size
and can find something bigger than it is.]
eval expression
expression (eval expression)
value 10000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000
0000000000000000000000000000000
[Here it fails to find anything bigger than it is.]
let (examine x)
if atom x false
if < n size car x car x
(examine cdr x)
let fas 'display 429 [insert FAS here preceeded by ']
let n + 410 size fas
let t 0
let (loop)
let v try t fas nil
let s (examine caddr v)
if s eval s
if = success car v failure
let t + t 1
(loop)
(loop)
expression ((' (lambda (examine) ((' (lambda (fas) ((' (lambd
a (n) ((' (lambda (t) ((' (lambda (loop) (loop)))
(' (lambda () ((' (lambda (v) ((' (lambda (s) (if
Page 292
s (eval s) (if (= success (car v)) failure ((' (la
mbda (t) (loop))) (+ t 1)))))) (examine (car (cdr
(cdr v))))))) (try t fas nil))))))) 0))) (+ 410 (s
ize fas))))) (' (display ( 429)))))) (' (lambd
a (x) (if (atom x) false (if (! n (size (car x)))
(car x) (examine (cdr x)))))))
value failure
End of LISP Run
Elapsed time is 2 seconds.
utm.r
LISP Interpreter Run
[[[
First steps with my new construction for
a selfdelimiting universal Turing machine.
We show that
H(x,y) <= H(x) + H(y) + c
and determine c.
Consider a bit string x of length .
We also show that
H(x) <= 2x + c
and that
H(x) <= x + H(the binary string for x) + c
and determine both these c's.
]]]
[
Here is the selfdelimiting universal Turing machine!
]
define (U p) cadr try notimelimit 'eval readexp p
define U
value (lambda (p) (car (cdr (try notimelimit (' (eval
(readexp))) p))))+
(U bits 'cons x cons y cons z nil)
expression (U (bits (' (cons x (cons y (cons z nil))))))
value (x y z)
(U append bits 'cons a debug readexp
bits '(b c d)
)
expression (U (append (bits (' (cons a (debug (readexp)))))
(bits (' (b c d)))))
debug (b c d)
value (a b c d)
[
Page 293
The length of alpha in bits is the
constant c in H(x) < + 2x + c.
]
define alpha
let (loop) let x readbit
let y readbit
if = x y
cons x (loop)
nil
(loop)
define alpha
value ((' (lambda (loop) (loop))) (' (lambda () ((' (lam
bda (x) ((' (lambda (y) (if (= x y) (cons x (loop)
) nil))) (readbit)))) (readbit)))))
length bits alpha
expression (length (bits alpha))
value 1104
(U
append
bits alpha
'(0 0 1 1 0 0 1 1 0 1)
)
expression (U (append (bits alpha) (' (0 0 1 1 0 0 1 1 0 1)))
)
value (0 1 0 1)
(U
append
bits alpha
'(0 0 1 1 0 0 1 1 0 0)
)
expression (U (append (bits alpha) (' (0 0 1 1 0 0 1 1 0 0)))
)
value outofdata
[
The length of beta in bits is the
constant c in H(x,y) <= H(x) + H(y) + c.
]
define beta
cons eval readexp
cons eval readexp
nil
define beta
value (cons (eval (readexp)) (cons (eval (readexp)) ni
l))
length bits beta
Page 294
expression (length (bits beta))
value 432
(U
append
bits beta
append
bits 'cons a cons b cons c nil
bits 'cons x cons y cons z nil
)
expression (U (append (bits beta) (append (bits (' (cons a (c
ons b (cons c nil))))) (bits (' (cons x (cons y (c
ons z nil))))))))
value ((a b c) (x y z))
(U
append
bits beta
append
append bits alpha '(0 0 1 1 0 0 1 1 0 1)
append bits alpha '(1 1 0 0 1 1 0 0 1 0)
)
expression (U (append (bits beta) (append (append (bits alpha
) (' (0 0 1 1 0 0 1 1 0 1))) (append (bits alpha)
(' (1 1 0 0 1 1 0 0 1 0))))))
value ((0 1 0 1) (1 0 1 0))
[
The length of gamma in bits is the
constant c in H(x) <= x + H(x) + c
]
define gamma
let (loop k)
if = 0 k nil
cons readbit (loop  k 1)
(loop base2to10 eval readexp)
define gamma
value ((' (lambda (loop) (loop (base2to10 (eval (read
exp)))))) (' (lambda (k) (if (= 0 k) nil (cons (re
adbit) (loop ( k 1)))))))
length bits gamma
expression (length (bits gamma))
value 1024
(U
append
bits gamma
append
[Arbitrary program for U to compute number of bits]
Page 295
bits' '(1 0 0 0)
[That many bits of data]
'(0 0 0 0 0 0 0 1)
)
expression (U (append (bits gamma) (append (bits (' (' (1 0 0
0)))) (' (0 0 0 0 0 0 0 1)))))
value (0 0 0 0 0 0 0 1)
End of LISP Run
Elapsed time is 19 seconds.
godel2.r
LISP Interpreter Run
[[[
Show that a formal system of complexity N
can't prove that a specific object has
complexity > N + 4872.
Formal system is a never halting lisp expression
that output pairs (lisp object, lower bound
on its complexity). E.g., (x 4) means
that x has complexity H(x) greater than or equal to 4.
]]]
[Here is the prefix.]
define pi
let (examine pairs)
if atom pairs false
if < n cadr car pairs
car pairs
(examine cdr pairs)
let t 0
let fas nil
let (loop)
let v try t 'eval readexp fas
let n + 4872 length fas
let p (examine caddr v)
if p car p
if = car v success failure
if = cadr v outofdata
let fas append fas cons readbit nil
(loop)
if = cadr v outoftime
let t + t 1
(loop)
unexpectedcondition
Page 296
(loop)
define pi
value ((' (lambda (examine) ((' (lambda (t) ((' (lambda
(fas) ((' (lambda (loop) (loop))) (' (lambda () ((
' (lambda (v) ((' (lambda (n) ((' (lambda (p) (if
p (car p) (if (= (car v) success) failure (if (= (
car (cdr v)) outofdata) ((' (lambda (fas) (loop)
)) (append fas (cons (readbit) nil))) (if (= (car
(cdr v)) outoftime) ((' (lambda (t) (loop))) (+
t 1)) unexpectedcondition)))))) (examine (car (c
dr (cdr v))))))) (+ 4872 (length fas))))) (try t (
' (eval (readexp))) fas))))))) nil))) 0))) (' (la
mbda (pairs) (if (atom pairs) false (if (! n (car
(cdr (car pairs)))) (car pairs) (examine (cdr pair
s)))))))
[Size pi.]
length bits pi
expression (length (bits pi))
value 4872
[Size pi + fas.]
length
append bits pi
bits 'display '(xyz 9999)
expression (length (append (bits pi) (bits (' (display (' (xy
z 9999)))))))
value 5072
[Here pi finds something suitable.]
cadr try notimelimit 'eval readexp
append bits pi
bits 'display '(xyz 5073)
expression (car (cdr (try notimelimit (' (eval (readexp)))
(append (bits pi) (bits (' (display (' (xyz 5073)
))))))))
value xyz
[Here pi doesn't find anything suitable.]
cadr try notimelimit 'eval readexp
append bits pi
bits 'display '(xyz 5072)
expression (car (cdr (try notimelimit (' (eval (readexp)))
(append (bits pi) (bits (' (display (' (xyz 5072)
))))))))
value failure
Page 297 End of LISP Run
Elapsed time is 153 seconds.
omega.r
LISP Interpreter Run
[[[[ Omega in the limit from below! ]]]]
define (allbitstringsofsize k)
if = 0 k '(())
(extendbyonebit (allbitstringsofsize  k 1))
define allbitstringsofsize
value (lambda (k) (if (= 0 k) (' (())) (extendbyonebi
t allbitstringsofsize ( k 1)))))
define (extendbyonebit x)
if atom x nil
cons append car x '(0)
cons append car x '(1)
(extendbyonebit cdr x)
define extendbyonebit
value (lambda (x) (if (atom x) nil (cons (append (car x)
(' (0))) (cons (append (car x) (' (1))) (extendb
yonebit (cdr x))))))
define (counthalt p)
if atom p 0
+
if = success car try t 'eval readexp car p
1 0
(counthalt cdr p)
define counthalt
value (lambda (p) (if (atom p) 0 (+ (if (= success (car
(try t(' (eval (readexp))) (car p)))) 1 0) (coun
thalt (cdr p)))))
define (omega t) cons (counthalt (allbitstringsofsize t))
cons /
cons
nil
define omega
value (lambda (t) (cons (counthalt (allbitstringsof
size t)) (cons / (cons ) nil))))
(omega 0)
expression (omega 0)
value (0 / 1)
Page 298
(omega 1)
expression (omega 1)
value (0 / 2)
(omega 2)
expression (omega 2)
value (0 / 4)
(omega 3)
expression (omega 3)
value (0 / 8)
(omega 8)
expression (omega 8)
value (1 / 256)
End of LISP Run
Elapsed time is 38 seconds.
omega2.r
LISP Interpreter Run
[[[[ Omega in the limit from below! ]]]]
define (counthalt prefix bitslefttoextend)
if = bitslefttoextend 0
if = success car try t 'eval readexp prefix
1 0
+ (counthalt append prefix '(0)  bitslefttoextend 1)
(counthalt append prefix '(1)  bitslefttoextend 1)
define counthalt
value (lambda (prefix bitslefttoextend) (if (= bitsl
efttoextend 0) (if (= success (car (try t (' (ev
al (readexp))) prefix))) 1 0) (+ (counthalt (app
end prefix (' (0))) ( bitslefttoextend 1)) (co
unthalt (append prefix (' (1))) ( bitslefttoe
xtend 1)))))
define (omega t) cons (counthalt nil t)
cons /
cons
nil
define omega
value (lambda (t) (cons (counthalt nil t) (cons / (cons
() nil))))
Page 299
(omega 0)
expression (omega 0)
value (0 / 1)
(omega 1)
expression (omega 1)
value (0 / 2)
(omega 2)
expression (omega 2)
value (0 / 4)
(omega 3)
expression (omega 3)
value (0 / 8)
(omega 8)
expression (omega 8)
value (1 / 256)
End of LISP Run
Elapsed time is 33 seconds.
omega3.r
LISP Interpreter Run
[[[
Show that
H(Omega_n) > n  8000.
Omega_n is the first n bits of Omega,
where we choose
Omega = xxx0111111...
instead of
Omega = xxx1000000...
if necessary.
]]]
[Here is the prefix.]
define pi
let (counthalt prefix bitslefttoextend)
if = bitslefttoextend 0
if = success car try t 'eval readexp prefix
1 0
+ (counthalt append prefix '(0)  bitslefttoextend 1)
Page 300
(counthalt append prefix '(1)  bitslefttoextend 1)
let (omega t) cons (counthalt nil t)
cons /
cons
nil
let w eval readexp
let n length w
let w cons base2to10 w
cons /
cons
nil
let (loop t)
if (<=rat w (omega t))
(big nil n)
(loop + t 1)
let (<=rat x y)
<= * car x caddr y * caddr x car y
let (big prefix bitslefttoadd)
if = 0 bitslefttoadd
cons cadr try t 'eval readexp prefix
nil
append (big append prefix '(0)  bitslefttoadd 1)
(big append prefix '(1)  bitslefttoadd 1)
(loop 0)
define pi
value ((' (lambda (counthalt) ((' (lambda (omega) ((' (
lambda (w) ((' (lambda (n) ((' (lambda (w) ((' (la
mbda (loop) ((' (lambda (<=rat) ((' (lambda (big)
(loop 0))) (' (lambda (prefix bitslefttoadd) (i
f (= 0 bitslefttoadd) (cons (car (cdr (try t ('
(eval (readexp))) prefix))) nil) (append (big (a
ppend prefix (' (0))) ( bitslefttoadd 1)) (big
(append prefix (' (1))) ( bitslefttoadd 1))))
))))) (' (lambda (x y) (!= (* (car x) (car (cdr (c
dr y)))) (* (car (cdr (cdr x))) (car y)))))))) ('
(lambda (t) (if (<=rat w (omega t)) (big nil n) (l
oop (+ t 1)))))))) (cons (base2to10 w) (cons / (
cons ( ) nil)))))) (length w)))) (eval (reade
xp))))) (' (lambda (t) (cons (counthalt nil t) (c
ons / (cons ( ) nil)))))))) (' (lambda (prefix
bitslefttoextend) (if (= bitslefttoextend 0
) (if (= success (car (try t (' (eval (readexp)))
prefix))) 1 0) (+ (counthalt (append prefix (' (
0))) ( bitslefttoextend 1)) (counthalt (appen
d prefix (' (1))) ( bitslefttoextend 1)))))))
Page 301
[Run pi.]
cadr try notimelimit 'eval readexp
append bits pi
bits '
[Program to compute first n = 8 bits of Omega]
'(0 0 0 0 0 0 0 1)
expression (car (cdr (try notimelimit (' (eval (readexp)))
(append (bits pi) (bits (' (' (0 0 0 0 0 0 0 1)))
)))))
value (outofdata outofdata outofdata outofdata o
utofdata outofdata outofdata outofdata out
ofdata outofdata () outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
Page 302
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata outofdata outofdata outofdata
outofdata outofdata outofdata outofdata ou
tofdata outofdata outofdata outofdata out
ofdata outofdata outofdata outofdata outof
data outofdata outofdata outofdata outofd
ata outofdata outofdata outofdata outofdat
a outofdata)
[Size pi.]
length bits pi
expression (length (bits pi))
value 8000
End of LISP Run
Elapsed time is 148 seconds.
godel3.r
LISP Interpreter Run
[[[
Show that a formal system of complexity N
can't determine more than N + 8000 + 7328
= N + 15328 bits of Omega.
Formal system is a never halting lisp expression
that outputs lists of the form (1 0 X 0 X X X X 1 0).
This stands for the fractional part of Omega,
and means that these 0,1 bits of Omega are known.
X stands for an unknown bit.
]]]
[Here is the prefix.]
define pi
let (numberofbitsdetermined w)
if atom w 0
+ (numberofbitsdetermined cdr w)
if = X car w
0
1
Page 303
let (supplymissingbits w)
if atom w nil
cons if = X car w
readbit
car w
(supplymissingbits cdr w)
let (examine w)
if atom w false
[if < n (numberofbitsdetermined car w)]
[ Change n to 1 here so will succeed. ]
if < 1 (numberofbitsdetermined car w)
car w
(examine cdr w)
let t 0
let fas nil
let (loop)
let v try t 'eval readexp fas
let n + 8000 + 7328 length fas
let w (examine caddr v)
if w (supplymissingbits w)
if = car v success failure
if = cadr v outofdata
let fas append fas cons readbit nil
(loop)
if = cadr v outoftime
let t + t 1
(loop)
unexpectedcondition
(loop)
define pi
value ((' (lambda (numberofbitsdetermined) ((' (lambd
a (supplymissingbits) ((' (lambda (examine) (('
(lambda (t) ((' (lambda (fas) ((' (lambda (loop) (
loop))) (' (lambda () ((' (lambda (v) ((' (lambda
(n) ((' (lambda (w) (if w (supplymissingbits w)
(if (= (car v) success) failure (if (= (car (cdr v
)) outofdata) ((' (lambda (fas) (loop))) (append
fas (cons (readbit) nil))) (if (= (car (cdr v))
outoftime) ((' (lambda (t) (loop))) (+ t 1)) une
xpectedcondition)))))) (examine (car (cdr (cdr v)
)))))) (+ 8000 (+ 7328 (length fas)))))) (try t ('
(eval (readexp))) fas))))))) nil))) 0))) (' (lam
bda (w) (if (atom w) false (if (! 1 (numberofbit
sdetermined (car w))) (car w) (examine (cdr w))))
))))) (' (lambda (w) (if (atom w) nil (cons (if (=
X (car w)) (readbit) (car w)) (supplymissingbi
ts (cdr w))))))))) (' (lambda (w) (if (atom w) 0 (
+ (numberofbitsdetermined (cdr w)) (if (= X (ca
r w)) 0 1))))))
Page 304
[Size pi.]
length bits pi
expression (length (bits pi))
value 7328
[Run pi.]
cadr try notimelimit 'eval readexp
append bits pi
append [Toy formal system with only one theorem.]
bits 'display '(1 X 0)
[Missing bit of omega that is needed.]
'(1)
expression (car (cdr (try notimelimit (' (eval (readexp)))
(append (bits pi) (append (bits (' (display (' (1
X 0))))) (' (1)))))))
value (1 1 0)
End of LISP Run
Elapsed time is 94 seconds.
