perm filename COMBIN.TST[AID,LSP] blob sn#679546 filedate 1982-09-24 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00010 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 (load "combin.3") C00004 00003 Bill, C00005 00004 (REDUCIBLE '(Y F) '(F (Y F))) C00006 00005 (reducible '(W (S (B W B)) F) '(S (B W B) F F)) C00007 00006 (reducible '(B W B F) C00010 00007 (REDUCIBLE '(Y1 F) '(Y F)) C00012 00008 (reduce '((W (B f))(W (B f)))) C00013 00009 (reduce '(S (S ((K S) (S (K K)I)))(S (K S)(S (K I)(K I))) A B)) C00014 00010 Ok, then what's wrong with this? It is from page 41. C00020 ENDMK C⊗; (load "combin.3") (alloc '(list 200000. 200000. ())) (*rset (nouuo ())) (load "combin.fas") (reduce '((Z 0) F X)) (reduce '((Z 3) f x)) ;(reduce '(S B (Z 8) f x))) (reduce '(D2 x y (Z 0))) (reduce '(D2 x y (Z (+ n 1)))) (reduce '(D2 x y (Z 1))) (reducible '((Z 0) F X) '(X)) (reducible '(X) '((Z 0) F X)) (reducible '(Y f) '(f (Y f))) (reducible '((Z (+ n 1))) '(S B (Z n))) (reduce '((Z (+ n 1)))) (reducible '(D2 x y (Z 0)) '(X)) (reducible '(D2 x y (Z (+ N 1))) '(Y)) (reducible '((W (B f))(W (B f))) '(W S (B W B) f)) ((W (B F)) (W (B F))) - (W (B F) (W (B F))) (B W B F (W (B F))) (B W B F (B W B F)) (B W B F ((B W B) F)) ((B W B) F ((B W B) F)) (S (B W B) (B W B) F) (W S (B W B) F) T (step apply1-reduction) (sprinter (apply1-reduction '(K I F X))) (SETQ PRINLEVEL 4 PRINGLENGTH ()) (reducible '((Z 0) F X) '(X)) (reducible '(x) '((Z 0) F X)) (X) (I X) (K I F X) ((K I) F X) ((Z 0) F X) T (reducible '((Z n)) '(S B (Z (- n 1)))) ;HUNK4 STORAGE CAPACITY EXCEEDED ;BKPT GC-LOSSAGE QUIT * Bill, I am reading Burge, and I think there is a bug in the proof that Yf=f(Yf). Burge gives: Yf = WS(BWB)f = S(BWB)ff = BWBf(BWBf) = W(Bf)(BWBf) = Bf(BWBf)(BWBf) = f(BWBf(BWBf)) = f(Yf) and I claim that going from the first to the second line is incorrect and should be: Yf = WS(BWB)f = S(BWB)(BWB)f = BWBf(BWBf) = W(Bf)(BWBf) = Bf(BWBf)(BWBf) = f(BWBf(BWBf)) = f(Yf) Does this jive with your understanding? -rpg- (REDUCIBLE '(Y F) '(F (Y F))) (Y F) (W S (B W B) F) (S (B W B) (B W B) F) (B W B F (B W B F)) (W (B F) (W (B F))) (B F (W (B F)) (W (B F))) (F (W (B F) (W (B F)))) (F (B W B F (W (B F)))) (F (B W B F (B W B F))) (F (Y F)) T (reducible '(W (S (B W B)) F) '(S (B W B) F F)) (reducible '(B W B F (B W B F)) '(S (B W B) F F)) (report) 366 nodes searched. (W (S (B W B)) F) ((S (B W B)) F F) (S (B W B) F F) 4 nodes searched. (reducible '(B W B F) '(W (B F))) (REDUCIBLE '(Y1 F) '(Y F)) (Y1 F) ((W (B F)) (W (B F))) (W (B F) (W (B F))) ((B F) (W (B F)) (W (B F))) (B F (W (B F)) (W (B F))) - (F ((W (B F)) (W (B F)))) (F (Y1 F)) T (Y1 F) ((W (B F)) (W (B F))) (W (B F) (W (B F))) ((B F) (W (B F)) (W (B F))) (B F (W (B F)) (W (B F))) (F ((W (B F)) (W (B F)))) - (F (W (B F) (W (B F)))) (F (B W B F (W (B F)))) (F (B W B F (B W B F))) (F (B W B F ((B W B) F))) (F ((B W B) F ((B W B) F))) (F (S (B W B) (B W B) F)) (F (W S (B W B) F)) (F (Y F)) T (Y1 F) ((W (B F)) (W (B F))) - (W (B F) (W (B F))) (B W B F (W (B F))) (B W B F (B W B F)) (B W B F ((B W B) F)) ((B W B) F ((B W B) F)) (S (B W B) (B W B) F) (W S (B W B) F) (Y F) T (reduce '((W (B f))(W (B f)))) (reduce '(D2 a b (Z (+ n 1)))) Reducing: (D2 A B (Z 0)) (D2 A B (Z 0)) 1 Processing: (Z 0) 1 (Z 0) = (Z 0) ((Z 0) (K B) A) ((K I) (K B) A) (K I (K B) A) (I A) (A) (D2 A B (Z 0)) = (A) (reduce '(D2 a b (Z (+ n 1)))) Reducing: (D2 A B (Z (+ N 1))) (D2 A B (Z (+ N 1))) 1 Processing: (Z (+ N 1)) 2 Processing: (+ N 1) 2 (+ N 1) = (+ N 1) 1 (Z (+ N 1)) = (Z (+ N 1)) ((Z (+ N 1)) (K B) A) (S B (Z N) (K B) A) (B (K B) ((Z N) (K B)) A) ((K B) (((Z N) (K B)) A)) 1 Processing: (K B) 1 (K B) = (K B) (K B (((Z N) (K B)) A)) (B) (D2 A B (Z (+ N 1))) = (B) T (reduce '(S (S ((K S) (S (K K)I)))(S (K S)(S (K I)(K I))) A B)) (reduce '(S (K S)(S (K I)(K I))(S (k i)(k i)) A B)) Ok, then what's wrong with this? It is from page 41. (S (K F) (S I I) x) is how I interpret the meaning of how λf.S(Kf)(SII) is supposed to be applied to x. (reduce '(S (K F) (S I I) x)) Reducing: (S (K F) (S I I) X) (S (K F) (S I I) X) ((K F) X ((S I I) X)) (K F X ((S I I) X)) (F ((S I I) X)) 1 Processing: ((S I I) X) 2 Processing: (S I I) 2 (S I I) = (S I I) 1 (S I I X) 1 (I X (I X)) 1 (X (I X)) 1 ((S I I) X) = (X (I X)) 1 Processing: (X (I X)) 2 Processing: (I X) 2 (X) 2 (I X) = (X) 1 (X X) 1 (X (I X)) = (X X) 1 Processing: (X X) 1 (X X) = (X X) (S (K F) (S I I) X) = (F (X X)) T Notice that this technology works like a champ on things like this: (reduce '(D2 a b (Z (+ n 1)))) Reducing: (D2 A B (Z (+ N 1))) (D2 A B (Z (+ N 1))) 1 Processing: (Z (+ N 1)) 2 Processing: (+ N 1) 2 (+ N 1) = (+ N 1) 1 (Z (+ N 1)) = (Z (+ N 1)) ((Z (+ N 1)) (K B) A) (S B (Z N) (K B) A) (B (K B) ((Z N) (K B)) A) ((K B) (((Z N) (K B)) A)) 1 Processing: (K B) 1 (K B) = (K B) (K B (((Z N) (K B)) A)) (B) (D2 A B (Z (+ N 1))) = (B) T and: (reduce '(D2 a b (Z 0))) Reducing: (D2 A B (Z 0)) (D2 A B (Z 0)) 1 Processing: (Z 0) 1 (Z 0) = (Z 0) ((Z 0) (K B) A) ((K I) (K B) A) (K I (K B) A) (I A) (A) (D2 A B (Z 0)) = (A) I can test reducibility to: (reducible '(D2 a b (Z (+ n 1))) '(B)) (D2 A B (Z (+ N 1))) ((Z (+ N 1)) (K B) A) (S B (Z N) (K B) A) (B (K B) ((Z N) (K B)) A) ((K B) (((Z N) (K B)) A)) (K B (((Z N) (K B)) A)) (K B ((Z N (K B)) A)) (K B (Z N (K B) A)) (B) 22 nodes searched. T So what am I doing wrong? -rpg-