[[[[[ Show that a real r is Martin-Lof random iff it is Chaitin random. An effective covering A_k of k is a function of k that enumerates bit strings s, which are the initial bits of the covered reals. We assume that no s in A_k is a proper prefix or extension of another. Thus the measure of the cover A_k of k is exactly Sum_{s in A_k} of 2^{-|s|}, where |s| is the length of the bit string s. ]]]]] [First part: not M-L random ===> not Ch random] [We create the following set of requirements] [(output, size-of-program)] [ (s, |s|-n) : s in A_{n^2}, n >= 2 ] [Stage k>=0, look at all A_{n^2} n = 2 to 2+k for time k.] [Then have to combine stage 0, stage 1,...] [and eliminate duplicates] [infinite computation that displays strings] [in cover A_m with measure mu <= 1/2^m] define (A m) cdr cons [test case, A_m = string of m 1's] display base10-to-2 - ^ 2 m 1 nil define (is-in? x l) [is x in the list l?] if atom l false if = x car l true (is-in? x cdr l) define (convert-to-requirements cover n) [display requirements] if atom cover requirements [finished?] let s car cover [get first string] let cover cdr cover [get rest of strings] let requirement cons s cons - length s n nil [form (s, |s|-n)] if (is-in? requirement requirements) [duplicate?] [yes] (convert-to-requirements cover n) [no] let requirements cons display requirement requirements (convert-to-requirements cover n) define (stage k) if = k 4 stop! [[[stop infinite computation!!!]]] let (loop i) [i = 0 to k] if > i k (stage + k 1) [go to next stage] let n + 2 i [n = 2 + i] let expr cons cons "' cons A nil cons * n n nil let cover caddr try k expr nil [caddr = displays] let requirements (convert-to-requirements cover n) (loop + i 1) [bump i] [initialize i] (loop 0) [to remove duplicates] define requirements () [run it] (stage 0)