[omega3.l]
[Show that]
[ H(Omega_n) > n - 9488.]
[Omega_n is the first n bits of Omega,]
[where we choose]
[ Omega = xxx0111111...]
[instead of]
[ Omega = xxx1000000...]
[if necessary.]
[This is an identity function with the size-effect of]
[displaying the length in bits of the binary prefix.]
define (display-length-of-prefix prefix)
cadr cons display length prefix cons prefix nil
cadr try no-time-limit 'eval read-exp [Universal Turing machine U ---]
display
[--- followed by its program.]
append [Append prefix and data.]
[Code to display size of prefix in bits.]
(display-length-of-prefix bits '
[]
[Omega2.l follows.]
[]
let (count-halt prefix time bits-left-to-extend)
if = bits-left-to-extend 0
if = success car try time 'eval read-exp prefix
1 0
+ (count-halt append prefix '(0) time - bits-left-to-extend 1)
(count-halt append prefix '(1) time - bits-left-to-extend 1)
let (omega k) cons (count-halt nil k k)
cons /
cons ^ 2 k
nil
[]
[Read and execute from remainder of tape]
[a program to compute an n-bit]
[initial piece of Omega.]
[]
let w debug eval debug read-exp
[]
[Convert Omega to ratio of integers,]
[i.e., from a bit string to a rational number.]
[]
let n length w
let w debug cons base2-to-10 w
cons /
cons ^ 2 n
nil
[]
let (loop k) [Main Loop ---]
let x debug (omega debug k) [Compute the kth lower bound on Omega.]
if debug (<=rat w x) (big nil k n) [Are the first n bits OK? If not, bump k.]
(loop + k 1) [If so, form the union of all output of n-bit]
[programs within time k, output it, and halt.]
[All n-bit programs that ever halt halt by time k.]
[Thus this union is bigger than anything of complexity]
[less than or equal to n!]
[ ]
[This total output will be bigger than each individual output,]
[and therefore must come from a program with more than n bits.]
[Therefore this program itself must be more than n bits long.]
[I.e., 9488 + H(Omega_n) > n. Q.E.D.]
[]
[Compare two rational numbers, i.e., is x= (a / b) <= y= (c / d)?]
let (<=rat x y)
let a car debug x
let b caddr x
let c car debug y
let d caddr y
<= * a d * b c
[Union of all output of n-bit programs within time k.]
let (big prefix time bits-left-to-add)
if = 0 bits-left-to-add
try time 'eval read-exp prefix
append (big append prefix '(0) time - bits-left-to-add 1)
(big append prefix '(1) time - bits-left-to-add 1)
(loop 0) [Start main loop running with k = 0.]
) [end of prefix]
bits ' [Here is the data: an optimal program to compute n bits of Omega.]
'(0 0 0 0 0 0 0 1) [n = 8! Are these really the first 8 bits of Omega?]