[[[[[ Show that a real r is Solovay random iff it is strong 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 Sol random ===> not Ch random] [We create the following set of requirements] [(output, size-of-program)] [ (s, |s|) : s in A_n, n >= N, Sum_{n >= N} mu A_n <= 1] [Stage k>=0, look at all A_n, n = N to N+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 total measure Sum_m of mu A_m < infinity] define (A m) cdr cons [test case, A_m = string of m 1's] display base10-to-2 - ^ 2 m 1 nil define A value (lambda (m) (cdr (cons (display (base10-to-2 (- (^ 2 m) 1))) nil))) [in the proof we pick N so that] [the total measure Sum_{m >= N} of mu A_m <= 1] [for example,] define N 5 define N value 5 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 is-in? value (lambda (x l) (if (atom l) false (if (= x (car l)) true (is-in? x (cdr l))))) define (convert-to-requirements cover) [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 nil [form (s, |s|)] if (is-in? requirement requirements) [duplicate?] [yes] (convert-to-requirements cover) [no] let requirements cons display requirement requirements (convert-to-requirements cover) define convert-to-requirements value (lambda (cover) (if (atom cover) requirements ((' (lambda (s) ((' (lambda (cover) ((' (lambda (requi rement) (if (is-in? requirement requirements) (con vert-to-requirements cover) ((' (lambda (requireme nts) (convert-to-requirements cover))) (cons (disp lay requirement) requirements))))) (cons s (cons ( length s) nil))))) (cdr cover)))) (car cover)))) define (stage k) if = k 5 stop! [[[stop infinite computation!!!]]] let (loop i) [i = 0 to k] if > i k (stage + k 1) [go to next stage] let expr cons cons "' cons A nil cons + N i nil let cover caddr try k expr nil let requirements (convert-to-requirements cover) (loop + i 1) [bump i] [initialize i] (loop 0) define stage value (lambda (k) (if (= k 5) stop! ((' (lambda (loop) ( loop 0))) (' (lambda (i) (if (> i k) (stage (+ k 1 )) ((' (lambda (expr) ((' (lambda (cover) ((' (lam bda (requirements) (loop (+ i 1)))) (convert-to-re quirements cover)))) (car (cdr (cdr (try k expr ni l))))))) (cons (cons ' (cons A nil)) (cons (+ N i) nil))))))))) [to remove duplicates] define requirements () define requirements value () [run it] (stage 0) expression (stage 0) display ((1 1 1 1 1) 5) display ((1 1 1 1 1 1) 6) display ((1 1 1 1 1 1 1) 7) display ((1 1 1 1 1 1 1 1) 8) display ((1 1 1 1 1 1 1 1 1) 9) value stop!