In Search for The Irreducible Lambda-Expressions.




; 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.

No comments:

Post a Comment