; In last post, I wrote the program that generates random lambda ; expressions, 500 of these. This is the program that generates ; roughly 3500000 random lambda expressions, then attempts to ; reduce these, and makes list of lambda-expressions such that ; reduction to normal form failed. There are two different kinds of ; lambda-expressions on that list: ; ; (i) the program proves that reductions fail to terminate, i.e. ; lambda-expression is reduced to the form that is further ; reduced to itself. ; ; (ii) the program doesn't prove that reductions fail to terminate ; generally, but it shows that after n (in our case 25) ; reductions the lambda expression is still not in normal ; form. ; ; The lambda expressions on the list are normalized, i.e. two lambda ; expressions are considered to be equivalent if there is ; alpha-conversion that transform one expression in the other. ; For example, there is alpha-conversion from (^ x . x) to (^ y . y). ; ; The results are at the bottom of the post. If you decide to try ; the program, be patient, it might need one hour of time. If ; you want it to run faster, change the constant in line ; ; (dotimes(dummy 200000) ... (setf [println.supressed] true [print.supressed] true) (load "http://www.instprog.com/Instprog.default-library.lsp") (setf [println.supressed] nil [print.supressed] nil) ;--------------------------------------------------------------- ; is-variable, is-function and is-application are predicated ; that return true or false (set 'is-variable (lambda(x)(symbol? x))) (set 'is-function (lambda(L)(and (list? L) (= (first L) '^) (= (nth 2 L) '.)))) (set 'is-application (lambda(L)(and (list? L) (= (length L) 2)))) ;--------------------------------------------------------------- ; function-variable and function-body return parts of the ; lambda-expression. For example ; ; (function-variable '(^ x . (x x))) returns x ; (function-body '(^ x . (x x))) returns (x x) (set 'function-variable (lambda(f)(nth 1 f))) (set 'function-body (lambda(f)(last f))) ;--------------------------------------------------------------- ; ; (substitute-free-occurences V E F) ; ; Substitutes free occurences of variable V in expression E with F. ; Don't change bounded occurences of the variable. (set 'substitute-free-occurences ; of variable V in E with F (lambda(V E F) (cond ((is-variable E) (if (= E V) F E)) ((is-function E) (if (= (function-variable E) V) E ; V is bounded in E - no substitution (list '^ (function-variable E) '. (substitute-free-occurences V (function-body E) F)))) ((is-application E) (list (substitute-free-occurences V (first E) F) (substitute-free-occurences V (last E) F)))))) ;--------------------------------------------------------------- ; ; (reduce-once E) ; ; performs beta-reduction on lambda-expression E. It returns pair ; ; (success result) ; where ; ; success = true or nil, dependently if E is reduced ; result = reduced E if reduction is possible ; original E if reduction is not possible (set 'reduce-once (lambda(E) (cond ((is-variable E) (list 'nil E)) ((is-function E) (let((rfb (reduce-once (function-body E)))) (if (first rfb) ; success (list 'true (append (chop E) (list (last rfb)))) (list 'nil E)))) ((is-application E) (let ((F (first E)) (G (last E))) (if (is-function F) ;E=((^V._) G) ==> E10[V:=E2] (list 'true (substitute-free-occurences (function-variable F) (function-body F) G)) ;E=(F G) ==> (let ((rF (reduce-once F))) (cond ((= (first rF) true) (list 'true (list (last rF) G))) ((= (first rF) nil) (let ((rG (reduce-once G))) (cond ((= (first rG) true) (list 'true (list F (last rG)))) ((= (first rG) nil) (list 'nil (list F G)))))))))))))) ; (println= (reduce-once 'a)) ; (println= (reduce-once '(a b))) ; (println= (reduce-once '(^ x . x))) ; (println= (reduce-once '((^ x . x) y))) ; (println= (reduce-once '((^ x . y) y))) ; (set 'pretty-form (lambda(t) (replace " . " (replace "^ " (replace ") (" (string t) ")(") "^") "."))) ;--------------------------------------------------------------- ; (bounded-var i) ; ; returns i-th of variables A0, B0, C0, ... A1, B1, C1 ... (set 'bounded-var (lambda(i)(sym (append (char (+ 64 (% i 25))) (string (/ i 25)))))) ;--------------------------------------------------------------- ; alpha-convert converts expressions, so beta-reduction can be ; performed on the way it is defined. (set 'init-and-alpha-convert (lambda(E) (setf bounded-vars-counter 0) (alpha-convert E))) (set 'alpha-convert (lambda(E) (cond ((is-variable E) E) ((is-function E) (begin (inc bounded-vars-counter) (let (new-E-1 (bounded-var bounded-vars-counter)) (list '^ new-E-1 '. (expand (alpha-convert (E 3)) (list (list (E 1) new-E-1))))))) ((is-application E) (list (alpha-convert (E 0)) (alpha-convert (E 1))))))) ;--------------------------------------------------------------- ; ; (reduce new-expression reduce-max to-print) ; ; reduces new-expression in at most reduce-max steps, producing ; output if to-print is set to true. ; ; It returs list ; ; (terminating result result-counter) ; ; where ; ; terminating = true if further reductions are impossible ; = nil if cyclical reduction is discovered ; = undefined if reduction is quited because of ; lack of computing resources ; ; result = last lambda-expression in process ; result-counter = numbers of derived lambda-expression ; before further derivation is canceled ; independently of a reason (set 'reduce (lambda(new-expr reduce-max to-print) (when to-print (println "\n--------------\n\n " (pretty-form new-expr))) (let ((reduce-counter 0) (terminating 'undefined) (result 'undefined) (reduce-end nil)) (setf new-expr (init-and-alpha-convert new-expr)) (when to-print (println " ==[alpha]==> " (pretty-form new-expr))) (until reduce-end ;(println "unless loop") (letn ((old-expr new-expr) (r (reduce-once old-expr)) (reduce-once-succeeded (first r))) (cond ((not reduce-once-succeeded) (begin (setf reduce-end true) (setf terminating true) (setf result old-expr) (when to-print (println "\n There are no further reductions")))) (reduce-once-succeeded (begin (inc reduce-counter) (setf new-expr (last r)) (when to-print (println " ==[beta " reduce-counter ".]==> " (pretty-form new-expr))) (setf new-expr (init-and-alpha-convert new-expr)) (when to-print (println " ==[alpha]==> " (pretty-form new-expr))) (cond ((= old-expr new-expr) (begin (setf reduce-end true) (setf terminating nil) (setf result old-expr) (when to-print (println "\n Self-evaluating expression.")))) ((>= reduce-counter reduce-max) (begin (setf reduce-end true) (setf terminating 'undefined) (setf result new-expr) (when to-print (println "\n Maximal number of the reductions reached.")))))))))) ;(println= "unless loop ended." old-expr new-expr reduce-end) (list terminating result reduce-counter)))) ;--------------------------------------------------------------- ; ; EXAMPLE OF REDUCTION (reduce '((^ c . (c c)) (^ c . (c (c (^ c . c))))) 15 true) ; -------------- ; ; ((^A0.(A0 A0))(^B0.(B0 (B0 (^C0.C0))))) ; ==[alpha]==> ((^A0.(A0 A0))(^B0.(B0 (B0 (^C0.C0))))) ; ==[beta 1.]==> ((^B0.(B0 (B0 (^C0.C0))))(^B0.(B0 (B0 (^C0.C0))))) ; ==[alpha]==> ((^A0.(A0 (A0 (^A0.A0))))(^C0.(C0 (C0 (^D0.D0))))) ; ==[beta 2.]==> ((^C0.(C0 (C0 (^D0.D0))))((^C0.(C0 (C0 (^D0.D0))))(^A0.A0))) ; ==[alpha]==> ((^A0.(A0 (A0 (^B0.B0))))((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))) ; ==[beta 3.]==> (((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))(((^C0.(C0 (C0 (^D0.D0))))(^E0.E0))(^B0.B0))) ; ==[alpha]==> (((^A0.(A0 (A0 (^B0.B0))))(^C0.C0))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ; ==[beta 4.]==> (((^C0.C0)((^C0.C0)(^B0.B0)))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ; ==[alpha]==> (((^A0.A0)((^B0.B0)(^C0.C0)))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ; ==[beta 5.]==> (((^B0.B0)(^C0.C0))(((^D0.(D0 (D0 (^E0.E0))))(^F0.F0))(^G0.G0))) ; ==[alpha]==> (((^A0.A0)(^B0.B0))(((^C0.(C0 (C0 (^C0.C0))))(^E0.E0))(^F0.F0))) ; ==[beta 6.]==> ((^B0.B0)(((^C0.(C0 (C0 (^C0.C0))))(^E0.E0))(^F0.F0))) ; ==[alpha]==> ((^A0.A0)(((^B0.(B0 (B0 (^B0.B0))))(^D0.D0))(^E0.E0))) ; ==[beta 7.]==> (((^B0.(B0 (B0 (^B0.B0))))(^D0.D0))(^E0.E0)) ; ==[alpha]==> (((^A0.(A0 (A0 (^A0.A0))))(^C0.C0))(^D0.D0)) ; ==[beta 8.]==> (((^C0.C0)((^C0.C0)(^A0.A0)))(^D0.D0)) ; ==[alpha]==> (((^A0.A0)((^B0.B0)(^C0.C0)))(^D0.D0)) ; ==[beta 9.]==> (((^B0.B0)(^C0.C0))(^D0.D0)) ; ==[alpha]==> (((^A0.A0)(^B0.B0))(^C0.C0)) ; ==[beta 10.]==> ((^B0.B0)(^C0.C0)) ; ==[alpha]==> ((^A0.A0)(^B0.B0)) ; ==[beta 11.]==> (^B0.B0) ; ==[alpha]==> (^A0.A0) ; ; There are no further reductions ; ;--------------------------------------------------------------- ; ; (random-var nvars) ; ; return random of the first nvars variables of ; a0, b0, c0, ..., a1, b1, c1 ... ; (set 'random-var (lambda(nvars) (let((r (rand nvars))) (sym (append (char (+ 97 (% r 25))) (string (/ r 25))))))) ;--------------------------------------------------------------- ; ; (random-^-expr nvars number-of-occurences) ; ; returns random lambda-expression with at most nvars variables ; in total of exactly number-of-occurences occurences (set 'random-^-expr (lambda(nvars number-of-occurences) (cond ((= number-of-occurences 1) (random-var nvars)) ((> number-of-occurences 1) (amb (let ((r (+ (rand (- number-of-occurences 1)) 1))) (list (random-^-expr nvars r) (random-^-expr nvars (- number-of-occurences r)))) (list '^ (random-var nvars) '. (random-^-expr nvars (- number-of-occurences 1)))))))) ;--------------------------------------------------------------- ; ; (normalized E) ; ; returns normalized expression E, i.e. variables sorted by some ; natural and unique order. It is important only for order of ; free variables. The order of bounded variables is sorted on ; natural and unique way using function init-and-alpha-convert. (set 'normalized (lambda(E) (let((varcounter 0) (F (flat E))) (dolist(i F) (when (and (!= i '^) (!= i '.) (= (string i) (lower-case (string i)))) (inc varcounter) (setf E (expand E ;((i _i)) (list (list i (sym (append "_" (lower-case (string (bounded-var varcounter))))))))))) (eval-string (append "'" (replace "_" (string E) "")))))) ; (println= (normalized '(b0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0)))) ;--------------------------------------------------------------- ; The program will generate large number of lambda-expressions, ; and attempt to reduce these. The lambda-expressions not reduced in ; 20 steps or more are good candidates for unreducible lambda-expressions. (for(number-of-occurences 6 8 1) (setf successes 0 failures 0 attempts 0 total-number-of-steps 0 max-number-of-steps-if-reduction-succeeded 0) (setf max-number-of-reductions 25) (setf unreduced '()) (println= "\n\n----------------" number-of-occurences) (for(nvars 1 (- number-of-occurences 1) 1) (dotimes(dummy 200000) (letn((F (random-^-expr nvars number-of-occurences)) (G (init-and-alpha-convert F))) (inc attempts) (letn((H (reduce G max-number-of-reductions nil))) (cond ((= (H 0) true) ; reduction succeeded (inc total-number-of-steps (H 2)) (inc successes) (when (> (H 2) max-number-of-steps-if-reduction-succeeded) (setf max-number-of-steps-if-reduction-succeeded (H 2)) (setf longest-reduction G))) ((= (H 0) nil) ; reduction failed (begin (inc failures) ;(print "!") (if (= (% failures 80) 0) (println)) (push (append (string (normalized G)) " failed.") unreduced -1))) ((= (H 0) 'undefined) ; reduction canceled (begin (inc failures) ;(print "?") (if (= (% failures 80) 0) (println)) (push (append (string (normalized G)) " didn't succeeded in " (string max-number-of-reductions) " steps.") unreduced -1)))))))) (println= "\n\n" attempts "\n" successes "\n" failures "\n" max-number-of-reductions "\n" total-number-of-steps "\n" max-number-of-steps-if-reduction-succeeded "\n" longest-reduction) (println "\nUnreduced (without duplicates):\n") (dolist(s (unique (sort unreduced))) (println (+ $idx 1) ". " s))) (exit) Output: (!'s and ?'s are printed during execution of the program) ----------------number-of-occurences=6; attempts=1000000; successes=998677; failures=1323; max-number-of-reductions=25; total-number-of-steps=596444; max-number-of-steps-if-reduction-succeeded=3; longest-reduction=(((^ A0 . (A0 A0)) (^ B0 . B0)) a0); Unreduced (without duplicates): 1. ((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) failed. ----------------number-of-occurences=7; attempts=1200000; successes=1197916; failures=2084; max-number-of-reductions=25; total-number-of-steps=908464; max-number-of-steps-if-reduction-succeeded=5; longest-reduction=((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 b0)))); Unreduced (without duplicates): 1. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) failed. 2. ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0))) failed. 3. ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0))) failed. 4. ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0))) failed. 5. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 6. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 7. ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 8. ((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 9. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0))) failed. 10. ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0))) failed. 11. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) failed. 12. (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. ----------------number-of-occurences=8; attempts=1400000; successes=1396693; failures=3307; max-number-of-reductions=25; total-number-of-steps=1278600; max-number-of-steps-if-reduction-succeeded=15; longest-reduction=((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 (B0 c0))))); Unreduced (without duplicates): 1. ((((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) a0) failed. 2. ((((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0) b0) failed. 3. (((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0))) a0) failed. 4. (((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0))) b0) failed. 5. (((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0))) a0) failed. 6. (((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0))) a0) didn't succeeded in 25 steps. 7. (((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) a0))) a0) didn't succeeded in 25 steps. 8. (((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0)))) a0) didn't succeeded in 25 steps. 9. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (^ C0 . C0)) failed. 10. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (^ C0 . a0)) failed. 11. (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) (a0 a0)) failed. 12. (((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 B0)))) b0) didn't succeeded in 25 steps. 13. (((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0))) a0) failed. 14. (((^ A0 . (^ B0 . (B0 B0))) a0) (^ C0 . (C0 C0))) failed. 15. (((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0))) a0) failed. 16. (((^ A0 . A0) (^ B0 . (B0 B0))) (^ C0 . (C0 C0))) failed. 17. ((^ A0 . (((A0 A0) A0) A0)) (^ B0 . (B0 B0))) failed. 18. ((^ A0 . (((A0 A0) A0) a0)) (^ B0 . (B0 B0))) failed. 19. ((^ A0 . (((A0 A0) a0) A0)) (^ B0 . (B0 B0))) failed. 20. ((^ A0 . (((^ B0 . A0) A0) A0)) (^ C0 . (C0 C0))) failed. 21. ((^ A0 . (((^ B0 . A0) a0) A0)) (^ C0 . (C0 C0))) failed. 22. ((^ A0 . (((^ B0 . B0) A0) A0)) (^ C0 . (C0 C0))) failed. 23. ((^ A0 . ((A0 (A0 A0)) A0)) (^ B0 . (B0 B0))) failed. 24. ((^ A0 . ((A0 (A0 A0)) a0)) (^ B0 . (B0 B0))) failed. 25. ((^ A0 . ((A0 A0) (A0 A0))) (^ B0 . (B0 B0))) failed. 26. ((^ A0 . ((A0 A0) (^ B0 . A0))) (^ C0 . (C0 C0))) failed. 27. ((^ A0 . ((A0 A0) (^ B0 . B0))) (^ C0 . (C0 C0))) failed. 28. ((^ A0 . ((A0 A0) (^ B0 . a0))) (^ C0 . (C0 C0))) failed. 29. ((^ A0 . ((A0 A0) (a0 A0))) (^ B0 . (B0 B0))) failed. 30. ((^ A0 . ((A0 A0) (a0 a0))) (^ B0 . (B0 B0))) failed. 31. ((^ A0 . ((A0 A0) A0)) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 32. ((^ A0 . ((A0 A0) A0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 33. ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 34. ((^ A0 . ((A0 A0) A0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 35. ((^ A0 . ((A0 A0) a0)) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 36. ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 37. ((^ A0 . ((A0 A0) a0)) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 38. ((^ A0 . ((A0 a0) (A0 A0))) (^ B0 . (B0 B0))) failed. 39. ((^ A0 . ((^ B0 . (A0 A0)) A0)) (^ C0 . (C0 C0))) failed. 40. ((^ A0 . ((^ B0 . (A0 A0)) a0)) (^ C0 . (C0 C0))) failed. 41. ((^ A0 . ((^ B0 . (A0 B0)) A0)) (^ C0 . (C0 C0))) failed. 42. ((^ A0 . ((^ B0 . (B0 A0)) A0)) (^ C0 . (C0 C0))) failed. 43. ((^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) a0) failed. 44. ((^ A0 . ((^ B0 . (B0 B0)) A0)) (^ C0 . (C0 C0))) failed. 45. ((^ A0 . ((^ B0 . B0) (A0 A0))) (^ C0 . (C0 C0))) failed. 46. ((^ A0 . ((a0 (A0 A0)) A0)) (^ B0 . (B0 B0))) failed. 47. ((^ A0 . ((a0 (A0 A0)) a0)) (^ B0 . (B0 B0))) failed. 48. ((^ A0 . ((a0 A0) (A0 A0))) (^ B0 . (B0 B0))) failed. 49. ((^ A0 . (A0 ((A0 A0) A0))) (^ B0 . (B0 B0))) failed. 50. ((^ A0 . (A0 ((A0 A0) a0))) (^ B0 . (B0 B0))) failed. 51. ((^ A0 . (A0 ((^ B0 . A0) a0))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 52. ((^ A0 . (A0 ((^ B0 . B0) A0))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 53. ((^ A0 . (A0 (A0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 54. ((^ A0 . (A0 (A0 (^ B0 . A0)))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 55. ((^ A0 . (A0 (A0 A0))) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 56. ((^ A0 . (A0 (A0 A0))) (^ B0 . ((B0 B0) a0))) didn't succeeded in 25 steps. 57. ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 58. ((^ A0 . (A0 (A0 A0))) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 59. ((^ A0 . (A0 (^ B0 . (A0 B0)))) (^ C0 . (C0 C0))) didn't succeeded in 25 steps. 60. ((^ A0 . (A0 (^ B0 . (B0 B0)))) (^ C0 . (C0 C0))) failed. 61. ((^ A0 . (A0 (^ B0 . A0))) (^ C0 . ((C0 a0) C0))) didn't succeeded in 25 steps. 62. ((^ A0 . (A0 (a0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 63. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (B0 B0))) a0)) didn't succeeded in 25 steps. 64. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (B0 C0))) a0)) didn't succeeded in 25 steps. 65. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (C0 B0))) a0)) didn't succeeded in 25 steps. 66. ((^ A0 . (A0 A0)) ((^ B0 . (^ C0 . (C0 C0))) a0)) didn't succeeded in 25 steps. 67. ((^ A0 . (A0 A0)) ((^ B0 . B0) (^ C0 . (C0 C0)))) didn't succeeded in 25 steps. 68. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) B0) B0))) didn't succeeded in 25 steps. 69. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) B0))) didn't succeeded in 25 steps. 70. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) a0))) didn't succeeded in 25 steps. 71. ((^ A0 . (A0 A0)) (^ B0 . (((B0 B0) a0) b0))) didn't succeeded in 25 steps. 72. ((^ A0 . (A0 A0)) (^ B0 . (((^ C0 . B0) B0) B0))) didn't succeeded in 25 steps. 73. ((^ A0 . (A0 A0)) (^ B0 . (((^ C0 . C0) B0) B0))) didn't succeeded in 25 steps. 74. ((^ A0 . (A0 A0)) (^ B0 . ((B0 (B0 B0)) B0))) didn't succeeded in 25 steps. 75. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (B0 B0)))) didn't succeeded in 25 steps. 76. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (B0 a0)))) didn't succeeded in 25 steps. 77. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . B0)))) didn't succeeded in 25 steps. 78. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . C0)))) didn't succeeded in 25 steps. 79. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (^ C0 . a0)))) didn't succeeded in 25 steps. 80. ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) (a0 B0)))) didn't succeeded in 25 steps. 81. ((^ A0 . (A0 A0)) (^ B0 . ((B0 a0) (B0 B0)))) didn't succeeded in 25 steps. 82. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (B0 C0)) B0))) didn't succeeded in 25 steps. 83. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (C0 B0)) B0))) didn't succeeded in 25 steps. 84. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . (C0 C0)) B0))) didn't succeeded in 25 steps. 85. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . B0) (B0 B0)))) didn't succeeded in 25 steps. 86. ((^ A0 . (A0 A0)) (^ B0 . ((^ C0 . C0) (B0 B0)))) didn't succeeded in 25 steps. 87. ((^ A0 . (A0 A0)) (^ B0 . ((a0 a0) (B0 B0)))) didn't succeeded in 25 steps. 88. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((B0 B0) B0)))) didn't succeeded in 25 steps. 89. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((^ C0 . B0) B0)))) didn't succeeded in 25 steps. 90. ((^ A0 . (A0 A0)) (^ B0 . (B0 ((^ C0 . C0) B0)))) didn't succeeded in 25 steps. 91. ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 (B0 B0))))) didn't succeeded in 25 steps. 92. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (B0 B0))))) failed. 93. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (B0 C0))))) didn't succeeded in 25 steps. 94. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (C0 B0))))) failed. 95. ((^ A0 . (A0 A0)) (^ B0 . (B0 (^ C0 . (C0 C0))))) failed. 96. ((^ A0 . (A0 A0)) (^ B0 . (B0 (a0 (B0 B0))))) didn't succeeded in 25 steps. 97. ((^ A0 . (A0 A0)) (^ B0 . (a0 (B0 (B0 B0))))) didn't succeeded in 25 steps. 98. ((^ A0 . (A0 A0)) (^ B0 . (a0 (a0 (B0 B0))))) didn't succeeded in 25 steps. 99. ((^ A0 . (^ B0 . ((A0 A0) A0))) (^ C0 . (C0 C0))) failed. 100. ((^ A0 . (^ B0 . ((A0 A0) B0))) (^ C0 . (C0 C0))) failed. 101. ((^ A0 . (^ B0 . ((A0 A0) a0))) (^ C0 . (C0 C0))) failed. 102. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . ((C0 C0) C0))) didn't succeeded in 25 steps. 103. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . ((C0 C0) a0))) didn't succeeded in 25 steps. 104. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 (C0 C0)))) didn't succeeded in 25 steps. 105. ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (a0 (C0 C0)))) didn't succeeded in 25 steps. 106. ((^ A0 . (^ B0 . (B0 (A0 A0)))) (^ C0 . (C0 C0))) failed. 107. ((^ A0 . (^ B0 . (^ C0 . (A0 A0)))) (^ D0 . (D0 D0))) failed. 108. ((^ A0 . (^ B0 . (a0 (A0 A0)))) (^ C0 . (C0 C0))) failed. 109. ((^ A0 . (a0 ((A0 A0) a0))) (^ B0 . (B0 B0))) failed. 110. ((^ A0 . (a0 (A0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 111. ((^ A0 . (a0 (A0 A0))) (^ B0 . ((B0 B0) B0))) didn't succeeded in 25 steps. 112. ((^ A0 . (a0 (A0 A0))) (^ B0 . ((B0 B0) b0))) didn't succeeded in 25 steps. 113. ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 (B0 B0)))) didn't succeeded in 25 steps. 114. ((^ A0 . (a0 (A0 A0))) (^ B0 . (a0 (B0 B0)))) didn't succeeded in 25 steps. 115. ((^ A0 . (a0 (A0 A0))) (^ B0 . (b0 (B0 B0)))) didn't succeeded in 25 steps. 116. ((^ A0 . (a0 (^ B0 . (A0 A0)))) (^ C0 . (C0 C0))) failed. 117. ((^ A0 . (a0 (b0 (A0 A0)))) (^ B0 . (B0 B0))) failed. 118. ((^ A0 . A0) ((^ B0 . (B0 B0)) (^ C0 . (C0 C0)))) failed. 119. ((a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) a0) failed. 120. ((a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) b0) failed. 121. ((a0 a0) ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. 122. ((a0 b0) ((^ A0 . (A0 A0)) (^ B0 . (B0 B0)))) failed. 123. (^ A0 . (((^ B0 . (B0 B0)) (^ C0 . (C0 C0))) A0)) failed. 124. (^ A0 . (((^ B0 . (B0 B0)) (^ C0 . (C0 C0))) a0)) failed. 125. (^ A0 . ((^ B0 . ((B0 B0) A0)) (^ C0 . (C0 C0)))) failed. 126. (^ A0 . ((^ B0 . ((B0 B0) B0)) (^ C0 . (C0 C0)))) failed. 127. (^ A0 . ((^ B0 . ((B0 B0) a0)) (^ C0 . (C0 C0)))) failed. 128. (^ A0 . ((^ B0 . (A0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 129. (^ A0 . ((^ B0 . (B0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 130. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) A0)))) didn't succeeded in 25 steps. 131. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) C0)))) didn't succeeded in 25 steps. 132. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . ((C0 C0) a0)))) didn't succeeded in 25 steps. 133. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (A0 (C0 C0))))) didn't succeeded in 25 steps. 134. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 (C0 C0))))) didn't succeeded in 25 steps. 135. (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (a0 (C0 C0))))) didn't succeeded in 25 steps. 136. (^ A0 . ((^ B0 . (^ C0 . (B0 B0))) (^ D0 . (D0 D0)))) failed. 137. (^ A0 . ((^ B0 . (a0 (B0 B0))) (^ C0 . (C0 C0)))) failed. 138. (^ A0 . (A0 ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 139. (^ A0 . (^ B0 . ((^ C0 . (C0 C0)) (^ D0 . (D0 D0))))) failed. 140. (^ A0 . (a0 ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 141. (a0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) a0)) failed. 142. (a0 (((^ A0 . (A0 A0)) (^ B0 . (B0 B0))) b0)) failed. 143. (a0 ((^ A0 . ((A0 A0) A0)) (^ B0 . (B0 B0)))) failed. 144. (a0 ((^ A0 . ((A0 A0) a0)) (^ B0 . (B0 B0)))) failed. 145. (a0 ((^ A0 . (A0 (A0 A0))) (^ B0 . (B0 B0)))) failed. 146. (a0 ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) B0)))) didn't succeeded in 25 steps. 147. (a0 ((^ A0 . (A0 A0)) (^ B0 . ((B0 B0) b0)))) didn't succeeded in 25 steps. 148. (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 (B0 B0))))) didn't succeeded in 25 steps. 149. (a0 ((^ A0 . (A0 A0)) (^ B0 . (b0 (B0 B0))))) didn't succeeded in 25 steps. 150. (a0 ((^ A0 . (^ B0 . (A0 A0))) (^ C0 . (C0 C0)))) failed. 151. (a0 ((^ A0 . (a0 (A0 A0))) (^ B0 . (B0 B0)))) failed. 152. (a0 (^ A0 . ((^ B0 . (B0 B0)) (^ C0 . (C0 C0))))) failed. 153. (a0 (a0 ((^ A0 . (A0 A0)) (^ B0 . (B0 B0))))) failed. |
In Search for The Irreducible Lambda-Expressions.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment